POPL 2017
Sun 15 - Sat 21 January 2017
Thu 19 Jan 2017 15:35 - 16:00 at Amphitheater 44 - Concurrency 2 Chair(s): Nobuko Yoshida

A thread-modular proof for the correctness of a concurrent program is based on an inductive and interference-free annotation of each thread. It is well-known that the corresponding proof system is not complete (unless one adds auxiliary variables). We introduce a hierarchy of proof systems where each level $k$ corresponds to a new notion of thread modularity (level 1 corresponds to the original notion). Each level is strictly more expressive than the previous. The hierarchy can be used to prove interesting programs. We give the to our knowledge first proof of the MACH shootdown algorithm for TLB consistency. The algorithm is correct for an arbitrary number of CPUs.

Thu 19 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:20 - 16:00
Concurrency 2POPL at Amphitheater 44
Chair(s): Nobuko Yoshida Imperial College London, UK
14:20
25m
Talk
Mixed-size Concurrency: ARM, POWER, C/C++11, and SC
POPL
Shaked Flur University of Cambridge, Susmit Sarkar University of St. Andrews, UK, Christopher Pulte University of Cambridge, Kyndylan Nienhuis University of Cambridge, Luc Maranget INRIA Rocquencourt, Kathryn E. Gray University of Cambridge, Ali Sezgin University of Cambridge, Mark Batty University of Kent, Peter Sewell University of Cambridge
14:45
25m
Talk
Dynamic Race Detection For C++11
POPL
Christopher Lidbury Imperial College London, Alastair F. Donaldson Imperial College London
15:10
25m
Talk
Serializability for Eventual Consistency: Criterion, Analysis and Applications
POPL
Lucas Brutschy ETH Zurich, Dimitar Dimitrov ETH Zurich, Switzerland, Peter Müller ETH Zurich, Martin Vechev ETH Zurich
Pre-print
15:35
25m
Talk
Thread Modularity at Many Levels: a Pearl in Compositional Verification
POPL
Jochen Hoenicke Universität Freiburg, Rupak Majumdar MPI-SWS, Andreas Podelski University of Freiburg, Germany