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

We present a method for automatic fence insertion in concurrent programs running under weak memory models that provides the best known trade-off between efficiency and optimality. On the one hand, the method can efficiently handle complex aspects of program behaviors such as unbounded buffers and large numbers of processes. On the other hand, it is able to find small sets of fences needed for ensuring correctness of the program. To this end, we propose a novel notion of correctness, called persistence, that compares the behavior of the program under the weak memory semantics with that under the classical interleaving semantics. We instantiate our framework for the Total Store Ordering memory model, and give an algorithm that reduces the fence insertion problem under TSO to the reachability problem for programs running under SC. Furthermore, we provide an abstraction scheme that substantially increases scalability to large numbers of processes.

Conference Day
Wed 15 Apr

Displayed time zone: Azores change

10:30 - 12:30
Session 4ESOP at Skeel
Chair(s): Lars BirkedalAarhus University
10:30
30m
Talk
The Problem of Programming Language Concurrency Semantics
ESOP
Mark BattyUniversity of Cambridge, Kayvan MemarianUniversity of Cambridge, Kyndylan NienhuisUniversity of Cambridge, Jean Pichon-PharabodUniversity of Cambridge, Peter SewellUniversity 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 AtigUppsala University, Tuan Phong NgoUppsala University
11:30
30m
Talk
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity
ESOP
Ilya SergeyIMDEA Software Institute, Aleksandar NanevskiIMDEA Software Institute, Anindya BanerjeeIMDEA Software Institute
12:00
30m
Talk
Witnessing (Co)datatypes
ESOP
Jasmin BlanchetteTU Munich, Andrei PopescuMiddlesex University, London, Dmitriy TraytelTU Munich