Compositional Reasoning for Explicit Resource Management in Channel-Based Concurrency
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 techni...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2014-06-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/691/pdf |
| _version_ | 1797268734588485632 |
|---|---|
| author | Adrian Francalanza Edsko DeVries Matthew Hennessy |
| author_facet | Adrian Francalanza Edsko DeVries Matthew Hennessy |
| author_sort | Adrian Francalanza |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:37:11Z |
| format | Article |
| id | doaj.art-ed9ab7fc9e0743e7ab9c4a1f9276b018 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:37:11Z |
| publishDate | 2014-06-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-ed9ab7fc9e0743e7ab9c4a1f9276b0182024-03-08T09:36:22ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742014-06-01Volume 10, Issue 210.2168/LMCS-10(2:15)2014691Compositional Reasoning for Explicit Resource Management in Channel-Based ConcurrencyAdrian Francalanzahttps://orcid.org/0000-0003-3829-7391Edsko DeVriesMatthew HennessyWe 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.https://lmcs.episciences.org/691/pdfcomputer science - logic in computer science |
| spellingShingle | Adrian Francalanza Edsko DeVries Matthew Hennessy Compositional Reasoning for Explicit Resource Management in Channel-Based Concurrency Logical Methods in Computer Science computer science - logic in computer science |
| title | Compositional Reasoning for Explicit Resource Management in Channel-Based Concurrency |
| title_full | Compositional Reasoning for Explicit Resource Management in Channel-Based Concurrency |
| title_fullStr | Compositional Reasoning for Explicit Resource Management in Channel-Based Concurrency |
| title_full_unstemmed | Compositional Reasoning for Explicit Resource Management in Channel-Based Concurrency |
| title_short | Compositional Reasoning for Explicit Resource Management in Channel-Based Concurrency |
| title_sort | compositional reasoning for explicit resource management in channel based concurrency |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/691/pdf |
| work_keys_str_mv | AT adrianfrancalanza compositionalreasoningforexplicitresourcemanagementinchannelbasedconcurrency AT edskodevries compositionalreasoningforexplicitresourcemanagementinchannelbasedconcurrency AT matthewhennessy compositionalreasoningforexplicitresourcemanagementinchannelbasedconcurrency |