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

We present a lightweight approach to Hoare-style specifications for fine-grained concurrency, based on a notion of time-stamped histories that abstractly capture atomic changes in the program state. Our key observation is that histories form a partial commutative monoid, a structure fundamental for representation of concurrent resources. This insight provides us with a unifying mechanism that allows us to treat histories just like heaps in separation logic. For example, both are subjects to the same assertion logic and inference rules. Moreover, the notion of ownership transfer, which usually applies to heaps, has an equivalent in histories. It can be used to formally represent helping—an important design pattern for concurrent algorithms whereby one thread can execute code on behalf of another. Specifications in terms of histories naturally abstract away the internal interference, so that sophisticated fine-grained algorithms can be given the same specifications as their simplified coarse-grained counterparts, making them equally convenient for client-side reasoning.

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