Verifiably Correct Transactional Memory.

在过去十年中，多核计算架构变得无处不在。这是由于不断提高性能的需求，以应对日益复杂的应用程序，再加上芯片设计的物理限制，通过更高的时钟速度加速已经变得不可行的。多核架构所带来的固有并行性提供了巨大的技术机会，然而，利用这些机会也带来了许多技术挑战。为了确保正确性，必须对并发程序进行适当的同步，但是同步总是会引入顺序瓶颈，从而影响性能。要充分挖掘并发的潜力，就需要在较低抽象层次上进行优化，例如底层内存模型、编译器优化、缓存一致性协议等。这些考虑的复杂性意味着以高度自信的方式检查正确性是极其困难的。并发错误被特别地归因于灾难，比如美国东北部的停电，纳斯达克Facebook股票的IPO失败，以及美国宇航局火星探路者任务的近乎失败。其他的安全关键错误已经从使用低级优化中显现出来，例如，双重检查锁定错误和Java帕克错误。该项目通过使用事务性内存（TM）提高了并发程序的可编程性，事务性内存是一种并发机制，可为普通应用程序程序员提供低级优化。TM是对数据库事务的一种改编。TM操作是高度并发的（这提高了效率），但是代表程序员管理同步以提供原子性的假象。因此，通过使用TM，程序员的关注点从应该使什么成为原子性转向应该如何保证原子性。这意味着并发系统可以以分层的方式开发（支持关注点分离）。TM承诺的一系列吸引人的特性意味着TM的实现越来越多地被纳入主流系统（硬件和软件）。自从20世纪90年代中期从数据库理论中引入事务以来，软件TM实现现在可用于所有主要的编程语言。最近的进展包括编译器中的实验性特性，如g++ 4.7可以直接编译事务性代码；将TM纳入c++的标准化工作正在进行中。学术界和工业界都对混合TM有广泛的研究兴趣，以充分利用，例如，Intel的Haswell/Broadwell和IBM的Blue Gene/Q处理器中的TM特性。TM的高度复杂性和广泛适用性意味着必须正式验证实现，以确保可靠性和可靠性。该项目解决了围绕TM的一些主要挑战，并采取了促进大规模采用所需的关键步骤。也就是说，我们在理解TM正确性方面取得了理论进展；TM验证技术的方法学进展；通过开发应用感知TM设计实现了实用主义的进步。验证工具将支持这些步骤中的每一个。因此，我们确定了以下目标：开发不同执行模型下TM正确性（原子性和交互保证）的基础，并将其与客户端正确性联系起来。机械地验证TM实现的正确性，并开发原则性的证明技术。设计在当前和未来的多核硬件下提供更好性能的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 speedup 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 transactional memory (TM), which is a concurrency mechanism that makes low-level optimisations available to general application programmers. TM is an adaptation of transactions from databases. TM operations 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. This project addresses some of the main challenges surrounding TM, and takes the key steps necessary to facilitate wide-scale adoption. Namely, we deliver theoretical advances in our understanding of TM correctness; methodological advances in verification techniques for TM; and pragmatic advances via the development of application-aware TM designs. Verification tools will support each of these steps. We therefore set the following objectives:O1. Develop foundations for TM correctness (atomicity and interaction guarantees) under different execution models and relate these to client correctness.O2. Mechanically verify correctness of TM implementations, and develop principled proof techniques.O3. Design TM implementations that provide better performance under current and future multi-core hardware.O4. Develop tool support to simplify mechanised verification of TM and automated checking of client programs that use them.Overall, we will improve the dependability, performance, and flexibility of TM implementations.