PPoPP 2016
Sat 12 - Wed 16 March 2016 Barcelona, Spain
Wed 16 Mar 2016 10:25 - 10:50 at Mallorca+Menorca - Consistency models Chair(s): James Larus

Modern shared memory multiprocessors permit reordering of memory operations for performance reasons. These reorderings are often a source of subtle bugs in programs written for such architectures. Traditional approaches to verify weak memory programs often rely on interleaving semantics, which is prone to state space explosion, and thus severely limits the scalability of the analysis. In recent times, there has been a renewed interest in modelling dynamic executions of weak memory programs using partial orders. However, such an approach typically requires ad-hoc mechanisms to correctly capture the data and control-flow choices/conflicts present in real-world programs. In this work, we propose a novel, conflict-aware, composable, truly concurrent semantics for programs written using C/C++ for modern weak memory architectures. We exploit our symbolic semantics based on general event structures to build an efficient decision procedure that detects assertion violations in bounded multi-threaded programs. Using a large, representative set of benchmarks, we show that our conflict-aware semantics outperforms the state-of-the-art partial-order based approaches.

Wed 16 Mar

Displayed time zone: Belfast change

10:00 - 11:15
Consistency modelsMain conference at Mallorca+Menorca
Chair(s): James Larus EPFL
10:00
25m
Talk
Benchmarking Weak Memory Models
Main conference
Carl Ritson University of Kent, Scott Owens University of Kent
Link to publication DOI
10:25
25m
Talk
The Virtues of Conflict: Analysing Modern ConcurrencyArtifact Evaluation
Main conference
Ganesh Narayanswamy Department of Computer Science, University of Oxford, Saurabh Joshi Department of Computer Science and Engineering, IIT Guwahati, Daniel Kroening University of Oxford
Link to publication DOI
10:50
25m
Talk
Causal Consistency: Beyond Memory
Main conference
Matthieu Perrin University of Nantes, Achour Mostefaoui University of Nantes, Claude Jard University of Nantes
Link to publication DOI