Despite decades of research, we do not have a satisfactory concurrency semantics for any general-purpose programming language that aims to support concurrent systems code. The Java Memory Model has been shown to be unsound with respect to standard compiler optimisations, while the C/C++11 model is too weak, admitting undesirable thin-air executions. Our goal in this paper is to articulate this major open problem as clearly as is currently possible, showing how it arises from the combination of multiprocessor relaxed-memory behaviour and the desire to accommodate current compiler optimisations. We make several novel contributions that each shed some light on the problem, constraining the possible solutions and identifying new difficulties.
Wed 15 AprDisplayed time zone: Azores change
Wed 15 Apr
Displayed time zone: Azores change
10:30 - 12:30 | |||
10:30 30mTalk | The Problem of Programming Language Concurrency Semantics ESOP Mark Batty University of Cambridge, Kayvan Memarian University of Cambridge, Kyndylan Nienhuis University of Cambridge, Jean Pichon-Pharabod University of Cambridge, Peter Sewell University of Cambridge | ||
11:00 30mTalk | The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO ESOP | ||
11:30 30mTalk | Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity ESOP Ilya Sergey IMDEA Software Institute, Aleksandar Nanevski IMDEA Software Institute, Anindya Banerjee IMDEA Software Institute | ||
12:00 30mTalk | Witnessing (Co)datatypes ESOP |