Verifying Optimizations of Concurrent Programs in the Promising Semantics

This is the mechanized proof of "Verifying Optimizations for Concurrent Programs in the Promising Semantics 2.1" in the Coq proof assistent.
Below we list contents of the mechanized proof. All mechanized proofs are under src/ subdirectory.


Promising semantics (PS2.1)

contains the definition of promising semantics 2.1 (PS2.1) and its corresponding properties.

Non-preemptive semantics

contains the definition of the non-preemptive semantics (Section 4 in paper).

CSimplRTL language

the syntax and semantics of concurrent programming language CSimplRTL introduced in Section 3 in paper.


the definitions of the thread-local upward simulation (in Section 6 in paper) and the whole program simulation.


Verified Optimizations

four verified common optimizations: constant propagation (ConstProp), dead code elimination (DCE), common subexpression elimination (CSE), loop invariant code motion (LICM).

Optimizer Analyzer in Opt Translation in Opt Correctness Proof
ConstProp Value Analysis (ValAnalysis.v) ConstProp.v ConstPropProof.v
DCE Liveness Analysis (LiveAnalysis.v) DCE.v DCEProof.v
CSE Available expression analysis (AveAnalysis.v) CSE.v CSEProof.v
LICM Detecting Loop Invariants (DetLoop.v) LICM.v LICMProof.v

Theorems, lemmas and definitions referenced in paper

We list the relevant theorems, lemmas and definitions mentioned in the paper by section.

Section 3

Paper Coq file Coq_name (related name in paper)
Syntax of the CSimpRTL language (Fig. 7) Syntax.v Inst (Instr), BBlock (BBlock), CodeHeap (Cdhp), Func (Code), Code (Prog)
Machine states and events (Fig. 8) Memory.v, Thread.v, Configuration.v, Local.v, Event.v, Behavior.v Memory.t (Mem), Thread.t (ThrdState), Configuration.t (World), ThreadEvent.t (ThrdEvt), MachineEvent.t (ProgEvt), conf_behaviors (EvtTrace)
Interleaving machine steps (Fig. 9) Configuration.v Configuration.init (init), Configuration.step (*-step and t-term), Configuration.abort_config (abort), Configuration.is_done (prog-done)
Event trace refinement and equivalence Behavior.v evttr_refinement (event trace refinement), evttr_equivalence (event trace equivalence)

Section 4

Paper Coq file Coq_name (related name in paper)
Non-preemptive semantics rules (Fig. 10) NPThread.v, NPConfiguration.v NPThread, NPConfiguration.t (NPWorld), NPConfiguration.step
Semantics Equivalence (Thm 4.1) SemaEq.v sema_eq_ps_nps (Thm. 4.1)

Section 5

Paper Coq file Coq_name (related name in paper)
Write-write race freedom in PS2.1 (ww-RF in Fig. 11) ww_RF.v ww_rf (ww-RF in Fig. 11)
Write-write race freedom in the non-preemptive semantics ww_RF.v ww_rf_np (ww-NPRF)
ww-RF Equivalence (Lm. 5.1) wwRFEq.v ww_RF_eq (Lm. 5.1)

Section 6

Paper Coq file Coq_name (related name in paper)
Well-formed timestamp mapping MsgMapping.v weak_MsgInj
Invariant parameter (Inv in Fig. 12) LocalSim.v Invariant(Inv in Fig. 12)
Rely condition LocalSim.v Rely
Delayed write set (Fig. 13) DelayedSet.v DelaySet (DlySet)
Step invariant Step invariant SI
Thread-local upward simulation (Def. 6.1) LocalSim.v local_sim (Def. 6.1), local_sim_state
Safe program in PS2.1 Configuration.v (Safe)
Safe program in the non-preemptive semantics NPConfiguration.v (Safe)
Whole program simulation GlobSim.v glob_sim
Compositionality and ww-RF Preservation (Lm. 6.2) Compositionality.v, wwRFPrsv.v compositionality and ww_RF_preservation (Lm. 6.2)
Correctness of optimizer (Def. 6.4) CorrectOpt.v Correct (Def. 6.4)
Optimization correctness theorem (Thm. 6.5) CorrectOpt.v Verif_implies_Correctness (Thm. 6.5)
Correct Optimizers (Thm. 6.6) VerifiedOpt.v Correct_optimizers (Thm. 6.6)

Section 7

Paper Coq file Coq_name (related name in paper)
I_dce (invariant in DCE proof) DCEProofMState.v I_dce
DCE is verified DCEProof.v verif_dce (Lm. 7.1)