Julian Tobias Rosemann: Bachelor's Thesis

Saarland University Computer Science

Formal Verification of a Family of Spilling Algorithms

Advisor: Sigurd Schneider


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.





The formalization in Coq is available: CoqDoc

Julian Tobias Rosemann, Sun Feb 26 15:57:05 2017