Relaxed exception semantics for Arm-A (extended version)

TL;DR

The paper tackles the challenge of defining precise exception semantics under relaxed memory for Arm-A, arguing that classic sequential notions are insufficient in modern out-of-order and speculative execution environments. It delivers an executable axiomatic model of Arm-A precise exceptions, implemented in Isla-cav from a Sail-derived Armv9.4-A ISA, and validates the framework with litmus tests and hardware experiments, while also outlining the semantics of synchronous external aborts and SGIs. The work also sketches an extension path for Chapter 7 GIC/SGI machinery, including a draft axiomatic extension to accommodate inter-processor interrupts and system-wide barriers, enabling practical reasoning about real-world synchronization patterns such as RCU and Verona-like locks. Overall, the paper provides a robust foundation for precise hardware-software interfaces in relaxed-memory systems and identifies the central open problem of a universally applicable definition of precision under memory relaxation, guiding future modeling and validation efforts.

Abstract

To manage exceptions, software relies on a key architectural guarantee, precision: that exceptions appear to execute between instructions. However, this definition, dating back over 60 years, fundamentally assumes a sequential programmers model. Modern architectures such as Arm-A with programmer-observable relaxed behaviour make such a naive definition inadequate, and it is unclear exactly what guarantees programmers have on exception entry and exit. In this paper, we clarify the concepts needed to discuss exceptions in the relaxed-memory setting -- a key aspect of precisely specifying the architectural interface between hardware and software. We explore the basic relaxed behaviour across exception boundaries, and the semantics of external aborts, using Arm-A as a representative modern architecture. We identify an important problem, present yet unexplored for decades: pinning down what it means for exceptions to be precise in a relaxed setting. We describe key phenomena that any definition should account for. We develop an axiomatic model for Arm-A precise exceptions, tooling for axiomatic model execution, and a library of tests. Finally we explore the relaxed semantics of software-generated interrupts, as used in sophisticated programming patterns, and sketch how they too could be modelled.

Figures (14)

• Figure 1: Top. The tree of (partially) executed FDX instances at one time, in hardware or operational model execution. Bottom. The sequence of architecturally executed FDX instances in a completed execution.
• Figure 2: Arm prose specification Arm-K.a (top) and our suggested rephrasing (bottom).
• Figure 3: The tree of partially and completely executed FDX instances with exceptions, in hardware or operational model execution. Instructions may execute out-of-order across exception boundaries, requiring a modern definition for precision.
• Figure 4: Reads and writes may be executed out-of-order across exception entry, exit, or even both. This shows executing a read out-of-order across exception entry+exit.
• Figure 5: Context synchronising exception entry (and returns) are not executed speculatively.