ESOP 2015
Tue 14 - Thu 16 April 2015 London, United Kingdom
Wed 15 Apr 2015 10:30 - 11:00 at Skeel - Session 4 Chair(s): Lars Birkedal

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 Apr

Displayed time zone: Azores change

10:30 - 12:30
Session 4ESOP at Skeel
Chair(s): Lars Birkedal Aarhus University
10:30
30m
Talk
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
30m
Talk
The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO
ESOP
Parosh Aziz Abdulla , Mohamed Faouzi Atig Uppsala University, Tuan Phong Ngo Uppsala University
11:30
30m
Talk
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
30m
Talk
Witnessing (Co)datatypes
ESOP
Jasmin Blanchette TU Munich, Andrei Popescu Middlesex University, London, Dmitriy Traytel TU Munich