An Operational Semantics for C/C++11 Concurrency
Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
Association for Computing Machinery
MetadataShow full item record
Nienhuis, K., Memarian, K., & Sewell, P. (2016). An Operational Semantics for C/C++11 Concurrency. Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, 111-128. https://doi.org/10.1145/2983990.2983997
The C/C++11 concurrency model balances two goals: it is relaxed enough to be efficiently implementable and (leaving aside the "thin-air" problem) it is strong enough to give useful guarantees to programmers. It is mathematically precise and has been used in verification research and compiler testing. However, the model is expressed in an axiomatic style, as predicates on complete candidate executions. This suffices for computing the set of allowed executions of a small litmus test, but it does not directly support the incremental construction of executions of larger programs. It is also at odds with conventional operational semantics, as used implicitly in the rest of the C/C++ standards. Our main contribution is the development of an operational model for C/C++11 concurrency. This covers all the features of the previous formalised axiomatic model, and we have a mechanised proof that the two are equivalent, in Isabelle/ HOL. We also integrate this semantics with an operational semantics for sequential C (described elsewhere); the combined semantics can incrementally execute programs in a small fragment of C. Doing this uncovered several new aspects of the C/C++11 model: we show that one cannot build an equivalent operational model that simply follows program order, sequential consistent order, or the synchronises-with order. The first negative result is forced by hardware-observable behaviour, but the latter two are not, and so might be ameliorated by changing C/C++11. More generally, we hope that this work, with its focus on incremental construction of executions, will inform the future design of new concurrency models.
This work was partly funded by a Gates studentship (Nienhuis) and by the EPSRC Programme Grant REMS: Rigorous Engineering for Mainstream Systems, EP/K008528/1.
External DOI: https://doi.org/10.1145/2983990.2983997
This record's URL: https://www.repository.cam.ac.uk/handle/1810/264329