ARM have recently revised the ARMv8 architecture with two major simplifications: a shift to a syntactic definition of preserved dependencies and multi-copy-atomicity. Moreover, ARM has introduced an official, formal memory model. This axiomatic memory model was designed alongside and informed by an operational model with an “abstract microarchitectural flavour”, to relate to hardware implementions and enable its validation. Both these two memory models serve their purposes for specification and validation. In both of them, however, execution order is divorced from program order, making them difficult to understand. In particular, in the operational model instructions execute out-of-order, non-atomically, and speculatively, and the model needs to sometimes discard or restart already-executed instructions.
In this paper, we introduce an equivalent simpler operational memory model for ARMv8. This model emphasises the execution of instructions in program order: instructions execute in order, without speculation, and atomically, with the exception of a notion of write promises. RISC-V has recently adopted a memory model closely following that of ARMv8. We extend our model to also handle RISC-V concurrency, in an even simpler model. Moreover, we integrate this model with ISA models for ARMv8 and RISC-V to obtain a more efficient tool for interactive or exhaustive exploration of small algorithm examples. With two simple optimisations it performs better than the two previous models for ARMv8.
The main results are formalised in Coq.