Name
Abstract | ||
|---|---|---|
Lock-free implementations of data structures try to better utilize the capacity of modern multi-core computers, by increasing the potential to run in parallel. The resulting high degree of possible interference makes verification of these algorithms challenging. In this paper we describe a technique to verify lock-freedom, their main liveness property. The result complements our earlier work on proving linearizability, the standard safety property of lock-free algorithms. Our approach mechanizes both, the derivation of proof obligations as well as their verification for individual algorithms. It is based on an encoding of rely-guarantee reasoning using the temporal logic framework of the interactive theorem prover KIV. By means of a slightly improved version of Michael and Scott's lock-free queue algorithm we demonstrate how the most complex parts of the proofs can be reduced to relatively simple steps of symbolic execution. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-13321-3_21 | MPC |
Keywords | Field | DocType |
complex part,high degree,lock-free queue algorithm,lock-free implementation,lock-free algorithm,earlier work,main liveness property,temporal logic verification,improved version,standard safety property,data structure,theorem prover,verification,temporal logic,linearizability | Data structure,Discrete mathematics,Programming language,Computer science,Runtime verification,Theoretical computer science,Mathematical proof,Symbolic execution,Temporal logic,High-level verification,Liveness,Proof assistant | Conference |
Volume | ISSN | ISBN |
6120 | 0302-9743 | 3-642-13320-7 |
Citations | PageRank | References |
10 | 0.56 | 28 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Bogdan Tofan | 1 | 86 | 4.93 |
| Simon Bäumler | 2 | 116 | 5.89 |
| Gerhard Schellhorn | 3 | 769 | 56.43 |
| Wolfgang Reif | 4 | 915 | 95.46 |