BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The Problem of Programming Language Concurrency Semantics - Jean P
 ichon-Pharabod
DTSTART:20150408T120000Z
DTEND:20150408T130000Z
UID:TALK58864@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:Despite decades of research\, we do not have a satisfactory co
 ncurrency semantics for any general-purpose programming language that aims
  to support concurrent systems code.  The Java Memory Model has been shown
  to be unsound with respect to standard compiler optimisations\, while the
  C/C++11 model is too weak\, admitting undesirable *thin-air executions*.\
 n\nOur goal in this work is to articulate this major open problem as clear
 ly as is currently possible\, showing how it arises from the combination o
 f multiprocessor relaxed-memory behaviour and the desire to accommodate cu
 rrent compiler optimisations.  We make several novel contributions that ea
 ch shed some light on the problem\, constraining the possible solutions an
 d identifying new difficulties.\n\nFirst we give a positive result\, provi
 ng in HOL4 that the existing axiomatic model for C/C++11 guarantees sequen
 tially consistent semantics for simple race-free programs that do not use 
 low-level atomics (DRF-SC\, one of the core design goals).  We then descri
 be the thin-air problem and show that it cannot be solved\, without restri
 cting current compiler optimisations\, using any per-candidate-execution c
 ondition in the style of the C/C++11 model.  Thin-air executions were thou
 ght to be confined to programs using relaxed atomics\, but we further show
  that they recur when one attempts to integrate the concurrency model with
  more of C\, mixing atomic and nonatomic accesses\, and that also breaks t
 he DRF-SC result.  We then describe a semantics based on an explicit opera
 tional construction of out-of-order execution\, giving the desired behavio
 ur for thin-air examples but exposing further difficulties with accommodat
 ing existing compiler optimisations.  Finally\, we show that there are maj
 or difficulties integrating concurrency semantics with the C/C++ notion of
  undefined behaviour.\n\nWe hope thereby to stimulate and enable research 
 on this key issue. \n\n[This is a practice talk for ESOP 2015]\n\nMark Bat
 ty\, Kayvan Memarian\, Kyndylan Nienhuis\, Jean Pichon-Pharabod\, Peter Se
 well
LOCATION:FW11
END:VEVENT
END:VCALENDAR