Julian Tobias Rosemann: Bachelor's Thesis
Formal Verification of a Family of Spilling Algorithms
Advisor: Sigurd Schneider
Abstract:
Spilling is an important translation phase mandatory in every compiler backend. Spilling translates a program with unbounded maximal live sets to a program where the variables are partitioned into an unbounded set (memory) and a set bounded by an integer k (registers). Additionally spilling must ensure that the variables used at a program point are in the register set at that program point. For any program there are different ways to achieve the bound, and the choice greatly impacts performance.
In this thesis we develop a permissive correctness criterion designed to accommodate many spilling choices. If a spilling satisfies our criterion the register partition satisfies the register bound, all variables are in the registers when they are used and program equivalence is preserved.
As case study we verify two spilling algorithms. The first is a trivial one where variables are loaded from the memory before any usage and the whole register set is spilled to the memory after every instruction. The second tries to minimize the spills and loads by remembering which variables are in the registers and in the memory.
References

Compilers: Principles, Technique, and Tools (2nd Edition) (2006)
Alfred V. Aho et al.

A study of replacement algorithms for a virtualstorage computer (1996)
Labslo A. Belady

Formal Verification of Coalescing GraphColoring Register Allocation (2010)
Sandrine Blazy, Benoit Robillard, and Andrew W. Appel

On the complexity of register coalescing (2007)
Florent Bouchez, Alain Darte, and Fabrice Rastello

On the Complexity of Spill Everywhere
Under SSA Form (2007)
Florent Bouchez, Alain Darte, and Fabrice Rastello

Register spilling and liverange splitting for SSAform
programs (2009)
Matthias Braun and Sebastian Hack

Register allocation via graph coloring (1992)
Preston Briggs

Improvements to graph coloring register
allocation (1994)
Preston Briggs, Keith D Cooper, and Linda Torczon

Register allocation via hierarchical graph coloring (1991)
David Callahan and Brian Koblenz

Register allocation via coloring (1981)
Gregory J Chaitin

Register allocation by prioritybased coloring (1984)
Frederick Chow and John Hennessy

Iterated register coalescing (1996)
Lal George and Andrew W Appel

Register Allocation for Programs in SSAForm (2006)
Sebastian Hack, Daniel Grund, and Gerhard Goos

Towards Register Allocation for Programs in
SSAForm (2005)
Sebastian Hack, Daniel Grund, and Gerhard Goos

Closing the Gap  The Formally Verified Optimizing Compiler CompCert (2017)
Daniel Kaestner et al.

Verification of Spilling Algorithms in Coq (2015)
Patrick Klitzke

A Formally Verified Compiler Backend (2009)
Xavier Leroy

Linear scan register allocation (1999)
Massimiliano Poletto and Vivek Sarkar

Validating register allocation and spilling (2010)
Silvain Rideau and Xavier Leroy

A Linear FirstOrder Functional Intermediate
Language for Verified Compilers (2015)
Sigurd Schneider, Gert Smolka, and Sebastian Hack

An Inductive Proof Method for Simulation
based Compiler Correctness (2016)
Sigurd Schneider, Gert Smolka, and Sebastian Hack

A New Verified Compiler Backend for CakeML (2016)
Yong Kiam Tan et al.

Quality and Speed in Linearscan Register
Allocation (1998)
Omri Traub, Glenn Holloway, and Michael D. Smith

Linear scan register allocation on SSA form (2010)
Christian Wimmer and Michael Franz

Finding and Understanding Bugs in C Compilers (2011)
Xuejun Yang et al.
Thesis
Presentations
 Initial Seminar Talk: Slides (June 10, 2016)
 Second Seminar Talk: Slides (November 4, 2016)
 Final Talk: Slides (February 24, 2017)
Formalization
The formalization in Coq is available: CoqDoc
Julian Tobias Rosemann,
Sun Feb 26 15:57:05 2017