POPL 2017
Sun 15 - Sat 21 January 2017
Thu 19 Jan 2017 14:20 - 14:45 at Amphitheater 44 - Concurrency 2 Chair(s): Nobuko Yoshida

Previous work on the semantics of relaxed shared-memory concurrency has only considered the case in which each load reads the data of exactly one store. In practice, however, multiprocessors support mixed-size accesses, and these are used by systems software and (to some degree) exposed at the C/C++ language level. A semantic foundation for software therefore has to address them.

We investigate the mixed-size behaviour of ARMv8 and IBM POWER architectures and implementations: by experiment, by developing semantic models, by testing the correspondence between these, and by discussion with ARM and IBM staff. This turns out to be surprisingly subtle, and on the way we have to revisit the fundamental concepts of coherence and sequential consistency, which change in this setting. In particular, we show that adding a memory barrier between each instruction does not restore sequential consistency. We go on to extend the C/C++11 model to support non-atomic mixed-size memory accesses, and prove the standard compilation scheme from C11 atomics to POWER remains sound.

This is a necessary step towards semantics for real-world shared-memory concurrent code, beyond litmus tests.

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