Name
Abstract | ||
|---|---|---|
Linearizability is a global correctness criterion for concurrent systems. One technique to prove linearizability is applying a composition theorem which reduces the proof of a property of the overall system to sufficient rely-guarantee conditions for single processes. In this paper, we describe how the temporal logic framework implemented in the KIV interactive theorem prover can be used to model concurrent systems and to prove such a composition theorem. Finally, we show how this generic theorem can be instantiated to prove linearizability of two classic lock-free implementations: a Treiber-like stack and a slightly improved version of Michael and Scott’s queue. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/s00165-009-0130-y | Formal Asp. Comput. |
Keywords | Field | DocType |
kiv interactive theorem prover,classic lock-free implementation,temporal logic,concurrent system,lock-free,composition theorem,compositional reasoning,improved version,overall system,generic theorem,proving linearizability,verification,sufficient rely-guarantee condition,rely-guarantee,linearizability,global correctness criterion,single process,theorem prover,lock free | Linearizability,Discrete mathematics,Gödel's completeness theorem,Non-blocking algorithm,Computer science,Queue,Correctness,Theoretical computer science,Temporal logic,Compactness theorem,Proof assistant | Journal |
Volume | Issue | ISSN |
23 | 1 | 1433-299X |
Citations | PageRank | References |
16 | 0.71 | 36 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Simon Bäumler | 1 | 116 | 5.89 |
| Gerhard Schellhorn | 2 | 769 | 56.43 |
| Bogdan Tofan | 3 | 86 | 4.93 |
| Wolfgang Reif | 4 | 915 | 95.46 |