Memory Model meeting, Cambridge, Wed 24

Memory Model meeting, Cambridge, Wed 24 - Thur 25 September 2014

This is an small informal meeting to discuss the design of more satisfactory concurrent memory models for C/C++, Java, and similar programming languages, given the various difficulties (especially the thin-air issues) with the current (C/C++11 and JSR-133) memory models.

Location

Computer Laboratory, University of Cambridge, room FW11 (first floor)

Schedule

We aim for a discussion-heavy schedule rather than a solid block of talks. We'll order in sandwich lunches and likely go for dinner on Wednesday; maybe also Thursday).

Wednesday 24 September (mostly thin-air focussed)

before 9.30: coffee
9.30 introductions
Peter Sewell: The Thin-Air Problem - Introduction
Hans Boehm: Outlawing Ghosts: Avoiding Out-of-Thin-Air Results
Jean Pichon: An out-of-order thread-local semantics for something like volatile relaxed atomics in C and the problems it highlights
Lunch
Viktor Vafeiadis: possible two-phase model reformulation (on whiteboard
Ali Sezgin: ALOOTA
Break
Alan Jeffrey: Event structures and refinement for relaxed memory (Kyndylan whiteboard example)
18.30 dinner - St John Chophouse (booked for 15-20)

Thursday 25 September (thin-air continued and GPGPU)

9.00 coffee and start
Kyndylan Nienhuis: An operational semantics of C11 concurrency
Jean Pichon: An overview of Jaroslav Sevcik's trace-set transformation semantics from "Safe Optimisations for Shared-Memory Concurrent Programs" (PLDI’11)
Lunch
Viktor Vafeiadis: "Easy" fixes to the C11 memory model
Discussion of GPGPU models
Peter Sewell: summary

Context

The following describe our current state of knowledge about the thin-air problem, as far as I know.

Common compiler optimisations are invalid in the C11 memory model and what we can do about it, Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, Francesco Zappa Nardelli. Draft.
C Concurrency Challenges Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon, Peter Sewell. Draft.
Outlawing Ghosts: Avoiding Out-of-Thin-Air Results Hans-J. Boehm, Brian Demsky, MSPC 2014.
Compiler testing via a theory of sound optimisations in the C11/C++11 memory model, R. Morisset, P. Pawan, F. Zappa Nardelli, PLDI'13
Safe Optimisations for Shared-Memory Concurrent Programs. Jaroslav Ševčík. PLDI 2011
jmm-dev discussion (including the event structure semantics sketched by Alan Jeffrey)
the JSR-133 FAQ

Attendees

name	coming?
Paul McKenney (IBM, Linux)	y
Doug Lea (SUNY Oswego, Java)	teleconf (Wed until 11amEDT, Thur until 8amEDT ?)
Hans Boehm (Google)	y
Alan Jeffrey (Bell Labs)	y
Viktor Vafeiadis (MPI-SWS)	y
Olivier Giroux (Nvidia)	y
Torvald Riegel (Red Hat, GCC)	teleconf?
Gustavo Petri (Purdue)	y
Mark Batty (Cambridge)	y
Shaked Flur (Cambridge)	y
Kyndylan Nienhuis (Cambridge)	y
Jean Pichon (Cambridge)	y
Peter Sewell (Cambridge)	y
Ali Sezgin (Cambridge)	y
Susmit Sarkar (St Andrews)	y
Scott Owens (Kent)	y
Carl Ritson (Kent)	y (Wed only?)
Tim Harris (Oracle)	y
Gavin Bierman (Oracle)	y
Hakan Persson (ARM)	y (25 and around 26 am)
Andrew Haley (Redhat)	y
John Wickerson (Imperial)

Also on the mailing cc list:

Ohad Kammar (Cambridge) n

Francesco Zappa Nardelli (INRIA) n

Robin Morisset (INRIA)

Suresh Jagannathan (Purdue, DARPA) n

Richard Grisenthwaite (ARM)

Jem Davies (ARM) y for some ARM - esp.25th

Jeremy Manson (Google)

Jade Alglave (UCL) n

Luc Maranget (INRIA)

Jaroslav Sevcik (Google)

Alistair Donaldson (Imperial)

Ohad Kammar (Cambridge)	n
Francesco Zappa Nardelli (INRIA)	n
Robin Morisset (INRIA)
Suresh Jagannathan (Purdue, DARPA)	n
Richard Grisenthwaite (ARM)
Jem Davies (ARM)	y for some ARM - esp.25th
Jeremy Manson (Google)
Jade Alglave (UCL)	n
Luc Maranget (INRIA)
Jaroslav Sevcik (Google)
Alistair Donaldson (Imperial)