VeriCAS

VeriCAS - Verification of Lock-Free Concurrent Algorithms

The efficient control of concurrent access to shared resources is a major topic in computer science which has become even more important with the spread of multi-core computers. The classic approach to ensure consistency, mutual exclusion, is well understood but typically can not make use of the capacity of modern multicore computers and suffers from severe problems such as deadlocks. Lock-free algorithms are a class of concurrent algorithms designed to avoid these shortcomings. They can ensure a comparable performance to that of lock-based implementations under no contention or multiprogramming, and outperform them significantly otherwise, while ensuring global progress in the presence of arbitrary process failures or delays. This is typically achieved by applying synchronization primitives such as CAS (Compare And Swap) and an optimistic try and retry scheme. The application domain of these algorithms ranges from managing multiprocessor communication to real-time gaming or hash tables for the efficient indexing in distributed databases or webservers.

The main concern of this project is the verification of current lock-free implementations of different multithread-safe data structures. The analysis focuses on the main correctness and liveness properties of these algorithms: The main correctness condition, linearizability, ensures that lock-free operations can be seen as atomic from an external point of view, i.e. they either take place in one step or they have no visible effect. The main liveness property, lock-freedom, guarantees that even in the presence of process failure, one of the currently active operations terminates.

The project defines a new approach for the integrated development and analysis of lock-free algorithms in the interactive theorem prover KIV. The technique embeds the main properties linearizability and lock-freedom in a verification approach based on refinement to allow for the modular development of correct software. Based on a generic and expressive temporal logic framework for the verification of concurrent algorithms, proof obligations can be deduced and instantiated to verify algorithms using automated verification techniques. In particular, the approach shall meet the following expectations:

• Specification of lock-free algorithms at different levels of abstraction.
• Development of a refinement theory which translates linearizability and lock-freedom to process-local proof-obligations.
• Interactive verification of these proof-obligations, as well as the decomposition of global properties to process-local proof-obligations, in an expressive temporal logic framework.
• Integration of different automation techniques for the analysis of algorithms. In particular, we would like to consider techniques such as Shape Analysis, Ownership or Atomicity Analysis.

Compared to other existing approaches our technique integrates the mechanized specification, decomposition of global properties and the proof of the resulting process-local proof obligations (which imply linearizability and lock-freedom) into one calculus. Using interactive theorem proving, scaling problems from which automated techniques suffer can be reduced, while these techniques can be applied to reduce the number of required interactions.

First steps have already been made to fulfill these goals. In [FACJ09] we describe a generic composition theorem which reduces the proof of linearizability to sufficient rely-guarantee conditions for single processes and its application to a classic lock-free stack algorithm. In [MPC10] we describe a generic decomposition for lock-freedom and its application to a well known lock-free queue algorithm. The KIV projects can be found here.

[FACJ09] Proving Linearizability with Temporal Logic
S. Bäumler, G. Schellhorn, B. Tofan, W. Reif,
Formal Aspects of Computing 2009, Springer.

[VLL09] Verifying Linearizability and Lock-Freedom with Temporal Logic
B. Tofan, S. Bäumler, G. Schellhorn, W. Reif,
Technical Reports / Universität Augsburg.

[MPC10] Temporal Logic Verification of Lock-Freedom
B. Tofan, S. Bäumler, G. Schellhorn, W. Reif,
In Proc. of the Conference on Mathematics of Program Construction (MPC) 2010, Springer, LNCS 6120.

[ERG10] Embedding Rely-Guarantee Reasoning in Temporal Logic
B. Tofan, S. Bäumler, G. Schellhorn, W. Reif,
Technical Reports / Universität Augsburg.