UTP semantics for the MCA ARMv8 architecture

Hardware architectures like x86 and ARM provide relaxed memory models for efficiency reasons. The revised ARMv8 architecture is multi-copy atomic (MCA), which brings relaxed-memory effects through thread-local out-of-order, speculative execution and thread-local buffering. In this paper, we investigate the trace semantics for the MCA ARMv8 architecture, acting in the denotational semantics style based on Unifying Theories of Programming (UTP). In order to present all the valid execution results including reorderings of any program under ARMv8, a trace expressed as a sequence of snapshots is introduced, and it relies heavily on various dependencies among program statements. We also study the algebraic laws for MCA ARMv8, including a set of sequential and parallel expansion laws, which are implemented in the rewriting engine Maude. The concept of head normal form is explored for each program, and every program is described in the form of guarded choice which can model the execution of a program with reorderings. Therefore, the linearizability for ARMv8 is supported. Finally, we provide a strategy for deriving the trace semantics from the algebraic semantics. Using the strategy, the trace semantics for each program can be calculated.