The Semantics of Multicopy Atomic ARMv8 and RISC-V

Change log
Pulte, Christopher 

Previous work has established precise operational concurrency models for Power and ARMv8, in an abstract micro-architectural style based on detailed discussion with IBM and ARM staff and extensive hardware testing. To account for the precise architectural behaviour these models are complex. This thesis aims to provide a better understanding for the relaxed memory concurrency models of the architectures ARMv8, RISC-V, and (to a lesser degree) Power.

Power and early versions of ARMv8 have non-multicopy-atomic (non-MCA) concurrency models. This thesis provides abstraction results for these, including a more abstract non-MCA ARMv8 storage subsystem model, and characterisations of the behaviour of mixed-size Power and non-MCA ARMv8 programs when using barriers or release/acquire instructions for all memory accesses, with respect to notions of Sequential Consistency for mixed-size programs.

During the course of this PhD project, and partly due to our extended collaboration with ARM, ARM have shifted to a much simplified multicopy-atomic concurrency architecture that also includes a formal axiomatic concurrency model. We develop a correspondingly simplified operational model based on the previous non-MCA models, and, as the main result of this thesis, prove equivalence between the simplified operational and the reference axiomatic model.

We have also been actively involved in the RISC-V Memory Model Task Group. RISC-V has adopted a multicopy atomic model closely following that of ARMv8, but which incorporates some changes motivated by issues raised in our operational modelling of ARMv8. We develop an adapted RISC-V operational concurrency model that is now part of the official architecture documentation.

Finally, in order to give a simpler explanation of the MCA ARMv8 and RISC-V concurrency models for programmers, we develop an equivalent operational concurrency model in a different style. The \promisingarmriscv model, based on the C11 Promising model, gives up the micro-architectural intuition the other operational models offer in favour of providing a more abstract model. We prove it equivalent to the MCA ARMv8 and RISC-V axiomatic models in Coq.

Sewell, Peter Michael
Programming language semantics, relaxed memory concurrency, processor architectures
Doctor of Philosophy (PhD)
Awarding Institution
University of Cambridge
This work was funded by a Computer Laboratory and Qualcomm Premium Studentship, an EPSRC and Arm Ltd. Industrial CASE Studentship (grant no. EP/L505389/1), and the EPSRC Programme Grant “REMS: Rigorous Engineering for Mainstream Systems” (grant no. EP/K008528/1).