Difference between revisions of "WG211/M21Blazy"
(Created page with " Static Single Assignment (SSA) has proven useful for implementing many static-analysis and optimisation passes, thanks to its structural and semantic properties. However,...") |
|||
| Line 1: | Line 1: | ||
| − | + | Static Single Assignment (SSA) has proven useful for implementing | |
| − | + | many static-analysis and optimisation passes, thanks to its | |
| − | + | structural and semantic properties. However, SSA phi-instructions | |
| − | + | depend on control-flow, whereas many advanced analysis passes are | |
| − | + | data-flow dependent, limiting these inherently. One | |
| − | + | solution is to use a richer intermediate representation, namely | |
| − | + | Gated-SSA, which partially transforms control-flow dependencies into | |
| − | + | data-dependencies, and encode enough information to make the | |
| − | + | semantics of phi-instructions independent of | |
| − | + | control-flow. Gated-SSA has been successfully applied in various | |
| − | + | practical contexts of optimising compilation, and yet, no reference | |
| − | + | implementation or semantics have been described in the literature. | |
| − | + | In this talk, we formulate an operational semantics for Gated-SSA. | |
| − | + | We also provide a formal specification of a translation from SSA to | |
| − | + | Gated-SSA, and we prove it is semantics preserving. To demonstrate | |
| − | + | the practicality of our approach, we implement this specification as | |
| − | + | a translation pass within the CompCertSSA compiler, which is | |
| − | + | formally verified in Coq. | |
Latest revision as of 10:17, 2 August 2022
Static Single Assignment (SSA) has proven useful for implementing many static-analysis and optimisation passes, thanks to its structural and semantic properties. However, SSA phi-instructions depend on control-flow, whereas many advanced analysis passes are data-flow dependent, limiting these inherently. One solution is to use a richer intermediate representation, namely Gated-SSA, which partially transforms control-flow dependencies into data-dependencies, and encode enough information to make the semantics of phi-instructions independent of control-flow. Gated-SSA has been successfully applied in various practical contexts of optimising compilation, and yet, no reference implementation or semantics have been described in the literature.
In this talk, we formulate an operational semantics for Gated-SSA. We also provide a formal specification of a translation from SSA to Gated-SSA, and we prove it is semantics preserving. To demonstrate the practicality of our approach, we implement this specification as a translation pass within the CompCertSSA compiler, which is formally verified in Coq.
