On Friday October 17, this site was moved to a new server, https://mw.hh.se. The original address will continue to work. Whithin a week or two this site will return to the original address. /Peo HH IT-dep

WG211/M21Blazy: Difference between revisions

From WG 2.11
Jump to navigationJump to search
VisualWikitext
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,..."
 
No edit summary
 
Line 1: Line 1:
Static Single Assignment (SSA) has proven useful for implementing
Static Single Assignment (SSA) has proven useful for implementing
  many static-analysis and optimisation passes, thanks to its
many static-analysis and optimisation passes, thanks to its
  structural and semantic properties. However, SSA phi-instructions
structural and semantic properties. However, SSA phi-instructions
  depend on control-flow, whereas many advanced analysis passes are
depend on control-flow, whereas many advanced analysis passes are
  data-flow dependent, limiting these inherently.  One
data-flow dependent, limiting these inherently.  One
  solution is to use a richer intermediate representation, namely
solution is to use a richer intermediate representation, namely
  Gated-SSA, which partially transforms control-flow dependencies into
Gated-SSA, which partially transforms control-flow dependencies into
  data-dependencies, and encode enough information to make the
data-dependencies, and encode enough information to make the
  semantics of phi-instructions independent of
semantics of phi-instructions independent of
  control-flow. Gated-SSA has been successfully applied in various
control-flow. Gated-SSA has been successfully applied in various
  practical contexts of optimising compilation, and yet, no reference
practical contexts of optimising compilation, and yet, no reference
  implementation or semantics have been described in the literature.
implementation or semantics have been described in the literature.


  In this talk, we formulate an operational semantics for Gated-SSA.
In this talk, we formulate an operational semantics for Gated-SSA.
  We also provide a formal specification of a translation from SSA to
We also provide a formal specification of a translation from SSA to
  Gated-SSA, and we prove it is semantics preserving. To demonstrate
Gated-SSA, and we prove it is semantics preserving. To demonstrate
  the practicality of our approach, we implement this specification as
the practicality of our approach, we implement this specification as
  a translation pass within the CompCertSSA compiler, which is
a translation pass within the CompCertSSA compiler, which is
  formally verified in Coq.
formally verified in Coq.

Latest revision as of 11: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.

Retrieved from "http://mw.hh.se/wg211/index.php?title=WG211/M21Blazy&oldid=2249"