Verifying Concurrent Lock-free Algorithms

点击翻译按钮获取中文摘要

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.