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.

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.

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.

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.

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.
- Invariant parameter: invariant for shared state;
- Step invariant: step invariant that holds at every simulation step;
- Rely condition: rely condition;
- 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.

- 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.
- Correct Optimizer: The correctness of an optimizer (Definition 6.4 in paper);
- 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.
- 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).

- CorrectOpt.v: The top-level theorem shows the soundness of our verification framework. This file has the following main contents.

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 |

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

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

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

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

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

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