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

Verifiably correct concurrency abstractions

可验证正确的并发抽象

基本信息

批准号：
EP/R019045/1
负责人：
Brijesh Dongol
金额：
$ 1.83万
依托单位：
Brunel University London
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2017
资助国家：
英国
起止时间：
2017 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FR019045%2F1
关键词：
Verifiably correct concurrency abstractions

项目摘要

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 ever-increasing sophistication of applications, combined with physical limitations on chip designs, whereby speed-up via higher clock speeds has become infeasible. The inherent parallelism that multi-core architectures entail offers great technical opportunities, however, exploiting these opportunities presents a number of technical challenges.To ensure correctness, concurrent programs must be properly synchronised, but synchronisation invariably introduces sequential bottlenecks, causing performance to suffer. Fully exploiting the potential for concurrency requires optimisations to consider executions at low levels of abstraction, e.g., the underlying memory model, compiler optimisations, cache-coherency protocols etc. The complexity of such considerations means that checking correctness with a high degree of confidence is extremely difficult. Concurrency bugs have specifically been attributed to disasters such as a power blackout in north-eastern USA, Nasdaq's botched IPO of Facebook shares, and the near failure of NASA's Mars Pathfinder mission. Other safety-critical errors have manifested from using low-level optimisations, e.g., the double-checked locking bug and the Java Parker bug.This project improves programmability of concurrent programs through the use of scalable atomicity abstractions such as TM and concurrent objects that make low-level optimisations available to general application programmers. Operations of such objects are highly concurrent (which improves efficiency), yet manage synchronisation on behalf of a programmer to provide an illusion of atomicity. Thus, by using TM, the focus of a programmer switches from what should be made atomic, as opposed to how atomicity should be guaranteed. This means concurrent systems can be developed in a layered manner (enabling a separation of concerns).The attractive set of features that TM promises means that TM implementations are increasingly being incorporated into mainstream systems (hardware and software). Since the adaptation of transactions from database theory in the mid 1990s, software TM implementations are now available for all major programming languages. Recent advances include experimental features in compilers such as G++ 4.7 that directly enable compilation of transactional code; standardisation work to include TM within C++ is ongoing. There is extensive research interest in hybrid TM within both academia and industry to make best use of, for example, TM features in Intel's Haswell/Broadwell and IBM's Blue Gene/Q processors.The high level of complexity, yet wide-scale applicability of TM means that implementations must be formally verified to ensure dependability and reliability. Overall, we will improve the dependability, performance, and flexibility of TM implementations.

在过去的十年里，多核计算架构已经变得无处不在。这是由于为了应对不断增长的应用复杂性而不断改进性能的需求，加上芯片设计的物理限制，通过更高的时钟速度来加速已经变得不可行。多核架构固有的并行性提供了巨大的技术机会，然而，利用这些机会提出了许多技术挑战。为了确保正确性，并发程序必须正确同步，但同步总是会引入顺序瓶颈，导致性能受到影响。充分利用并发潜力需要优化以考虑低抽象级别的执行，例如底层内存模型、编译器优化、缓存一致性协议等。此类考虑的复杂性意味着以高度置信度检查正确性极其困难。并发错误具体归因于诸如美国东北部停电、纳斯达克 Facebook 股票首次公开募股失败以及美国宇航局火星探路者任务几近失败等灾难。其他安全关键错误是通过使用低级优化而显现出来的，例如双重检查锁定错误和 Java Parker 错误。该项目通过使用可扩展的原子性抽象（例如 TM 和并发对象）来提高并发程序的可编程性，这些抽象使一般应用程序程序员可以使用低级优化。此类对象的操作是高度并发的（这提高了效率），但代表程序员管理同步以提供原子性的错觉。因此，通过使用 TM，程序员的焦点从应该原子性转向如何保证原子性。这意味着并发系统可以以分层方式开发（实现关注点分离）。TM 承诺的一系列有吸引力的功能意味着 TM 实现越来越多地被纳入主流系统（硬件和软件）中。自从 20 世纪 90 年代中期数据库理论对事务进行改编以来，软件 TM 实现现在可用于所有主要编程语言。最近的进展包括编译器中的实验性功能，例如 G++ 4.7，可以直接编译事务代码；将 TM 纳入 C++ 的标准化工作正在进行中。学术界和工业界对混合 TM 有着广泛的研究兴趣，以充分利用英特尔的 Haswell/Broadwell 和 IBM 的 Blue Gene/Q 处理器中的 TM 功能。 TM 的高度复杂性和广泛的适用性意味着必须对实现进行正式验证，以确保可靠性和可靠性。总体而言，我们将提高 TM 实现的可靠性、性能和灵活性。

项目成果

期刊论文数量（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

Proceedings 18th Refinement Workshop Preface

第十八届精炼研讨会论文集前言