Closure conversion is safe for space
Closure conversion is safe for space
复制标题
闭合转换对于空间来说是安全的
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
A. Appel
中科院分区：
文献类型：
--
作者：
Zoe Paraskevopoulou;A. Appel
我们正式证明 CPS lambda 演算的平坦环境的闭包转换是正确的（保留语义）并且对于时间和空间来说是安全的，这意味着生成的代码保留了源程序执行所需的时间和空间。我们通过形式化分析语义来为闭包转换前和闭包后的代码提供一个成本模型，这些语义跟踪程序执行所需的时间和空间资源，并考虑垃圾收集。为了显示时间和空间的保存，我们建立了一个通用的“垃圾收集兼容”的二元逻辑关系，该关系建立了相关程序的资源消耗的不变量以及功能的正确性。使用这个框架，我们展示了终止源程序的语义保留和空间和时间安全性，以及发散源程序的发散保留和空间安全性。我们正式证明 CPS lambda 演算的平坦环境的闭包转换是正确的（保留语义）并且对于时间和空间来说是安全的，这意味着生成的代码保留了源程序执行所需的时间和空间。我们通过形式化分析语义来为闭包转换前和闭包后的代码提供一个成本模型，这些语义跟踪程序执行所需的时间和空间资源，并考虑垃圾收集。为了显示时间和空间的保存，我们建立了一个通用的“垃圾收集兼容”的二元逻辑关系，该关系建立了相关程序的资源消耗的不变量以及功能的正确性。使用这个框架，我们展示了终止源程序的语义保留和空间和时间安全性，以及发散源程序的发散保留和空间安全性。这是闭包转换的空间安全性的第一个正式证明。转换和证明是 CertiCoq 编译器管道的一部分，从 Coq (Gallina) 通过 CompCert Clight 到汇编语言。我们的结果在 Coq 证明助手中被机械化。
We formally prove that closure conversion with flat environments for CPS lambda calculus is correct (preserves semantics) and safe for time and space, meaning that produced code preserves the time and space required for the execution of the source program. We give a cost model to pre- and post-closure-conversion code by formalizing profiling semantics that keep track of the time and space resources needed for the execution of a program, taking garbage collection into account. To show preservation of time and space we set up a general, "garbage-collection compatible", binary logical relation that establishes invariants on resource consumption of the related programs, along with functional correctness. Using this framework, we show semantics preservation and space and time safety for terminating source programs, and divergence preservation and space safety for diverging source programs. We formally prove that closure conversion with flat environments for CPS lambda calculus is correct (preserves semantics) and safe for time and space, meaning that produced code preserves the time and space required for the execution of the source program. We give a cost model to pre- and post-closure-conversion code by formalizing profiling semantics that keep track of the time and space resources needed for the execution of a program, taking garbage collection into account. To show preservation of time and space we set up a general, "garbage-collection compatible", binary logical relation that establishes invariants on resource consumption of the related programs, along with functional correctness. Using this framework, we show semantics preservation and space and time safety for terminating source programs, and divergence preservation and space safety for diverging source programs. This is the first formal proof of space-safety of a closure-conversion transformation. The transformation and the proof are parts of the CertiCoq compiler pipeline from Coq (Gallina) through CompCert Clight to assembly language. Our results are mechanized in the Coq proof assistant.