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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10
Semantics and VerificationOOPSLA at Matterhorn 2
Chair(s): Jonathan Aldrich Carnegie Mellon University
Semantics-Based Program Verifiers for All LanguagesAECDistinguished Paper Award
Andrei Stefanescu University of Illinois at Urbana-Champaign, Daejun Park University of Illinois at Urbana-Champaign, Shijiao Yuwen University of Illinois at Urbana-Champaign, Yilong Li Runtime Verification, Inc., Grigore Roşu University of Illinois at Urbana-Champaign
DOI Media Attached
Hoare-Style Specifications as Correctness Conditions for Non-linearizable Concurrent ObjectsAEC
Ilya Sergey University College London, Aleksandar Nanevski IMDEA Software Institute, Anindya Banerjee IMDEA Software Institute, Germán Andrés Delbianco IMDEA Software Institute
DOI Pre-print Media Attached File Attached
An Operational Semantics for C/C++11 ConcurrencyAEC
Kyndylan Nienhuis University of Cambridge, Kayvan Memarian University of Cambridge, Peter Sewell University of Cambridge
Modeling and Analysis of Remote Memory Access ProgrammingAECDistinguished Paper Award
Andrei Marian Dan ETH Zurich, Patrick Lam University of Waterloo, Canada, Torsten Hoefler ETH Zurich, Martin Vechev ETH Zurich
DOI Pre-print Media Attached