POPL 2017
Sun 15 - Sat 21 January 2017
Wed 18 Jan 2017 14:45 - 15:10 at Auditorium - Concurrency 1 Chair(s): Ilya Sergey

A memory consistency model (MCM) is the part of a programming language or computer architecture specification that defines which values can legally be read from shared memory locations. Because MCMs take into account various optimisations employed by architectures and compilers, they are often complex and counterintuitive, which makes them challenging to design and to understand.

We identify four tasks involved in designing and understanding MCMs: generating conformance tests, distinguishing two MCMs, checking compiler optimisations, and checking compiler mappings. We show that all four tasks are instances of a general constraint-satisfaction problem to which the solution is either a program or a pair of programs. Although this problem is intractable for automatic solvers when phrased over programs directly, we show how to solve analogous constraints over program executions, and then construct programs that satisfy the original constraints.

Our technique, which is implemented in the Alloy modelling framework, is illustrated on several software- and architecture-level MCMs, both axiomatically and operationally defined. We automatically recreate several known results, often in a simpler form, including: distinctions between variants of the C11 MCM; a failure of the ‘SC-DRF guarantee’ in an early C11 draft; that x86 is ‘multi-copy atomic’ and Power is not; bugs in common C11 compiler optimisations; and bugs in a compiler mapping from OpenCL to AMD-style GPUs. We also use our technique to develop and validate a new MCM for NVIDIA GPUs that supports a natural mapping from OpenCL.

Preprint (memalloy.pdf)527KiB

Wed 18 Jan

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

14:20 - 16:00
Concurrency 1POPL at Auditorium
Chair(s): Ilya Sergey University College London
14:20
25m
Talk
A Promising Semantics for Relaxed-Memory Concurrency
POPL
Jeehoon Kang Seoul National University, Chung-Kil Hur Seoul National University, Ori Lahav MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany, Derek Dreyer MPI-SWS
Link to publication Pre-print Media Attached
14:45
25m
Talk
Automatically Comparing Memory Consistency Models
POPL
John Wickerson Imperial College London, Mark Batty University of Kent, Tyler Sorensen Imperial College London, George A. Constantinides Imperial College London, UK
Pre-print Media Attached File Attached
15:10
25m
Talk
Interactive Proofs in Higher-Order Concurrent Separation Logic
POPL
Robbert Krebbers Delft University of Technology, Netherlands, Amin Timany imec - Distrinet, KU Leuven, Lars Birkedal Aarhus University
DOI Pre-print Media Attached
15:35
25m
Talk
A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic
POPL
Morten Krogh-Jespersen Aarhus University, Kasper Svendsen Aarhus University, Lars Birkedal Aarhus University