Blogs (9) >>
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
Wed 2 Nov 2016 11:20 - 11:45 at Matterhorn 2 - Semantics and Verification Chair(s): Jonathan Aldrich

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.

Wed 2 Nov

10:30 - 12:10: OOPSLA - Semantics and Verification at Matterhorn 2
Chair(s): Jonathan AldrichCarnegie Mellon University
splash-2016-oopsla147807900000010:30 - 10:55
Andrei StefanescuUniversity of Illinois at Urbana-Champaign, Daejun ParkUniversity of Illinois at Urbana-Champaign, Shijiao YuwenUniversity of Illinois at Urbana-Champaign, Yilong LiRuntime Verification, Inc., Grigore RosuUniversity of Illinois at Urbana-Champaign
DOI Media Attached
splash-2016-oopsla147808050000010:55 - 11:20
Ilya SergeyUniversity College London, Aleksandar NanevskiIMDEA Software Institute, Anindya BanerjeeIMDEA Software Institute, Germán Andrés DelbiancoIMDEA Software Institute
DOI Pre-print Media Attached File Attached
splash-2016-oopsla147808200000011:20 - 11:45
Kyndylan NienhuisUniversity of Cambridge, Kayvan MemarianUniversity of Cambridge, Peter SewellUniversity of Cambridge
splash-2016-oopsla147808350000011:45 - 12:10
Andrei Marian DanETH Zurich, Patrick LamUniversity of Waterloo, Canada, Torsten HoeflerETH Zurich, Martin VechevETH Zurich
DOI Pre-print Media Attached