Spilling is a mandatory translation phase in every compiler back-end. It decides whether and where a value is stored in a register or in memory and has therefore a significant impact on performance. In this paper, we study spilling in the setting of a verified compiler with a term-based intermediate representation that provides an alternative way to realize SSA. We devise a permissive correctness criterion to accommodate many SSA-based spilling algorithms and prove the criterion sound. As case study, we verify two basic spilling algorithms. Finally, we show that our criterion is decidable by deriving a translation validator that repairs spilling information if necessary. We show that the validator always produces a valid spilling, and that the validator does not alter valid spilling information. Our results are formalized in Coq as part of the LVC compiler project.
Download PDF Show BibTeX
Login to edit