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:

• Definition 5.1: fun incCom (line 214, Cmm_op.thy)
• Theorem 5.2: lemma opsemOrder_isStrictPartialOrder (line 401, Cmm_op_proofs.thy). Here incComAlt is an abbreviation for incCom (pre, wit, getRel pre wit).
• Definition 5.3: definition preRestrict (line 115), and definition incWitRestrict (line 129, Cmm_op.thy). exRestrict is not explicitely defined.
• Definition 5.4: definition downclosed (line 1415, Cmm_csem.thy).
• Theorem 5.5: lemma monotonicity_with_consume_hb (line 1268, Cmm_op_proofs.thy)
• Theorem 5.6: lemma final_with_consume_hb (line 1927, Cmm_op_proofs.thy)
• Theorem 5.7: lemma axsimpConsistent_restriction (line 2341, Cmm_op_proofs.thy)
• Definition 5.8: definition incStep (line 263, Cmm_op.thy)
• Theorem 5.9: lemma existenceIncTrace (line 2572, Cmm_op_proofs.thy)
• Definition 5.10: definition incConsistent (line 318, Cmm_op.thy)
• Theorem 5.11: corollary incConsistentEquivalence (line 2714, Cmm_op_proofs.thy)
• Definition 6.1: definition sameLocWrites (line 331, Cmm_op.thy)
• Lemma 6.2: lemma step_mo_not_atomic_write (line 3995) and lemma step_mo_atomic_write (line 4013, Cmm_op_proofs.thy)
• Definition 6.3: definition exeAddToRfLoad (line 439, Cmm_op.thy)
• Definition 6.4: definition exeAddToRfRmw (line 470, Cmm_op.thy)
• Lemma 6.5: lemma step_rf_non_read (line 4136), lemma step_rf_load (line 4209) and lemma step_rf_rmw (line 4233, Cmm_op_proofs.thy)
• Definition 6.6: definition exeStep (line 599, Cmm_op.thy)
• Theorem 6.7: this theorem does not directly correspond to any theorem in the proof files. However, lemma exeConsistentEquivalence_aux (line 5131, Cmm_op_proofs.thy) states that incrementalConsistent is the same as executableConsistent, which is more or less the purpose of Theorem 6.7.
• Corollary 6.8: corollary exeConsistentEquivalence_as_in_submission (line 5143, Cmm_op_proofs.thy)