Please use this identifier to cite or link to this item:
Title: Compositional reasoning for explicit resource management in channel-based concurrency
Authors: Francalanza, Adrian
Devries, Edsko
Hennessy, Matthew
Keywords: Computer multitasking
Issue Date: 2014
Publisher: International Federation for Computational Logic
Citation: Francalanza, A., Devries, E., & Hennessy, M. (2014). Compositional reasoning for explicit resource management in channel-based concurrency. Logical Methods in Computer Science, 10, 1-52.
Abstract: We define a π-calculus variant with a costed semantics where channels are treated as re- sources 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 wrt. 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.
Appears in Collections:Scholarly Works - FacICTCS

Files in This Item:
File Description SizeFormat 
journal.pdf328.55 kBAdobe PDFView/Open

Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.