Verifiably correct concurrency abstractions

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

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.