Verifiably correct high-performance concurrency libraries for multi-core computing systems

快速计算机系统的好处是显而易见的--性能的提高使更复杂的应用程序得以开发。然而，通过更高的处理器时钟速度来加速，在21世纪初达到了物理上限，功耗成为一个主要问题。因此，硬件设计人员转而使用具有固定时钟速度的多核处理器，在这种处理器中，通过在单个处理器中包含多个内核来实现加速。多核处理器广泛存在于计算的各个方面，从集群服务器、桌面到低功耗的移动设备。多核处理器通过允许多个计算在不同的核中同时进行，从而高效地执行由多个线程组成的并发程序。这些线程通过同步访问和修改存储在共享内存中的共享资源进行通信。虽然一些问题(令人尴尬的并行问题)自然能够利用多核计算，但大多数问题需要巧妙地管理线程同步，而这很难实现。此外，现代体系结构迫使程序员除了了解他们开发的程序中的并发问题外，还必须了解硬件/软件接口的复杂细节。在多核处理器中，每个处理核心都可以访问充当临时缓存的本地缓冲区-在缓冲区刷新之前，存储在本地缓冲区中的任何写入都对其他内核不可见。出于效率原因，多核体系结构实现了所谓的松弛内存模型，其中单个线程中的读写事件可能无序地在共享内存中生效，从而导致程序员可能无法预期的行为。要恢复正确性，需要在程序代码中手动引入“栅栏”指令，这不是一项微不足道的任务--栅栏不足会导致不正确的行为，而栅栏过度会导致程序效率低下。因此，正如Shavit所说，“多核处理器作为标准计算平台的出现将迫使软件设计发生重大变化。”在学术界和工业界都有大量的国际努力来更好地利用多核处理，从新的基础和理论基础到开发新的抽象、工具支持、工程范例等。在这个项目中，我们的目标是通过高性能(提高效率)、可验证的正确(以确保可靠性)和处理放松内存模型(如现代硬件所使用的)的实用解决方案来简化系统开发。特别是，我们开发了高效的“并发对象”，这些对象提供来自低级硬件接口的抽象，并代表程序员管理线程同步。并发对象最终将成为编程语言库的一部分--一些语言，如Java已经提供了基本的并发对象作为其标准库的一部分--因此具有很高的适用性。我们提供的对象将利用宽松的内存模型。这里，众所周知，过于严格的正确性条件(例如，线性化)本身正在成为效率的障碍。因此，我们从发展新的理论基础开始，以符合放松记忆模型的放松正确性条件的形式。将建立不同条件的等级，使人们能够容易地确定每种条件的相对强度。这些条件将与改进的上下文概念相关联，以提供客户端程序中的可替换性的基础。这为更有效、可验证正确的、用于松弛记忆模型的并发对象提供了基础。我们将专注于为TSO内存模型开发并发数据结构(例如，堆栈、队列、双队列)。它们的验证将在KIV定理证明器中实现机械化，以消除验证中的人为错误，这反过来又提高了可靠性。

The benefits of fast computer systems are clear - improving performance allows more sophisticated applications to be developed. Speed-up via higher processor clock speeds, however, reached a physical upper limit in the early 2000s, with power-dissipation becoming a major issue. Hardware designers have therefore switched to multicore processors with fixed clock speeds, where speed-up is achieved by including several cores in a single processor. Multicore processors are now pervasive in all aspects of computing, from cluster servers and desktops to low-power mobile devices.A multicore processor efficiently executes concurrent programs comprising multiple threads by allowing several computations to take place simultaneously in the different cores. These threads communicate via synchronised access and modification of shared resources stored in shared memory. While some problems (coined embarrassingly parallel problems) are naturally able to take advantage of multicore computing, the majority require clever management of thread synchronisation that is difficult to achieve. Moreover, modern architectures have forced programmers to understand intricate details of the hardware/software interface in addition to concurrency issues within the programs they develop.Within a multicore processor, each processing core has access to a local buffer that acts as a temporary cache - any writes stored in a local buffer are not visible to other cores until the buffer is flushed. For efficiency reasons, multicore architectures implement so-called relaxed-memory models, where read and write events within a single thread may take effect in shared memory out-of-order, leading to behaviours that may not be expected by a programmer. Restoring correctness requires manual introduction of "fence" instructions in a program's code, which is a non-trivial task - under-fencing leads to incorrect behaviours, while overfencing leads to inefficient programs. Therefore, as Shavit states, "The advent of multicore processors as the standard computing platform will force major changes in software design." There is a large international effort in both academia and industry to make better use of multicore processing, ranging from new foundational and theoretical underpinnings to the development of novel abstractions, tool support, engineering paradigms, etc.In this project, we aim to simplify system development via practical solutions that are highly performant (to increase efficiency), verifiably correct (to ensure dependability) and cope with relaxed-memory models (as used by modern hardware). In particular, we develop efficient "concurrent objects" that provide abstractions from the low-level hardware interface and manage thread synchronisation on behalf of a programmer. Concurrent objects are to ultimately become part of a programming language library - some languages e.g., Java already offer basic concurrent objects as part of their standard library - hence are highly applicable.The objects we deliver will take advantage of relaxed memory models. Here, it is well known that correctness conditions that are too strict (e.g., linearizability) are themselves becoming a barrier to efficiency. We therefore begin by developing new theoretical foundations in the form of relaxed correctness conditions that match relaxed memory models. A hierachy of different conditions will be developed, enabling one to easily determine the relative strengths of each condition. These conditions will be linked to a contextual notion of refinement to provide a basis for substitutability in client programs. This provides a basis for more efficient, verifiably correct, concurrent objects for relaxed memory models. We will focus on developing concurrent data structures (e.g., stacks, queues, deques) for the TSO memory model. Their verification will be mechanised in the KIV theorem prover to eliminate human error in verification, which in turn improves dependability.