Verifying Concurrent Lock-free Algorithms

软件正变得越来越复杂，对提高性能的需求由许多不同的应用程序驱动。作为对这一需求的回应，有效利用多核体系结构的并发软件可能会成为许多行业的标准。然而，开发正确的并发算法是一项艰巨的任务。对于通过提供在共享内存上工作的不同进程的最大交错量来充分利用潜在并发性的一类并发算法而言尤其如此。因此，构建能够验证这些已知的无锁算法是否正确的技术在经济上是当务之急。测试和模拟虽然在一定程度上是有价值的和自动化的，但它们所能提供的正确性保证最终是有限的，特别是在并发算法的情况下，其中多线程交织作用于可能无限大小的数据结构。这类算法的形式化验证变得越来越容易，人们对应用这类技术的兴趣激增，在一类算法被广泛采用之前，这是一个独特的验证机会。本项目专注于无锁算法(也称为非阻塞算法)。已经为许多常见的数据结构发现了无锁的算法。非阻塞算法广泛用于操作系统和JVM级别的任务，如线程和进程调度。虽然它们的实现更加复杂，但与基于锁的替代方案相比，它们具有许多优势--避免了优先级反转和死锁等危险，争用成本更低，协调发生在更精细的粒度级别，实现了更高程度的并行性。该项目寻求开发能够证明此类算法正确的技术。这些技术基于精化的概念，它将抽象规范与更详细的具体实现联系在一起。我们在这里要做的是展示抽象描述和并发算法之间的某种类型的精化意味着并发算法是正确的。这里的正确性概念是线性化。我们提议做的部分新奇之处在于构建了正确类型的精化关系-它必须是一种将意味着线性化，但同时又产生了对特定算法容易处理的证明义务，也就是说，实际上使线性化的验证更容易实现。另一个新颖性是，我们将把整个事情机械化--既是对特定算法的证明，也是我们技术正确的证明，从而额外确保技术确实是健全的-细节足够复杂和微妙，以至于机械化真的必须100%确定正确性。除了这些基本知识之外，我们还想要一种适用于广泛算法的证明方法，并且是一种合成的方法。为了提高适用性，我们开发了两种技术--一种基于正向模拟，另一种基于反向模拟，以及对无界点和动态线性化点的具体支持。为了帮助合成性(这样证明可以被分解成更小的局部步骤，而不是承担一个大型的全局证明)，我们将开发线程模块模拟条件和干扰自由条件，以帮助该过程。我们的工作将在一些基准算法上进行评估，例如堆栈、队列、哈希表等的无锁实现。最后，我们将研究如何证明我们的证明方法是完整的，即每个算法都可以通过使用该方法进行验证。我们还将调查活性，即表明并发算法保证了各种形式的级数。

Software is becoming increasingly complex, and the demand for increased performance is driven by many diverse applications. As a response to this demand, concurrent software that efficiently exploits multi-core architectures is likely to be the norm in many sectors. However, developing correct concurrent algorithms is a difficult task. This is particularly true for a class of concurrent algorithms that fully exploit the potential concurrency by offering the maximum amount of interleavings of different processes working on a shared memory. There is then a real economic imperative to build techniques that can verify as correct such lock-free algorithms as they are known.Testing and simulation, while valuable and automated to a degree, are ultimately limited in the guarantees they can offer for correctness, particularly in the case of concurrent algorithms, where multiple thread interleavings act on data structures potentially unbounded in size. Formal verification of this class of algorithm is becoming tractable and there has been a surge of interest in applying such techniques, and a unique opportunity to verify a class of algorithms before their widespread adoption.This project focusses on lock-free algorithms (also called non-blocking algorithms). Lock-free algorithms have been discovered for many common data structures. Non-blocking algorithms are used extensively at the operating system and JVM level for tasks such as thread and process scheduling. While they are more complicated to implement, they have a number of advantages over lock-based alternatives -- hazards like priority inversion and deadlock are avoided, contention is less expensive, and coordination occurs at a finer level of granularity, enabling a higher degree of parallelism.This project seeks to develop techniques whereby such algorithms can be proved correct. The techniques are based on the notion of refinement which relates an abstract specification with a more detailed concrete implementation. What we will do here is show that a certain type of refinement between an abstract description and a concurrent algorithm implies that the concurrent algorithm is correct. The notion of correctness here being linearizability.Part of the novelty of what we propose to do is in the construction of the right sort of refinement relation - it has to be one that will imply linearizability, yet at the same time give rise to proof obligations that are tractable for specific algorithms, that is, actually make the verification of linearizability easier to achieve. Another part of the novelty is that we will mechanize the whole thing - both the proofs for specific algorithms, but also the proof that our technique is correct, thus giving an extra level of assurance that the techniques really are sound - the details are sufficiently complex and subtle that mechanization really is necessary to be 100% sure of correctness.In addition to these basics we want a proof method that is applicable to a wide range of algorithms, and one that is compositional. To aid applicability we develop two flavours of technique - one based on forward simulation, and another based on backward simulation, as well as specific support for unboundedness and dynamic linearization points. To aid compositionality (so that the proofs can be broken down into smaller local steps rather than undertaking one large global proof) we will develop thread modular simulation conditions, and interference freedom conditions that aid the process.Our work will be evaluated on a number of 'benchmark' algorithms, such as lock-free implementations of stacks, queues, hashtables etc. Finally, we will investigate how our proof methods can be shown to be complete, that is, every algorithm could potentially be verified by using the method. We will also investigate liveness, ie, showing that a concurrent algorithm guarantees various forms of progression.