Academic
Publications
Mechanically verified proof obligations for linearizability

Mechanically verified proof obligations for linearizability,10.1145/1889997.1890001,ACM Transactions on Programming Languages and Systems,John Derrick

Mechanically verified proof obligations for linearizability   (Citations: 2)
BibTex | RIS | RefWorks Download
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.
Journal: ACM Transactions on Programming Languages and Systems - TOPLAS , vol. 33, no. 1, pp. 1-43, 2011
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...To verify linearizability [11] and [13] give modular proof obligations, that reduce the problem to two processes by exploiting their symmetry...

    Gerhard Schellhornet al. Formal Verification of Lock-Free Algorithms

    • ...The technique extends our previous approach [4,5] to cope with the class of algorithms like the lazy set...
    • ...1 Line R2b is the only modification of remove compared to the pessimistic version studied in [5]...
    • ...These operations are then promoted (using the same standard schema as in [5]) to operations COp j on CS for each process p ∈ P , which work on the local state lsf (p)...
    • ...Our proof technique introduced in [4] and further elaborated in [5] relies on a proof of linearisability via refinement...
    • ...For some simpler classes of algorithms (e.g., stack and non-lazy set considered in [5]), LPs can be determined from the current state of a process (basically, its program counter), and in our methodology are fixed by defining a so-called status function assigning values from a type STATUS :...
    • ...With the help of the status function we define specific status-dependent proof obligations in [4,5]...
    • ...The proof obligations in [5] are particular instances of forward simulations...
    • ...For our case study, the proof obligations of [5] are sufficient to verify the add and remove operation, where the LP can be identified in the code...
    • ...Defining the invariants: As in [5], in addition to the abstraction function our theory requires a local invariant INV on GS × LS to capture constraints which are always valid in our linked list implementation (e.g., that tail is always reachable from head)...
    • ...The latter point requires an extension to the theory developed in [5]...
    • ...Many of these instances are similar to the ones for verifying the pessimistic algorithm in [5]...
    • ...With these instances the verification of the proof obligation (LPO) in KIV is now only slightly more difficult than for the pessimistic case, and the additional complexity is solely due to the more complex invariant NODEINV . The technical encoding of Z schemata in KIV is the same as described in Section 7 of [5]...

    John Derricket al. Verifying Linearisability with Potential Linearisation Points

Sort by: