Verifying concurrent algorithms on Weak Memory Models

在过去的十年中，多核计算架构变得无处不在。这是由于需要不断改进性能以应对日益复杂的应用程序(例如，在图形和音频处理领域)的需求。这是必要的，因为对芯片制造的限制阻碍了主要通过加速顺序计算实现的最初几十年的性能改进的持续。这些多核架构所具有的内在并行性提供了巨大的技术机遇。利用这些机会带来了许多技术挑战。该项目的高级目标是解决该领域的两个关键技术挑战。首先，为了充分利用潜在的并发性，程序员正在开发非常微妙的并发算法，这些算法不需要锁定共享的内存和数据结构。可线性化是并发程序的标准正确性准则。然而，这些算法的复杂性意味着要以高度的置信度检查它们的正确性是极其困难的。验证是需要的，我们试图开发适当的证明方法来支持它。第二，以前关于正确性的工作大多假设了一个记忆模型(顺序一致性)，但在实践中并没有实现。实际上，为了提高效率，典型的多核系统通过共享内存进行通信，并使用宽松的内存模型，这为优化提供了更大的空间。这些是在x86、PowerPC和ARM等处理器中实现的内存模型，基于这些模型，线性化并不是唯一相关的正确性标准，我们还将开发静态一致性的证明方法，这正在成为这些处理器上的替代正确性标准。

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 every increasing sophistication of applications (for example, in the areas of graphics and audio processing). It has been necessary due to the constraints on chip manufacture which have prevented the continuation of performance improvements of earlier decades achieved primarily by speeding up sequential computation. The inherent parallelism these multi-core architectures entail offer great technical opportunities. Exploiting these opportunities presents a number of technical challenges.The high-level aim of this project is to address two key technical challenges in the area. Firstly, in order to fully exploit the potential concurrency, programmers are developing very subtle concurrent algorithms which dispense with the need to lock shared memory and data structures. Linearizability is the standard correctness criterion for concurrent programs. However, the complexity of these algorithms means that checking their correctness with a high degree of confidence is extremely difficult. Verification is needed, and we seek to develop appropriate proof methods to support it.Secondly, most prior work on correctness assumes a memory model (sequential consistency) which is not implemented in practice. In reality to increase efficiency, typical multicore systems communicate via shared memory and use relaxed memory models which give greater scope for optimization. These are the memory models implemented in processors such as x86, PowerPC, and ARM, and on these linearizability isn't the only relevant correctness criteria, and we shall also develop proof methods to quiescent consistency, which is emerging as an alternative correctness criteria on these processors.