Name
Abstract | ||
|---|---|---|
Concurrent objects are inherently complex to verify. In the late 80s and early 90s, Herlihy and Wing proposed linearizability as a correctness condition for concurrent objects, which, once proven, allows us to reason about concurrent objects using pre- and postconditions only. A concurrent object is linearizable if all of its operations appear to take effect instantaneously some time between their invocation and return. In this article we define simulation-based proof conditions for linearizability and apply them to two concurrent implementations, a lock-free stack and a set with lock-coupling. Similar to other approaches, we employ a theorem prover (here, KIV) to mechanize our proofs. Contrary to other approaches, we also use the prover to mechanically check that our proof obligations actually guarantee linearizability. This check employs the original ideas of Herlihy and Wing of verifying linearizability via possibilities. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1145/1889997.1890001 | ACM Trans. Program. Lang. Syst. |
Keywords | Field | DocType |
concurrent object,proof obligation,refinement,concurrent access,concurrent implementation,verifying linearizability,simulation-based proof condition,proposed linearizability,theorem proving,kiv,effect instantaneously,correctness condition,nonatomic refinement,linearizability,z,theorem prover,original idea | Atomicity,Linearizability,Programming language,Computer science,Correctness,Automated theorem proving,Proof theory,Theoretical computer science,Mathematical proof,Gas meter prover,Linearization | Journal |
Volume | Issue | ISSN |
33 | 1 | 0164-0925 |
Citations | PageRank | References |
28 | 0.98 | 34 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| John Derrick | 1 | 120 | 8.80 |
| Gerhard Schellhorn | 2 | 769 | 56.43 |
| Heike Wehrheim | 3 | 1013 | 104.85 |