Francalanza, Adrian and DeVries, Edsko and Hennessy, Matthew - Compositional Reasoning for Explicit Resource Management in Channel-Based Concurrency

lmcs:691 - Logical Methods in Computer Science, June 26, 2014, Volume 10, Issue 2
Compositional Reasoning for Explicit Resource Management in Channel-Based Concurrency

Authors: Francalanza, Adrian and DeVries, Edsko and Hennessy, Matthew

We define a pi-calculus variant with a costed semantics where channels are treated as resources that must explicitly be allocated before they are used and can be deallocated when no longer required. We use a substructural type system tracking permission transfer to construct coinductive proof techniques for comparing behaviour and resource usage efficiency of concurrent processes. We establish full abstraction results between our coinductive definitions and a contextual behavioural preorder describing a notion of process efficiency w.r.t. its management of resources. We also justify these definitions and respective proof techniques through numerous examples and a case study comparing two concurrent implementations of an extensible buffer.


Source : oai:arXiv.org:1405.6100
DOI : 10.2168/LMCS-10(2:15)2014
Volume: Volume 10, Issue 2
Published on: June 26, 2014
Submitted on: November 28, 2012
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 123 times.
This article's PDF has been downloaded 28 times.