Verifiably correct concurrency abstractions

在过去的十年中，多核计算架构变得无处不在。这是由于对持续改进性能的需求，以应对日益复杂的应用程序，加上芯片设计的物理限制，通过更高的时钟速度进行加速已变得不可行。多核体系结构固有的并行性提供了巨大的技术机会，然而，利用这些机会带来了许多技术挑战。为了确保正确性，并发程序必须正确同步，但同步总是会引入顺序瓶颈，导致性能下降。充分利用并发性的潜力需要优化来考虑低抽象级别的执行，例如底层存储器模型、编译器优化、高速缓存一致性协议等。这些考虑的复杂性意味着以高度的置信度检查正确性是极其困难的。并发漏洞被明确地归因于灾难，如美国东北部的停电，纳斯达克拙劣的Facebook股票首次公开募股，以及NASA的火星探路者任务几乎失败。这个项目通过使用可伸缩的原子性抽象(如TM和并发对象)来提高并发程序的可编程性，这些抽象使低级优化对一般应用程序程序员可用。这类对象的操作是高度并发的(这提高了效率)，但仍代表程序员管理同步，以提供原子性的错觉。因此，通过使用TM，程序员的关注点从应该使之原子化的内容转变，而不是应该如何保证原子性。这意味着并发系统可以以分层的方式开发(实现关注点分离)。TM承诺的一组吸引人的功能意味着TM实现正越来越多地被纳入主流系统(硬件和软件)。自20世纪90年代中期从数据库理论中改编事务以来，软件TM实现现在可用于所有主要编程语言。最近的进展包括编译器中的实验性功能，如G++4.7，它直接支持事务代码的编译；将TM包括在C++中的标准化工作正在进行中。学术界和工业界对混合TM有着广泛的研究兴趣，以充分利用英特尔的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.