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

Verifiably correct concurrency abstractions

可验证正确的并发抽象

基本信息

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

来源：
https://gtr.ukri.org/projects?ref=EP%2FR019045%2F2
关键词：
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股票的IPO失败，以及美国宇航局火星探路者任务的近乎失败。其他的安全关键错误已经从使用低级优化中显现出来，例如，双重检查锁定错误和Java帕克错误。该项目通过使用可伸缩的原子性抽象（如TM）和并发对象来提高并发程序的可编程性，这些抽象使普通应用程序程序员可以使用低级优化。这些对象的操作是高度并发的（这提高了效率），但是代表程序员管理同步以提供原子性的错觉。因此，通过使用TM，程序员的关注点从应该使什么成为原子性转向应该如何保证原子性。这意味着并发系统可以以分层的方式开发（支持关注点分离）。TM承诺的一系列吸引人的特性意味着TM的实现越来越多地被纳入主流系统（硬件和软件）。自从20世纪90年代中期从数据库理论中引入事务以来，软件TM实现现在可用于所有主要的编程语言。最近的进展包括编译器中的实验性特性，如g++ 4.7可以直接编译事务性代码；将TM纳入c++的标准化工作正在进行中。学术界和工业界都对混合TM有广泛的研究兴趣，以充分利用，例如，Intel的Haswell/Broadwell和IBM的Blue Gene/Q处理器中的TM特性。TM的高度复杂性和广泛适用性意味着必须正式验证实现，以确保可靠性和可靠性。总的来说，我们将改进TM实现的可靠性、性能和灵活性。