Write a Blog >>
Tue 20 Jun 2017 16:10 - 16:35 at Actes, Civil Engineering - Correctness Chair(s): Joseph Devietti

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 Day
Tue 20 Jun

Displayed 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
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
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