Verification of Spilling Algorithms
This is the Coq development accompanying our submission to ITP 2017. Coq sources are available for download. The development is a part of the LVC verified compiler. In previous work, we introduced LVC's intermediate language IL, a first-order language with system calls. IL has two semantics, which interpret variables differently, as binders or as assignables. Using a correspondence between the two semantic interpretations, IL in the binder representation realizes term-based static single assignment (SSA).
This development focuses on the verification of spilling in LVC. The implementation of spilling is based on annotations on the program that indicate at each program point the values of which variables should be spilled and the values of which variables should be loaded. On these annotations, we inductively define a correctness predicate for spilling. We then show that the predicate is sound, i.e. that every spilling annotation leads to a program that
- meets the register bound
- keeps values of variables in registers where required by an instruction
- is semantically equivalent to the original program in a certain sense
To show a spilling algorithm correct, it now suffices to show that all annotations it produces satisfy the predicate. We verify two spilling algoithms using our predicate. The first algorithm produces a trivial spilling, that maintains the invariant that all values are kept in spill slots. The algorithm inserts the neccessary loads and spills to ensure register availability if required by an instruction. The correctness proof of the algorithm is short. The second algorithm is a little bit more clever, and only spills and reloads when required by register pressure, but makes no effort to avoid spilling and reloading inside loops. The decision which variables are overwritten at any given program point is outsourced to an oracle with only trivial correctness requirements and thus any heuristic can be used with little proof effort. The correctness proof is still compact.
Finally, we exploit that our correctness predicate is decidable, and give a translation validator. The translation validator has a twist: It is able to repair incorrect spilling information in a non-invasive way. We show two theorems about our translation validator. First, that every spilling it produces is correct. This means that the translation validator is effectively a spilling algorithm. And second, that the translation validator does not alter correct spillings. This is the translation validation part of the algorithm. The translation validator tries to remain as faithful as possible to original spilling.