Reasoning with Relaxed Memory Models

计算机科学正在经历一场艰难的转型。过去几十年的持续性能改进主要是通过加速顺序计算实现的。设备制造中的限制，特别是功耗问题，正在推动向无处不在的并发计算的转变，多核处理器变得司空见惯。然而，对这些进行编程以提供高性能和可靠的系统仍然非常具有挑战性。有两个关键的困难，我们在这里解决。首先，正在开发的并发算法，如非阻塞数据结构和软件事务存储器的实现，都是非常微妙的，因此非形式化推理不能给它们的正确性带来很高的置信度。其次，关于并发的软件验证(包括时序逻辑、依赖保证推理、分离逻辑和进程演算)的大量先前工作忽略了现在的一个关键现象：放松的内存模型。出于性能原因，典型的多处理器不提供顺序一致的内存模型。相反，内存访问可能会以各种受限的方式重新排序，这使得对执行进行推理变得更加困难。在这个项目中，我们将为真实处理器的行为建立准确的语义，例如x86、PowerPC和ARM体系结构，涵盖它们的内存模型和指令集片段。我们将基于我们以前使用真实的大规模语义的经验，对这些进行实验验证。在这些基础上，我们将根据我们在分离逻辑、机械化推理和算法设计方面的经验，开发理论和实践工具来指定和证明现代算法的正确性。因此，我们将为针对真实多核处理器的验证编译奠定基础，为未来的应用提供高性能和高信心。

Computer Science is undergoing a difficult transition. The continual performance improvements of past decades were achieved primarily by speeding up sequential computation. Constraints in device manufacture, especially the problem of power consumption, are driving a shift to ubiquitous concurrent computation, with multicore processors becoming commonplace. Programming these, however, to deliver high-performance and reliable systems, remains very challenging. There are two key difficulties, which we address here. Firstly, the concurrent algorithms that are being developed, such as non-blocking datastructures and implementations of software transactional memory, are very subtle, so informal reasoning cannot give high confidence in their correctness. Secondly, the extensive prior work on software verification for concurrency (including temporal logics, rely-guarantee reasoning, separation logic, and process calculi) neglects what is now a key phenomenon: relaxed memory models. For performance reasons, typical multiprocessors do not provide a sequentially consistent memory model. Instead, memory accesses may be reordered in various constrained ways, making it still harder to reason about executions. In this project we will establish accurate semantics for the behaviour of real-world processors, such as x86, PowerPC, and ARM architectures, covering their memory models and fragments of their instruction sets. We will experimentally validate these, building on our previous experience with realistic large-scale semantics. Above these, we will develop theoretical and practical tools for specifying and proving correctness of modern algorithms, building on our experience with separation logic, mechanized reasoning, and algorithm design. We will thereby lay the groundwork for verified compilation targeting real multicore processors, providing both high performance and high confidence for future applications.