Julian Tobias Rosemann: Bachelor's Thesis

Programming Systems

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 back-end. 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 virtual-storage computer (1996)
  Labslo A. Belady
• Formal Verification of Coalescing Graph-Coloring 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 live-range splitting for SSA-form 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 priority-based coloring (1984)
  Frederick Chow and John Hennessy
• Iterated register coalescing (1996)
  Lal George and Andrew W Appel
• Register Allocation for Programs in SSA-Form (2006)
  Sebastian Hack, Daniel Grund, and Gerhard Goos
• Towards Register Allocation for Programs in SSA-Form (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 Back-end (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 First-Order 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 Linear-scan 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

• Bachelor Thesis: Formal Verification of Spilling Algorithms (February 1, 2017)

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