Safety Guarantees from Explicit Resource Management

David Aspinall, Patrick Maier, Ian Stark

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.
Original languageEnglish
Title of host publicationFormal Methods for Components and Objects
Subtitle of host publication6th International Symposium, FMCO 2007; Amsterdam, The Netherlands, October 24-26, 2007; Revised Lectures
PublisherSpringer
Pages52-71
Number of pages20
Volume5382
DOIs
Publication statusPublished - 2008
Event6th International Symposium on Formal Methods for Components and Objects - Amsterdam, Netherlands
Duration: 24 Oct 200726 Oct 2007

Publication series

NameLecture Notes in Computer Science
PublisherSpringer

Conference

Conference6th International Symposium on Formal Methods for Components and Objects
Abbreviated titleFMCO 2007
CountryNetherlands
CityAmsterdam
Period24/10/0726/10/07

Fingerprint

Managers
Codes (standards)

Cite this

Aspinall, D., Maier, P., & Stark, I. (2008). Safety Guarantees from Explicit Resource Management. In Formal Methods for Components and Objects: 6th International Symposium, FMCO 2007; Amsterdam, The Netherlands, October 24-26, 2007; Revised Lectures (Vol. 5382, pp. 52-71). (Lecture Notes in Computer Science). Springer. https://doi.org/10.1007/978-3-540-92188-2_3
Aspinall, David ; Maier, Patrick ; Stark, Ian. / Safety Guarantees from Explicit Resource Management. Formal Methods for Components and Objects: 6th International Symposium, FMCO 2007; Amsterdam, The Netherlands, October 24-26, 2007; Revised Lectures. Vol. 5382 Springer, 2008. pp. 52-71 (Lecture Notes in Computer Science).
@inproceedings{4309c511ce144249a5c616581fc87899,
title = "Safety Guarantees from Explicit Resource Management",
abstract = "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.",
author = "David Aspinall and Patrick Maier and Ian Stark",
year = "2008",
doi = "10.1007/978-3-540-92188-2_3",
language = "English",
volume = "5382",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "52--71",
booktitle = "Formal Methods for Components and Objects",

}

Aspinall, D, Maier, P & Stark, I 2008, Safety Guarantees from Explicit Resource Management. in Formal Methods for Components and Objects: 6th International Symposium, FMCO 2007; Amsterdam, The Netherlands, October 24-26, 2007; Revised Lectures. vol. 5382, Lecture Notes in Computer Science, Springer, pp. 52-71, 6th International Symposium on Formal Methods for Components and Objects, Amsterdam, Netherlands, 24/10/07. https://doi.org/10.1007/978-3-540-92188-2_3

Safety Guarantees from Explicit Resource Management. / Aspinall, David; Maier, Patrick; Stark, Ian.

Formal Methods for Components and Objects: 6th International Symposium, FMCO 2007; Amsterdam, The Netherlands, October 24-26, 2007; Revised Lectures. Vol. 5382 Springer, 2008. p. 52-71 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Safety Guarantees from Explicit Resource Management

AU - Aspinall, David

AU - Maier, Patrick

AU - Stark, Ian

PY - 2008

Y1 - 2008

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-540-92188-2_3

DO - 10.1007/978-3-540-92188-2_3

M3 - Conference contribution

VL - 5382

T3 - Lecture Notes in Computer Science

SP - 52

EP - 71

BT - Formal Methods for Components and Objects

PB - Springer

ER -

Aspinall D, Maier P, Stark I. Safety Guarantees from Explicit Resource Management. In Formal Methods for Components and Objects: 6th International Symposium, FMCO 2007; Amsterdam, The Netherlands, October 24-26, 2007; Revised Lectures. Vol. 5382. Springer. 2008. p. 52-71. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-540-92188-2_3