Safety Guarantees from Explicit Resource Management
Safety Guarantees from Explicit Resource Management
复制标题
显式资源管理的安全保证
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
I. Stark
中科院分区：
文献类型：
--
作者：
David Aspinall;Patrick Maier;I. Stark
我们提出一种语言和程序分析，该语言可以证明灵活资源管理成语的安全使用，尤其是预订或昂贵资源的“块预订”。这是基于以前的资源经理进行运行时安全检查的工作，通过展示如何通过编译时间检查来帮助这些检查。我们将提供一种小型的ANF风格语言，并具有明确的资源经理，并引入一种捕获其运行时行为的类型和效果系统。在这种情况下，我们确定了运行代码的动态安全性概念，并证明可以在没有运行时检查的情况下执行动态安全的代码。我们为类型安全代码展示了类似的静态安全属性，并证明静态安全意味着动态安全性。结果是可以在没有运行时仪器的情况下执行打字的代码，并保证只能适当使用资源。
We present a language and a program analysis that certifies the safe use of flexible resource management idioms, in particular advance reservation or "block booking" of costly resources. This builds on previous work with resource managers that carry out runtime safety checks, by showing how to assist these with compile-time checks. We give a small ANF-style language with explicit resource managers, and introduce a type and effect system that captures their runtime behaviour. In this setting, we identify a notion of dynamic safety for running code, and show that dynamically safe code may be executed without runtime checks. We show a similar static safety property for type-safe code, and prove that static safety implies dynamic safety. The consequence is that typechecked code can be executed without runtime instrumentation, and is guaranteed to make only appropriate use of resources.