Skip to main content

Compositional relaxed concurrency

Batty, Mark (2017) Compositional relaxed concurrency. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 375 (2104). ISSN 1364-503X. E-ISSN 1471-2962. (doi:10.1098/rsta.2015.0406)

PDF - Author's Accepted Manuscript
Download (234kB) Preview
[img]
Preview
PDF - Publisher pdf
Restricted to Repository staff only
Contact us about this Publication Download (290kB)
[img]
Official URL
https://doi.org/10.1098/rsta.2015.0406

Abstract

There is a broad design space for concurrent computer processors: they can be optimized for low power, low latency or high throughput. This freedom to tune each processor design to its niche has led to an increasing diversity of machines, from powerful pocketable devices to those responsible for complex and critical tasks, such as car guidance systems. Given this context, academic concurrency research sounds notes of both caution and optimism. Caution because recent work has uncovered flaws in the way we explain the subtle memory behaviour of concurrent systems: specifications have been shown to be incorrect, leading to bugs throughout the many layers of the system. And optimism because our tools and methods for verifying the correctness of concurrent code—although built above an idealized model of concurrency—are becoming more mature. This paper looks at the way we specify the memory behaviour of concurrent systems and suggests a new direction. Currently, there is a siloed approach, with each processor and programming language specified separately in an incomparable way. But this does not match the structure of our programs, which may use multiple processors and languages together. Instead we propose a compositional approach, where program components carry with them a description of the sort of concurrency they rely on, and there is a mechanism for composing these. This will support not only components written for the multiple varied processors found in a modern system but also those that use idealized models of concurrency, providing a sound footing for mature verification techniques.

Item Type: Article
DOI/Identification number: 10.1098/rsta.2015.0406
Subjects: Q Science
Divisions: Faculties > Sciences > School of Computing
Depositing User: Mark Batty
Date Deposited: 07 Nov 2017 15:16 UTC
Last Modified: 29 May 2019 19:47 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/64300 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year