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:
- A definition of linearizability and a proof that linearizability is implied by
an inductively defined predicate of possibilities.
- A specific instance of data refinement is set up such that refinement correctness
coincides with linearizability.
- The local proof obligations for one process we give in Section 3 of [FMOODS08]
are defined.
- It is shown that these proof obligations imply a forward simulation using possibilities
for the full scenario of running an arbitrary number of interleaved processes.
- Since the forward simulation implies refinement correctness for the refinement defined above,
the proof obligations are sufficient to prove linearizability.
- Finally we show that the local proof obligations are satisfied for the
lock-free stack algorithm.
The development is organized into three projects:
- A small generic theory of data refinement
according to Hoare and He.
Specification forward
gives the proof obligations of forward simulation, and
forward-is-refine proves that they imply refinement, as defined in
refine.
- The generic theory of non-atomic refinement, which implies linearizability. This project consists of three parts:
- A formal definition of linearizability as a predicate on lists of
invoke and return events.
A number of auxiliary predicates (legal histories, sequential histories, matching pairs of invokes and returns, pending invokes) are used.
We
prove, that linearizability can be expressed in terms of
possibilities.
Possibilities were defined in [HeWi90], and we prove a formal equivalent of
Theorem 9. Instead of writing "<v,P,R> in Poss(H)" we define an equivalent predicate "Poss(H,R,v)".
The parameter P was dropped, since it is redundant (it is the just the set of pending invokes of H). Explicit constraints,
that all histories considered must be legal had to be added in many formal definitions, and the inductive proof
requires
a generalization. The proof splits into three cases (invoke,
do,
return), the second case being rather complex due to the many cases that must be considered.
- The second part of the development defines
the local proof obligations of Section 3 of [FMOODS08], based on
abstract and
concrete operations of a single process. Two data types that instantiate data refinement
are created by lifting the operations to an arbitrary number of processes
here and
here. The embedding indexes operations with processes p and gives each process its own local state lsf(p) on the
concrete level.
Operations now also create a history:
abstract operations add an invoke and a return event, thus creating sequential histories.
Those concrete operations which are invokes and returns add an invoke resp. a return event.
- The third part brings together the operations and a specific instance of data refinement, that guarantees linearizability.
To do this, concrete finalization is defined to be identity on histories (so the global state for both data types is
histories). Abstract finalization holds between an abstract and a concrete history, iff the concrete
history is linearizable to the abstract one. For
these definitions, refinement and linearizability are equivalent.
To prove that linearizability follows from the proof obligations, we
define a forward simulation (names FS in [FMOODS08], called fullR here)
based on possibilities and the relation R used in the local proof obligations. The main proof obligations
for forward simulation are
proved over this theory. Finally, specification
lockfree-is-refinement gives the mapping to the generic data refinement theory of the first project.
- The third project is the case study of the lock-free stack as described in [FMOODS08].
We define an abstract stack with push and pop operation (based on a library specification of lists), and
the lock-free implementation.
The simulation relation R and the necessary status function are defined. Finally, we
prove that the local proof obligations from the second project are satisfied
by the case study. This implies that the implementation of the stack is indeed linearizable.
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.