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.

---

Structure

Promising semantics (PS2.1)

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

• promising/lang
  the definition of promising semantics 2.1 (PS2.1). Below, we list the Coq implementation of some important components in PS2.1.
  • Memory.v: Memory in PS2.1. The memory in PS2.1 is a message pool (in Figure 8 in paper).
  • Thread.v: Thread steps in PS2.1 (in Figure 8 in paper).
  • Configuration.v: Program steps (or machine steps) in promising semantics (in Figure 8 in paper). It also contains the definition of the program configuration (or machine states in Figure 5 in paper).
  • Behavior.v: behaviors of program in promising semantics.
• promising/prop
  some properties about PS2.1.
• promising/wwrf
  the definition of the write-write race freedom.
  • ww_RF.v: Write-write race freedom in PS2.1, which is defined in Figure 11 in paper. We also define the write-write race freedom in the non-preemptive semantics in this file.

Non-preemptive semantics

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

• NPThread.v: thread steps in the non-preemptive semantics (in Figure 10 in paper).
• NPConfiguration.v: Program steps (or machine steps) in the non-preemptive semantics (in Figure 10 in paper).
• NPBehavior.v: behaviors of the program in the non-preemptive semantics.

CSimplRTL language

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

• Syntax.v: Syntax of CSimplRTL language (in Figure 8 in paper).
• Semantics.v: Semantics of CSimplRTL language (or transition on the thread-local state), whose definition is omitted in paper.

Simulation

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

• DelayedSet.v: Delayed write set and some operations about delayed write set (in Figure 13 in paper).
• MsgMapping.v: Timestamp mapping (defined as TMap) in Figure 12 in paper).
• LocalSim.v: Thread-local upward simulation. It covers the most of the definitions in Section 6 in paper.
  1. Invariant parameter: invariant for shared state;
  2. Step invariant: step invariant that holds at every simulation step;
  3. Rely condition: rely condition;
  4. Thread-local simulation: thread-local upward simulation (Definition 6.1 in paper);
• GlobSim.v: whole program simulation (or global simulation). The theorem glob_sim_implies_refinement in this file shows that, if the whole target and source programs are simulated, they have refinement relation, and corresponds to the step (4) in Figure 6 (Our proof path) in paper.

Proofs

• src/proofs
  contains most of the proofs of the soundness proof of our verification framework shown in Figure 6 (Our proof path) in paper.
  • src/proofs/general-prop: general lemmas in soundness proof.
  • src/proofs/ps-np-equivalence:
    contains the proof of the semantics equivalence of PS2.1 and the non-preemptive semantics, and the equivalence of the write-write race freedoms in PS2.1 and the non-preemptive semantics. Below we list the main results.
    • SemaEq.v: The semantics equivalence (Theorem 4.1 in paper) proof of the promising semantics 2.1 (PS2.1) and the non-preemptive semantics. Theorem sema_eq_ps_nps in this file is the top-level theorem to show semantics equivalence and corresponds to the step (5) in Figure 6 (Our proof path) in paper.
    • wwRFEq.v: The proof of the equivalence of the write-write race freedoms (Lemma 5.1 in paper) in PS2.1 and the non-preemptive semantics. Theorem ww_RF_eq in this file is the top-level theorem to the write-write race freedom equivalence and corresponds to the step (1) in Figure 6 (Our proof path) in paper.
  • src/proofs/sim-compositionality and src/proofs/wwRF-preservation:
    contains the proof of Lemma 6.2 (Compositionality and ww-RF Preserving) in paper. It corresponds to the step (3) in Figure 6 (Our proof path) in paper. In the Coq proof, we divide the proof of Lemma 6.2 (Compositionality and ww-RF Preserving) in paper into two lemmas: compositionality and write-write race freedom preservation.
    • Compositionality.v: Thread-local upward simulation is compositional. Theorem compositionality in this file is the top-level theorem to show such conclusion.
    • wwRFPrsv.v: thread-local upward simulation is able to preserve write-write race freedom in the source program. The theorem ww_RF_preservation in this file is the top-level theorem to show such conclusion.
• src/result
  • CorrectOpt.v: The top-level theorem shows the soundness of our verification framework. This file has the following main contents.
    1. Correct Optimizer: The correctness of an optimizer (Definition 6.4 in paper);
    2. Verified Optimizer: An optimizer is verified (Definition 6.3 in paper), if we can always establish the thread-local simulation between the target and source code.
    3. Verified Optimizer is correct: An optimizer is correct if it is verified (Theorem 6.5 in paper). It is the top-level proof of the soundness proof of our verification framework and includes the proof of the step (2) in Figure 6 (Our proof path).

Verified Optimizations

src/rtl/optimizer
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	Configuration.safe (Safe)
Safe program in the non-preemptive semantics	NPConfiguration.v	NPConfiguration.safe (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)