ISSE

Search

Mechanically verified proof obligations for linearizability

J. Derrick, G. Schellhorn, and H. Wehrheim

Mechanically verified proof obligations for linearizability

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.

ACMLink
published 2011 Journal ACM Transactions on Programming Languages and Systems (TOPLAS)

Publisher: ACM New York, Volume 33 Issue 1, Article No. 4, January 2011