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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:20 - 16:00: Concurrency 1POPL at Auditorium
Chair(s): Ilya SergeyUniversity College London
14:20 - 14:45
A Promising Semantics for Relaxed-Memory Concurrency
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
14:45 - 15:10
Automatically Comparing Memory Consistency Models
John WickersonImperial College London, Mark BattyUniversity of Kent, Tyler SorensenImperial College London, George A. ConstantinidesImperial College London, UK
Pre-print Media Attached File Attached
15:10 - 15:35
Interactive Proofs in Higher-Order Concurrent Separation Logic
Robbert KrebbersDelft University of Technology, Netherlands, Amin Timanyimec - Distrinet, KU Leuven, Lars BirkedalAarhus University
DOI Pre-print Media Attached
15:35 - 16:00
A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic
Morten Krogh-JespersenAarhus University, Kasper SvendsenAarhus University, Lars BirkedalAarhus University