CASCompCert

The results related to our paper reside in concurrency/ subdirectory, others are CompCert-3.0.1 files required by our formalization. Below we list contents of concurrency/.

Top-level files

• framework/Soundness.v The framework final theorem (Theorem 12)
• FinalTheorem.v CompCert correctness with x86-SC backend and object modules (Theorem 14).
• x86TSO/FinalTheoremExt.v Correctness with x86-TSO backend and object modules (Theorem 15).

Verification framework

• common/
  general definitions, e.g. abstract languages, global semantics, DRF, etc..

  • Footprint.v Footprint Definition
  • GMemory.v Global memory instantiation
  • InteractionSemantics.v The abstract module-local semantics, including the definition of “well-defined language” (Def. 1)
  • GAST.v, GlobDefs.v, GlobSemantics.v Preemptive global semantics (see Fig. 7)
  • ETrace.v Event trace definition
  • DRF.v Definition of DRF (see Fig. 9 and Sec. 5)
  • ReachClose.v Reach-close (Def. 4)
  • Injections, LDSimDefs.v Definitions of footprint matching and rely/guarantee conditions (Fig. 8).
  • LDSim.v Module local simulation (see Def. 2, 3).
  • SeqCorrect.v Definition of Sequential compiler correctness (Def. 10)

• framework/
  the verification framework

  • NPDefs/NPSemantics.v Non-preemptive global semantics (see Fig. 7)
  • NPDefs/NPDRF.v Definition of NPDRF (see Sec. 5)
  • NPDefs/NPEquiv.v Equivalence between DRF and NPDRF
  • NPDefs/RefineEquiv.v Equivalence between preemptive and non-preemptive semantics of DRF programs (Lemma 9)
  • GlobUSim/GlobUSim.v, GlobUSim/GlobUSimRefine.v Global upward simulation and the proofs of the Soundness Lemma (Lemma 7)
  • GlobDSim/GlobDSim.v, GlobDSim/Flipping.v Global downward simulation and the proofs of the Flip Lemma
  • Compositionality/Compositionality.v Proofs of Compositionality (Lemma 6)

CompCert verification

• comp_correct/ CompCert verification

  • ClightLang.v, AsmLang.v, SpecLang.v Clight, x86-SC, and CImp language instantiations
  • ClightWD.v, AsmWD.v, SpecLangWDDET.v Proofs showing that Clight, x86-SC, CImp languages are well-defined
  • AsmDET.v, SpecLangWDDET.v Proofs showing that x86-SC and CImp are deterministic
  • localize/Localize.v Lifting lemmas for reusing CompCert's proofs
  • localize/LDSim_local_transitive.v Transitivity of the CompCert memory based simulation
  • SpecLangIDTrans.v Correctness of the identity transformation of CImp modules
  • CompCorrect.v The adapted CompCert compiler and its correctness proof (Lemma 13)
  • cfrontend/ and backend/: Instantiations of the intermediate languages (*_local.v) and proved individual compilation passes. Below are tables of the intermediate language instantiations and proved passes.

  Intermediate Languages	Instantiation
  CSharpminor	Csharpminor_local.v
  Cminor	Cminor_local.v
  RTL	RTL_local.v
  LTL	LTL_local.v
  Linear	Linear_local.v
  Mach	Mach_local.v

  Pass	Compiler code	Correctness Proof
  Cshmgen	cshmgen.v	cshmgen_proof.v
  Cminorgen	cminorgen.v	cminorgenproof.v
  Selection	selection.v	selection_proof.v
  RTLgen	rtlgen.v	rtlgen_proof.v
  Tailcall	tailcall.v	tailcall_proof.v
  Renumber	renumber.v	renumber_proof.v
  Allocation	allocation.v	alloc_proof.v
  Tunneling	tunneling.v	tunneling_proof.v
  Linearize	linearize.v	linearize_proof.v
  CleanupLabels	cleanuplabels.v	cleanuplabels_proof.v
  Stacking	stacking.v	stacking_proof.v
  Asmgen	asmgen.v	asmgen_proof.v

Extended framework

• x86TSO/

  • AsmTSO.v The x86-TSO language instantiations
  • ObjectSim.v Object simulation
  • TSOCompositionality.v Proof of Lemma 16 (Restore SC semantics for DRF x86 programs)
  • lock_proof/ An efficient spin-lock implementation (code.v) with its correctness proof (LockProof.v)