POPL 2017
Sun 15 - Sat 21 January 2017
Wed 18 Jan 2017 14:20 - 14:45 at Auditorium - Concurrency 1 Chair(s): Ilya Sergey

Despite many years of research, it has proven very difficult to develop a memory model for concurrent programming languages that adequately balances the conflicting desiderata of programmers, compilers, and hardware. In this paper, we propose the first relaxed memory model that (1) accounts for nearly all the features of the C++11 concurrency model, (2) provably validates a number of standard compiler optimizations, as well as a wide range of memory access reorderings that commodity hardware may perform, (3) avoids bad “out-of-thin-air” behaviors that break invariant-based reasoning, (4) supports “DRF” guarantees, ensuring that programmers who use sufficient synchronization need not understand the full complexities of relaxed-memory semantics, and (5) defines the semantics of racy programs without relying on undefined behaviors, which is a prerequisite for applicability to type-safe languages like Java.

The key novel idea behind our model is the notion of promises: a thread may promise to execute a write in the future, thus enabling other threads to read from that write out of order. Crucially, to prevent out-of-thin-air behaviors, a promise step requires a thread-local certification that it will be possible to execute the promised write even in the absence of the promise. To establish confidence in our model, we have formalized most of our key results in Coq.

Wed 18 Jan

POPL-2017-papers
14:20 - 16:00: POPL - Concurrency 1 at Auditorium
Chair(s): Ilya SergeyUniversity College London
POPL-2017-papers14:20 - 14:45
Talk
Jeehoon KangSeoul National University, Chung-Kil HurSeoul National University, Ori LahavMPI-SWS, Viktor VafeiadisMPI-SWS, Germany, Derek DreyerMPI-SWS
Link to publication Pre-print Media Attached
POPL-2017-papers14:45 - 15:10
Talk
John WickersonImperial College London, Mark BattyUniversity of Kent, Tyler SorensenImperial College London, George A. ConstantinidesImperial College London, UK
Pre-print Media Attached File Attached
POPL-2017-papers15:10 - 15:35
Talk
Robbert KrebbersDelft University of Technology, Netherlands, Amin Timanyimec - Distrinet, KU Leuven, Lars BirkedalAarhus University
DOI Pre-print Media Attached
POPL-2017-papers15:35 - 16:00
Talk
Morten Krogh-JespersenAarhus University, Kasper SvendsenAarhus University, Lars BirkedalAarhus University