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. Fine-grained concurrent algorithms that use fine-grained locking or even avoid the use of locks are a class of concurrent algorithms designed to avoid these shortcomings. They typically provide good performance under no contention or multiprogramming, and outperform coarse-grained locking algorithms under high contention. Lock-free algorithms in particular, avoid deadlocks and livelocks and ensure 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, instead of locking. 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 efficient implementations of different multithread-safe algorithms, in particular data structure implementations. 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 fine-grained algorithms in the interactive theorem prover KIV. The technique embeds linearizability 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 for both linearizability and lock-freedom are derived and instantiated to verify algorithms using automated verification techniques. In particular, the approach shall meet the following expectations:

• Specification of fine-grained algorithms at different levels of abstraction.
• Development of a refinement theory which translates linearizability to process-local proof-obligations.
• Development of process-local proof obligations for lock-freedom.
• 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.

A comprehensive description of the logic RGITL can be found in this paper. The KIV projects can be found here.

Partners

Funded by

Key Facts

Start date:

01.01.2010

End date:

31.01.2016

Duration:

6 years