Imperial College London > Talks@ee.imperial > CAS Talks > Mechanised Semantics for Gated Static Single Assignment

Mechanised Semantics for Gated Static Single Assignment

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact George A Constantinides.

The Gated Static Single Assignment (GSA) form has been proposed by Ottenstein et al. in 1990, as an intermediate representation for implementing advanced static analysis and optimisation passes in compilers. Compared to SSA , GSA additionally records data and control dependencies. GSA has been used in various practical, challenging contexts, such as parallelising optimisers, high-level synthesis, or code generation for GPUs.

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 talk I'll present our formalisation of the syntax and
semantics of GSA which are implemented in CompCert, and will also
describe how GSA could possibly be used to implement a formally
verified dynamically scheduled high-level synthesis tool.

This talk is part of the CAS Talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Changes to Talks@imperial | Privacy and Publicity