Mechanised Semantics for Gated Static Single Assignment
summary
Provides a formal, mechanised semantics for Gated Static Single Assignment mechanised in Coq and clarifies the role of gamma and eta gates with a control-flow-insensitive semantic for gate predicates. Specifies and proves a semantics-preserving translation SSA→GSA and embeds it as a validated transformation in CompCertSSA. Uses smtcoq and Verit to discharge local predicate coherence checks (three-valued logic), notes current limitations: predicates cannot depend on memory (pointer tests) and SMT validation is currently slow.
AI-written summary · about
chapters (12)
- 0:00SSA introduction and limits
- 2:10Phi instruction weaknesses
- 3:15Gated SSA solution
- 5:24Formalizing gated SSA semantics
- 6:29SSA to GSA translation example
- 8:39Generating gamma predicates
- 10:48Validating predicates locally
- 12:34Predicate generation details
- 14:43Coherence proofs with SMT
- 18:20Summary and limitations
- 19:44Future work challenges
- 20:50Q&A
related talks
26mSSA Translation Is an Abstract Interpretation
18mSSA is Freyd Categories
15mTowards a Coq Specification for Generalized Algebraic Datatypes in OCaml
24mTowards a Higher-Order Mathematical Operational Semantics
25mA Semantic Approach to Robust Property Preservation
30mSemantics-Guided Synthesis
27mSM-based Semantics for Answer Set Programs Containing Conditional Literals and Arithmetic
36mSound and Complete Refinement for SSA with Substructural Effects