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.

As detailed in the 'pathways to impact', we would hope that this work has impact in a number of ways.

In terms of the specifics of the proposal the work will provide generic proof methods by which to show that concurrent algorithms are correct. This will contribute to the rapid recent interest in showing that concurrent algorithms are linearizable. In addition, we will verify that some specific algorithms are correct, with a fully mechanised proof of their correctness.

The detailed technical novelty in our work includes the following:
- a technique for verifying linearizability that can be shown to be sound,
- applicable when a process is linearized by another process, and one which can't be determined by looking forward,
- applicable to arbitrary data-structures,
- local reasoning for global properties and that supports reasoning at a local level of tightly coupled inter-process behaviour

And this will impact directly on those working in refinement, formal methods and simulation-based approaches to lock-free algorithms.

Although this project revolves around concurrent algorithms, the research will
have an impact on a much broader range of communities.
Specifically, those working on mechanized verification in numerous fields and the use of refinement will benefit from the work of the project. This impact will take place mostly through the academic research community.

In a wider context the technical contribution of our work will be felt in the mechanized proof community as well as in other communities striving to verify concurrent algorithms, such as those working on shape analysis and separation logic.

In our plans we have included a wide range of potential dissemination venues covering different research communities in order to engage with those for which this work might have an impact. This includes general formal methods forums, as well as those whose interest lies in refinement or verification of concurrent algorithms. We have costed for a number of activities (eg visits to Microsoft Cambridge) to further opportunities to collaborate on shared approaches.

In addition, we plan, via our German collaborators, to run a Dagstuhl seminar (see http://www.dagstuhl.de/en/about-dagstuhl/) bringing together those developing concurrent algorithms with those interested in their verification. Dagstuhl seminars are unique events allowing one to concentrate on the exploration of a research topic in depth, and typically involve around 30-40 academic and industrial participants. The inclusion of our German partners in this proposal, gives us a unique opportunity to run such an event.