Compositional relaxed concurrency
Compositional relaxed concurrency
复制标题
组合宽松并发
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Mark Batty
中科院分区：
文献类型：
--
作者：
Mark Batty
有一个可行的计算机处理器的广泛设计空间：它们可以针对低功率，低潜伏期或高吞吐量进行优化。负责复杂而关键的任务，例如汽车指导系统。证明这是不正确的，导致系统的许多层和优化性在我们指定并发系统的内存行为上，并提出了一个新的方向。可以一起使用多个处理器和语言。对于现代系统中的多种处理器，以及使用理想的并发模型的处理器，为成熟的验证技术提供了声音的基础。
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’.
登录
查看更多内容
彻底修改 C11 和 OpenCL 中的 SC 原子
DOI：
10.1145/2837614.2837637
发表时间：
2016
期刊：
--
影响因子：
--
作者：
Batty M
通讯作者：
Batty M
DOI：
10.1145/2837614.2837615
发表时间：
2016-01
期刊：
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
Shaked Flur;Kathryn E. Gray;Christopher Pulte;Susmit Sarkar;A. Sezgin;Luc Maranget;Will Deacon;Peter Sewell
通讯作者：
Shaked Flur;Kathryn E. Gray;Christopher Pulte;Susmit Sarkar;A. Sezgin;Luc Maranget;Will Deacon;Peter Sewell
同步 C/C 和 POWER
DOI：
10.1145/2254064.2254102
发表时间：
2012
期刊：
--
影响因子：
--
作者：
Sarkar S
通讯作者：
Sarkar S
DOI：
10.1145/2814270.2814283
发表时间：
2015
期刊：
--
影响因子：
--
作者：
Wickerson J
通讯作者：
Wickerson J
混合大小并发：ARM、POWER、C/C 11 和 SC
DOI：
10.1145/3009837.3009839
发表时间：
2017
期刊：
--
影响因子：
--
作者：
Flur S
通讯作者：
Flur S