Skip to main content

The Problem of Programming Language Concurrency Semantics

Batty, Mark, Memarian, Kayvan, Nienhuis, Kyndylan, Pichon-Pharabod, Jean, Sewell, Peter (2015) The Problem of Programming Language Concurrency Semantics. In: Lecture Notes in Computer Science. 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings. 9032. pp. 283-307. Springer-Verlag Berlin, Heidleberg, Germany ISBN 978-3-662-46668-1. (doi:10.1007/978-3-662-46669-8_12) (KAR id:50271)

PDF Author's Accepted Manuscript
Language: English
Click to download this file (771kB)
[thumbnail of c_concurrency_challenges.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


Despite decades of research, we do not have a satisfactory concurrency 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.

Our goal in this paper is to articulate this major open problem as clearly as is currently possible, showing how it arises from the combination of multiprocessor relaxed-memory behaviour and the desire to accommodate current compiler optimisations. We make several novel contributions that each shed some light on the problem, constraining the possible solutions and identifying new difficulties.

First we give a positive result, proving in HOL4 that the existing axiomatic model for C/C++11 guarantees sequentially consistent semantics for simple race-free programs that do not use low-level atomics (DRF-SC, one of the core design goals). We then describe the thin-air problem and show that it cannot be solved, without restricting current compiler optimisations, using any per-candidate-execution condition in the style of the C/C++11 model. Thin-air executions were thought 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 the DRF-SC result. We then describe a semantics based on an explicit operational construction of out-of-order execution, giving the desired behaviour for thin-air examples but exposing further difficulties with accommodating existing compiler optimisations. Finally, we show that there are major difficulties integrating concurrency semantics with the C/C++ notion of undefined behaviour.

We hope thereby to stimulate and enable research on this key issue.

Item Type: Conference or workshop item (Paper)
DOI/Identification number: 10.1007/978-3-662-46669-8_12
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Batty
Date Deposited: 03 Nov 2015 08:26 UTC
Last Modified: 09 Dec 2022 04:44 UTC
Resource URI: (The current URI for this page, for reference purposes)
Batty, Mark:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.