Linearizability and a lock-free stack implementation

This page describes the KIV proofs needed for the mechanization of the theorems that are described in [FMOODS08] (see bibliography below. A preliminary version of the paper is available from the authors). Altogether the proofs verify that an algorithm implementing lock-free stacks satisfies the correctness criterion of linearizability [HeWi90]. The project developed roughly consists of the following parts: The development is organized into three projects: Used basic libraries:

Here you can find all our publications.

Back to the overview of all KIV projects.
For general informations on KIV and a download site for the whole system refer to this page.


[FMOODS08] Mechanising a correctness proof for a lock-free concurrent stack, John Derrick, Gerhard Schellhorn and Heike Wehrheim submitted to FMOODS 2008, Oslo, Norway, 2008
[IFM07] Proving linearizabilty via non-atomic refinement, John Derrick, Gerhard Schellhorn and Heike Wehrheim, Proceedings iFM 2007, Springer LNCS 3491, p. 195-214
[HeWi90] Linearizability: A Correctness Condition for Concurrent Objects, M. Herlihy and J. M. Wing, ACM Transactions on Programming Languages and Systems, vol. 12, no. 3, p. 463-492

[Impressum] [E-Mail]