权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Verifying concurrent algorithms on Weak Memory Models

验证弱内存模型上的并发算法

基本信息

批准号：
EP/M017044/1
负责人：
John Derrick
金额：
$ 49.59万
依托单位：
University of Sheffield
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2015
资助国家：
英国
起止时间：
2015 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FM017044%2F1
关键词：
Verifying concurrent algorithms Weak Memory

项目摘要

Multi-core computing architectures have become ubiquitous over the last decade. This has been driven by the demand for continual performance improvements to cope with the every increasing sophistication of applications (for example, in the areas of graphics and audio processing). It has been necessary due to the constraints on chip manufacture which have prevented the continuation of performance improvements of earlier decades achieved primarily by speeding up sequential computation. The inherent parallelism these multi-core architectures entail offer great technical opportunities. Exploiting these opportunities presents a number of technical challenges.The high-level aim of this project is to address two key technical challenges in the area. Firstly, in order to fully exploit the potential concurrency, programmers are developing very subtle concurrent algorithms which dispense with the need to lock shared memory and data structures. Linearizability is the standard correctness criterion for concurrent programs. However, the complexity of these algorithms means that checking their correctness with a high degree of confidence is extremely difficult. Verification is needed, and we seek to develop appropriate proof methods to support it.Secondly, most prior work on correctness assumes a memory model (sequential consistency) which is not implemented in practice. In reality to increase efficiency, typical multicore systems communicate via shared memory and use relaxed memory models which give greater scope for optimization. These are the memory models implemented in processors such as x86, PowerPC, and ARM, and on these linearizability isn't the only relevant correctness criteria, and we shall also develop proof methods to quiescent consistency, which is emerging as an alternative correctness criteria on these processors.

在过去的十年中，多核计算架构已经变得无处不在。这是由不断提高性能的需求推动的，以科普日益复杂的应用程序（例如，在图形和音频处理领域）。这是必要的，由于芯片制造的限制，这阻止了前几十年主要通过加速顺序计算实现的性能改进的继续。这些多核架构固有的并行性提供了巨大的技术机会。利用这些机会提出了一系列技术挑战。本项目的高层次目标是解决该领域的两个关键技术挑战。首先，为了充分利用潜在的并发性，程序员正在开发非常微妙的并发算法，这些算法无需锁定共享内存和数据结构。可线性化是并发程序的标准正确性准则。然而，这些算法的复杂性意味着以高度的置信度检查其正确性是极其困难的。验证是必要的，我们寻求开发适当的证明方法来支持它。其次，大多数关于正确性的先前工作假设了一个在实践中没有实现的内存模型（顺序一致性）。实际上，为了提高效率，典型的多核系统通过共享内存进行通信，并使用宽松的内存模型，这为优化提供了更大的空间。这些是在x86、PowerPC和ARM等处理器中实现的内存模型，在这些处理器上，线性化不是唯一相关的正确性标准，我们还将开发静态一致性的证明方法，这是这些处理器上的替代正确性标准。

项目成果

期刊论文数量（10）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Verifying C11 programs operationally

DOI：
10.1145/3293883.3295702
发表时间：
2018-11
期刊：
Proceedings of the 24th Symposium on Principles and Practice of Parallel Programming
影响因子：
0
作者：
Simon Doherty;Brijesh Dongol;H. Wehrheim;J. Derrick
通讯作者：
Simon Doherty;Brijesh Dongol;H. Wehrheim;J. Derrick

Proving Opacity of a Pessimistic STM

证明悲观 STM 的不透明性