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)