Write a Blog >>
Fri 22 Jan 2016 11:45 - 12:10 at Grand Bay South - Track 2: Semantics and memory models Chair(s): Alexey Gotsman

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.57MiB

Fri 22 Jan

POPL-2016-papers
10:30 - 12:10: Research Papers - Track 2: Semantics and memory models at Grand Bay South
Chair(s): Alexey GotsmanIMDEA
POPL-2016-papers10:30 - 10:55
Talk
Shaked FlurUniversity of Cambridge, Kathryn E. GrayUniversity of Cambridge, Christopher PulteUniversity of Cambridge, Susmit SarkarUniversity of St Andrews, Luc MarangetINRIA Rocquencourt, Ali SezginUniversity of Cambridge, Will DeaconARM Ltd., Peter SewellUniversity of Cambridge
Media Attached File Attached
POPL-2016-papers10:55 - 11:20
Talk
Jean Pichon-PharabodUniversity of Cambridge, Peter SewellUniversity of Cambridge
File Attached
POPL-2016-papers11:20 - 11:45
Talk
John WickersonImperial College London, Mark BattyUniversity of Cambridge, Alastair DonaldsonImperial College London
Pre-print File Attached
POPL-2016-papers11:45 - 12:10
Talk
Ori LahavMPI-SWS, Nick GiannarakisMPI-SWS, Viktor VafeiadisMPI-SWS, Germany
Pre-print Media Attached File Attached