VeriCAS - Verification of Fine-Grained Concurrent Algorithms
|Projektträger:||DFG (Deutsche Forschungsgemeinschaft)|
|Projektverantwortung vor Ort:||Bogdan Tofan|
|Beteiligte Wissenschaftler der Universität Augsburg:||
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 list of publications is given below. The KIV projects can be found here. Proving linearizability with temporal logic.
S. Bäumler, G. Schellhorn, B. Tofan, and W. Reif.
Journal Formal Aspects of Computing (FAC), 23(1):91–112, 2011.
 Mechanically veriﬁed proof obligations for linearizability.
J. Derrick, G. Schellhorn, and H. Wehrheim.
Journal ACM transactions on Programming Languages and Systems, 33(4):1–43, 2011.
 Verifying linearisabilty with potential linearisation points.
J. Derrick, G. Schellhorn, and H. Wehrheim.
In Proc. of Formal Methods (FM), pages 323–337. Springer LNCS 6664, 2011.
 How to prove algorithms linearizable.
G. Schellhorn, J. Derrick, and H. Wehrheim.
In Proc. of CAV, Vol. 7358, pages 243–259. Springer LNCS, 2012.
 RGITL: A temporal logic framework for compositional reasoning about interleaved programs.
G. Schellhorn, B. Tofan, G. Ernst, J. Pfähler, and W. Reif.
Journal Annals of Mathematics and Artiﬁcial Intelligence (AMAI), accepted, 2013.
 Interleaved programs and rely-guarantee reasoning with ITL.
G. Schellhorn, B. Tofan, G. Ernst, and W. Reif.
In Proc. of Temporal Representation and Reasoning (TIME), IEEE, CPS, pages 99–106, 2011.
 Temporal logic veriﬁcation of lock-freedom.
B. Tofan, S. Bäumler, G. Schellhorn, and W. Reif.
In Proc. of MPC 2010, Springer LNCS 6120, pages 377–396, 2010.
 Compositional veriﬁcation of a lock-free stack with RGITL.
B. Tofan, G. Schellhorn, G. Ernst, J. Pfähler, and W. Reif.
In Proc. of AVoCS, submitted. ECEASST, 2013.
 Formal veriﬁcation of a lock-free stack with hazard pointers.
B. Tofan, G. Schellhorn, and W. Reif.
In Proc. of ICTAC, pages 239–255. Springer LNCS 6916, 2011.
 Two approaches for proving linearizability of multiset.
B. Tofan, O. Travkin, G. Schellhorn, and H. Wehrheim.
Journal Science of Computer Programming, submitted, 2013.
 Proving linearizability of multiset with local proof obligations.
O. Travkin, H. Wehrheim, and G. Schellhorn.
In Proc. of AVoCS, Vol. 53. ECEASST, 2012.