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.

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.

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 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)