Artifact: An operational semantics for C/C++ 11 concurrency

This artifact belongs to the paper An operational semantics for C/C++11 concurrency by Kyndylan Nienhuis, Kayvan Memarian and Peter Sewell (OOPSLA 2016). The artifact contains the mechanisation of the proof that our operational concurrency model is equivalent to the axiomatic model of Batty et al. The entire artifact can be downloaded as a zip file here.

Getting started

Install Isabelle 2016. If this version is still the latest version it can be downloaded from here, and otherwise from here. Instructions on how to install Isabelle are available on the same web pages.

Troubleshoot: Check whether the selected logic is HOL (a new installation should have this by default). The selected logic is displayed in the Theories panel (top menu: Plugins/Isabelle/Theories panel).

If the reader is not familiar with the axiomatic model, we suggest reading Section 2 of the paper. Table 1 in Section 2 contains an overview of the acronyms used in the axiomatic model, which might be helpful as a reference.

Overview of files

The toplevel file is Cmm_op_proofs.thy. The last theorem in that file states that our operational concurrency model is equivalent to the axiomatic model. The definition of the operational model is contained in Cmm_op.thy.

Nondeterminism.thy contains the definition of the non-deterministic monad, and Nondeterminism_lemmas.thy contains the simplification rules of the monad.

Cmm_master_lemmas.thy contains the auxiliary lemmas we proved about the axiomatic model.

Finally, the lib folder contains all files necessary for the proof which are not original work (the files mentioned above are orginial work). The file Cmm_csem.thy in the lib folder contains the definition of the original axiomatic model.

Correspondence with the paper

Correspondence to definitions and lemmas in the paper: