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). Article Number 20150406. ISSN 1364-503X. E-ISSN 1471-2962. (doi:10.1098/rsta.2015.0406) (KAR id:64300)

PDF Author's Accepted Manuscript
Language: English
Download this file
(PDF/327kB)
[thumbnail of battyRS.pdf]
Preview
Request a format suitable for use with assistive technology e.g. a screenreader
PDF Publisher pdf
Language: English

Restricted to Repository staff only
Contact us about this Publication
[thumbnail of battyRS.pdf]
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: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Batty
Date Deposited: 07 Nov 2017 15:16 UTC
Last Modified: 16 Feb 2021 13:49 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/64300 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.