Repairing Sequential Consistency in C/C++11
The C/C++11 memory model defines the semantics of concurrent memory accesses in C/C++, and in particular supports racy “atomic” accesses at a range of different consistency levels, from very weak consistency (“relaxed”) to strong, sequential consistency (“SC”). Unfortunately, as we observe in this paper, the semantics of SC atomic accesses in C/C++11, as well as in all proposed strengthenings of the semantics, is flawed, in that both suggested compilation schemes to Power are unsound. We propose a better semantics for SC accesses that restores the soundness of the compilation schemes to Power, maintains the DRF-SC guarantee, and provides stronger, more useful, guarantees to SC fences. In addition, we formally prove, for the first time, the correctness of the proposed stronger compilation schemes to Power that preserve load-to-store ordering and avoid “thin-air” reads.
Conference DayTue 20 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:10 - 17:00 | CorrectnessPLDI Research Papers at Actes, Civil Engineering Chair(s): Joseph DeviettiUniversity of Pennsylvania | ||
16:10 25mTalk | Repairing Sequential Consistency in C/C++11 PLDI Research Papers Ori LahavMPI-SWS, Viktor VafeiadisMPI-SWS, Germany, Jeehoon KangSeoul National University, Chung-Kil HurSeoul National University, Derek DreyerMPI-SWS Media Attached | ||
16:35 25mTalk | Taming Undefined Behavior in LLVM PLDI Research Papers Juneyoung LeeSeoul National University, Yoonseung KimSeoul National University (South Korea), Youngju SongSeoul National University, Chung-Kil HurSeoul National University, Sanjoy DasAzul Systems, David MajnemerGoogle, John RegehrUniversity of Utah, Nuno P. LopesMicrosoft Research Pre-print Media Attached | ||