Verified Spilling And Translation Validation With Repair
INTERACTIVE THEOREM PROVING (ITP 2017)(2017)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络