The Problem of Programming Language Concurrency Semantics

Batty, Mark and Memarian, Kayvan and Nienhuis, Kyndylan and Pichon-Pharabod, Jean and Sewell, Peter (2015) The Problem of Programming Language Concurrency Semantics. In: 24th European Symposium on Programming, held as Part of the European Joint Conferences on Theory and Practice of Software, 11-18 Apr 2015, London, UK. (doi:https://doi.org/10.1007/978-3-662-46669-8_12) (Full text available)

PDF
Download (296kB) Preview
[img]
Preview
Official URL
http://dx.doi.org/10.1007/978-3-662-46669-8_12

Abstract

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)
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Mark Batty
Date Deposited: 03 Nov 2015 08:26 UTC
Last Modified: 17 Jan 2017 20:51 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/50271 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year