Abstract
Liveness analysis is a standard compiler analysis, enabling several optimizations such as deadcode elimination. The SSA form is a popular compiler intermediate language allowing for simple and fast optimizations. Boissinot et al. [7] designed a fast liveness analysis by combining the specific properties of SSA with graph-theoretic ideas such as depth-first search and dominance. We formalize their approach in the Coq proof assistant, inside the CompCertSSA verified C compiler. We also compare experimentally this approach on CompCert’s benchmarks with respect to the classic data-flow-based liveness analysis, and observe performance gains.
Author supplied keywords
Cite
CITATION STYLE
Léchenet, J. C., Blazy, S., & Pichardie, D. (2020). A Fast Verified Liveness Analysis in SSA Form. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12167 LNAI, pp. 324–340). Springer. https://doi.org/10.1007/978-3-030-51054-1_19
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
