arrow
返回

Compositional relaxed concurrency

delete2017-09-04
delete5
delete
OA
AI
M
Mark Batty *
DOI:10.1098/rsta.2015.0406delete
delete原文链接
delete分享
delete收藏
查看原文
摘要

摘要

En 中文
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. This article is part of the themed issue 'Verified trustworthy software systems'.
Keyword:
relaxed memory
verification
semantics
concurrency
heterogeneous systems
graphics
processors
AI总结

AI总结

对已上传原文的论文进行重点信息的提取,主要内容包括:简要概述、研究摘要、背景介绍、关键亮点、图文解析、展望与总结。

期刊

P
Philosophical Transactions of the Royal Society A-Mathematical Physical and Engineering Sciences
IF:
3.7
论文数:
7.8K
被引数:
2.8W

机构

U
University of Kent
学者数:
5.3K
论文数: 6.1K
被引数: 8.1K
引用论文

引用论文

Exposure to Residential Indoor Air Induces Heritable DNA Mutations in Mice
err2009-11-02
err0
PREAI
errYin Zhou; Yunru Liu; Wen Qiu; Jinyan Zeng; Xiaodong Chen; Hanzhi Zhou; Aiping Li; Jianwei Zhou
err分享
err收藏
err分享
err收藏
Geographical variation in allometry in the guppy (Poecilia reticulata)
err2011-09-28
err0
PREAI
errC. K. EGSET; G. H. BOLSTAD; G. ROSENQVIST; J. A. ENDLER; C. PÉLABON
err分享
err收藏
学者 查看更多内容