We introduce a strengthening of the release-acquire fragment of the C11 memory model that (i) forbids dubious behaviors that are not observed in any implementation; (ii) supports fence instructions that restore sequential consistency; and (iii) 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 demonstrate their application to an efficient RCU implementation.
Poster (poster.pdf) | 1.58MiB |
Fri 22 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
10:30 - 12:10 | Track 2: Semantics and memory modelsResearch Papers at Grand Bay South Chair(s): Alexey Gotsman IMDEA | ||
10:30 25mTalk | Modelling the ARMv8 Architecture, Operationally: Concurrency and ISA Research Papers Shaked Flur University of Cambridge, Kathryn E. Gray University of Cambridge, Christopher Pulte University of Cambridge, Susmit Sarkar University of St Andrews, Luc Maranget INRIA Rocquencourt, Ali Sezgin University of Cambridge, Will Deacon ARM Ltd., Peter Sewell University of Cambridge Media Attached File Attached | ||
10:55 25mTalk | A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions Research Papers File Attached | ||
11:20 25mTalk | Overhauling SC atomics in C11 and OpenCL Research Papers John Wickerson Imperial College London, Mark Batty University of Cambridge, Alastair F. Donaldson Imperial College London Pre-print File Attached | ||
11:45 25mTalk | Taming Release-Acquire Consistency Research Papers Pre-print Media Attached File Attached |