Amortised resource analysis with separation logic

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

57 Downloads (Pure)

Abstract

Type-based amortised resource analysis following Hofmann and Jost—where resources are associated with individual elements of data structures and doled out to the programmer under a linear typing discipline—have been successful in providing concrete resource bounds for functional programs, with good support for inference. In this work we translate the idea of amortised resource analysis to imperative languages by embedding a logic of resources, based on Bunched Implications, within Separation Logic. The Separation Logic component allows us to assert the presence and shape of mutable data structures on the heap, while the resource component allows us to state the resources associated with each member of the structure. We present the logic on a small imperative language with procedures and mutable heap, based on Java bytecode. We have formalised the logic within the Coq proof assistant and extracted a certified verification condition generator. We demonstrate the logic on some examples, including proving termination of in-place list reversal on lists with cyclic tails.
Original languageEnglish
Title of host publicationProceedings of 19th European Symposium on Programming, ESOP 2010
EditorsAndrew Gordon
PublisherSpringer
Pages85-103
Volume6012
DOIs
Publication statusPublished - 2010

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume6012

Fingerprint

Data structures
Concretes

Keywords

  • separation logic
  • programming languages

Cite this

Atkey, R. (2010). Amortised resource analysis with separation logic. In A. Gordon (Ed.), Proceedings of 19th European Symposium on Programming, ESOP 2010 (Vol. 6012, pp. 85-103). (Lecture Notes in Computer Science; Vol. 6012). Springer. https://doi.org/10.1007/978-3-642-11957-6_6
Atkey, Robert. / Amortised resource analysis with separation logic. Proceedings of 19th European Symposium on Programming, ESOP 2010. editor / Andrew Gordon. Vol. 6012 Springer, 2010. pp. 85-103 (Lecture Notes in Computer Science).
@inproceedings{441e289c1963478d811e6f7dda74a9e5,
title = "Amortised resource analysis with separation logic",
abstract = "Type-based amortised resource analysis following Hofmann and Jost—where resources are associated with individual elements of data structures and doled out to the programmer under a linear typing discipline—have been successful in providing concrete resource bounds for functional programs, with good support for inference. In this work we translate the idea of amortised resource analysis to imperative languages by embedding a logic of resources, based on Bunched Implications, within Separation Logic. The Separation Logic component allows us to assert the presence and shape of mutable data structures on the heap, while the resource component allows us to state the resources associated with each member of the structure. We present the logic on a small imperative language with procedures and mutable heap, based on Java bytecode. We have formalised the logic within the Coq proof assistant and extracted a certified verification condition generator. We demonstrate the logic on some examples, including proving termination of in-place list reversal on lists with cyclic tails.",
keywords = "separation logic , programming languages",
author = "Robert Atkey",
year = "2010",
doi = "10.1007/978-3-642-11957-6_6",
language = "English",
volume = "6012",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "85--103",
editor = "Andrew Gordon",
booktitle = "Proceedings of 19th European Symposium on Programming, ESOP 2010",

}

Atkey, R 2010, Amortised resource analysis with separation logic. in A Gordon (ed.), Proceedings of 19th European Symposium on Programming, ESOP 2010. vol. 6012, Lecture Notes in Computer Science, vol. 6012, Springer, pp. 85-103. https://doi.org/10.1007/978-3-642-11957-6_6

Amortised resource analysis with separation logic. / Atkey, Robert.

Proceedings of 19th European Symposium on Programming, ESOP 2010. ed. / Andrew Gordon. Vol. 6012 Springer, 2010. p. 85-103 (Lecture Notes in Computer Science; Vol. 6012).

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

TY - GEN

T1 - Amortised resource analysis with separation logic

AU - Atkey, Robert

PY - 2010

Y1 - 2010

N2 - Type-based amortised resource analysis following Hofmann and Jost—where resources are associated with individual elements of data structures and doled out to the programmer under a linear typing discipline—have been successful in providing concrete resource bounds for functional programs, with good support for inference. In this work we translate the idea of amortised resource analysis to imperative languages by embedding a logic of resources, based on Bunched Implications, within Separation Logic. The Separation Logic component allows us to assert the presence and shape of mutable data structures on the heap, while the resource component allows us to state the resources associated with each member of the structure. We present the logic on a small imperative language with procedures and mutable heap, based on Java bytecode. We have formalised the logic within the Coq proof assistant and extracted a certified verification condition generator. We demonstrate the logic on some examples, including proving termination of in-place list reversal on lists with cyclic tails.

AB - Type-based amortised resource analysis following Hofmann and Jost—where resources are associated with individual elements of data structures and doled out to the programmer under a linear typing discipline—have been successful in providing concrete resource bounds for functional programs, with good support for inference. In this work we translate the idea of amortised resource analysis to imperative languages by embedding a logic of resources, based on Bunched Implications, within Separation Logic. The Separation Logic component allows us to assert the presence and shape of mutable data structures on the heap, while the resource component allows us to state the resources associated with each member of the structure. We present the logic on a small imperative language with procedures and mutable heap, based on Java bytecode. We have formalised the logic within the Coq proof assistant and extracted a certified verification condition generator. We demonstrate the logic on some examples, including proving termination of in-place list reversal on lists with cyclic tails.

KW - separation logic

KW - programming languages

UR - http://www.springerlink.com/content/x626l080j8037147/

UR - http://personal.cis.strath.ac.uk/~raa/amortised-sep-logic.html

U2 - 10.1007/978-3-642-11957-6_6

DO - 10.1007/978-3-642-11957-6_6

M3 - Conference contribution book

VL - 6012

T3 - Lecture Notes in Computer Science

SP - 85

EP - 103

BT - Proceedings of 19th European Symposium on Programming, ESOP 2010

A2 - Gordon, Andrew

PB - Springer

ER -

Atkey R. Amortised resource analysis with separation logic. In Gordon A, editor, Proceedings of 19th European Symposium on Programming, ESOP 2010. Vol. 6012. Springer. 2010. p. 85-103. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-11957-6_6