Mon 16 Jan 2023 10:08 - 10:30 at Studio 1 - CompCert and Beyond Chair(s): Steve Zdancewic

The Gated Static Single Assignment (GSA) form was proposed by Ottenstein et al. in 1990, as an intermediate representation for implementing advanced static analyses and optimisation passes in compilers. Compared to SSA, GSA records additional data dependencies and provides more context, making optimisations more effective and allowing one to reason about programs as data-flow graphs.

Many practical implementations have been proposed that follow, more or less faithfully, Ottenstein et al.’s seminal paper. But many discrepancies remain between these, depending on the kind of dependencies they are supposed to track and to leverage in analyses and code optimisations.

In this paper, we present a formal semantics for GSA, mechanised in Coq. In particular, we clarify the nature and the purpose of gates in GSA, and define control-flow insensitive semantics for them. We provide a specification that can be used as a reference description for GSA. We also specify a translation from SSA to GSA and prove that this specification is semantics-preserving. We demonstrate that the approach is practical by implementing the specification as a validated translation within the CompCertSSA verified compiler.

Mon 16 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:30
CompCert and BeyondCPP at Studio 1
Chair(s): Steve Zdancewic University of Pennsylvania
CompCert: a journey through the landscape of mechanized semantics for verified compilation
K: Sandrine Blazy University of Rennes; Inria; CNRS; IRISA
Mechanised Semantics for Gated Static Single Assignment
Yann Herklotz Imperial College London, Delphine Demange Univ Rennes, Inria, CNRS, IRISA, Sandrine Blazy University of Rennes; Inria; CNRS; IRISA
DOI Pre-print