Taming Release-Acquire Consistency
Abstract
This paper introduces a strengthening of the release-acquire fragment of the C11 memory model that
- forbids dubious behaviors of programs such as 2+2W that are not observed in any implementation;
- supports fence instructions that restore sequential consistency; and
- admits an equivalent intuitive operational semantics based on point-to-point communication.
This strengthening has no additional implementation cost: it allows the same local optimizations as C11 release and acquire accesses, and has exactly the same compilation schemes to the x86-TSO and Power architectures. In fact, the compilation to Power is complete with respect to a recent axiomatic model of Power; that is, the compiled program exhibits exactly the same behaviors as the source one. Moreover, we provide criteria for placing enough fence instructions to ensure sequential consistency, and apply them to an efficient RCU implementation.
Paper
-
Ori Lahav, Nick Giannarakis, and Viktor Vafeiadis.
Taming release-acquire consistency.
In POPL 2016: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 2016.
[Full paper with appendix]
People
- Ori Lahav (MPI-SWS)
- Nick Giannarakis (MPI-SWS)
- Viktor Vafeiadis (MPI-SWS)
Coq formalisation
Some of the proofs in the paper have been formalized in Coq (latest version 1.1, released 2016-12-20).- Download the formalization [sra-1.1.zip] [README.txt] [CHANGELOG.txt] [all versions]
- Browse the formalization online [proofs hidden] [proofs visible]
- Download a VirtualBox bootable virtual machine with Debian, Coq 8.4, and version 1.0 of the formalization [sravm.ova, 1GB].
MD5 hashes for all the downloads can be found here.