Linearizability proofs for two lock-free algorithms

Compared to the KIV proofs documented here for the original FMOODS paper these improvements have been made:

• The local simulation relation R(as,gs,ls) has been split into a pure abstraction relation ABS(as,gs) and and an invariant INV(gs,ls). This allows to separate the side conditions that "no other processes are affected" (\forall lsq ...) that we had in the ( original proof obligations beforesync, aftersync etc. into separate invariance conditions for all operations invariant_and_D-invoke/intern/return. Essentially we get Owicki-Gries style proof obligations now, the invariance conditions express noninterference between processes.
• The theory has been enhanced with a disjointness predicate D(ls1,ls2). This is used (and necessary) to indicate that two references are disjoint. It seems this is sufficient to imitate ownership of pointers.
• The lock-free stack has been implemented over a memory with references to cells containing an integer and a next-reference.

The development is organized into four projects, the first two give a generic theory that embeds linearizability into data refinement and defines proof obligations.

The second two projects give two applications. A lock-free stack, and a lock-free set implemenation based on pressimistic small-grained locking.

In detail the projects are:

• A small generic theory of data refinement according to Hoare and He (but with partial operations allowed). 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, matchin pairs of invokes and returns, pending invokes) are used. We prove, that linearizability can be expressed in terms of possibilities. Possibilities were defined in Herlihy and Wing's original paper, so we prove a formal equivalent of their 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 proof obligations for concrete operations (improving those of the paper) , based on abstract and concrete operations of a single process. The proof obligations use the following three predicates with parameters gs (for the global state consisting of globally accessible data of all processes (the heap), ls (the local variables of one process) and as (the abstract state; in the two case studies a stack and a set respectively):
    • ABS(as,gs): This is the abstraction relation, that checks whether the pointer structure is indeed a valid represenation of the abstract type.
    • INV(gs,ls): An invariant stating various properties of the states of the algorithms.
    • D(ls1,ls2): A disjointness property between two local states: this is typicaly used to say that new allocated memory is unaccessible for others processes before inserting it into the global data structure. In the set case study the predicate is also used to say that removed cells (that some local variable still references) are disjoint from the new ones and other removed ones.
    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 linearizabilty. 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 (called fullR) based on possibilities and the relations ABS, INV, D used in the proof obligations. The main proof obligations for forward simulation are shown 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 on a lock-free implementation of sets using fine-grained locking (taken from [VHHS06]). The memory model used for this case study as well as the next is based on the specification store from the library. stores are partial functions with finite domain (represented first-order). Based on an empty store (the nowhere defined function), a new "key"-"value" pair is added to a store "st" (or the store is updated, if there is already a value stored under key) with "st[key,value]". "key \in st" checks if a value is stored under key (i.e. whether key is in the domain) and "st[key]" applies the function to get the value stored under key (the functions is unspecified if key is not allocated). For the memory model we first define an abstract memory model of linear heaps. This memory model fixes the keys of the store to use references which include a null reference. The values in the memory are just specified to have a ".nxt" reference, leaving open their exact content. Over this specification it is possible to derive basic facts about paths and reachability. For the case study we need memory cells consisting of a integer (which may also be onbe of the special values "+/-infinity"), a lock (a process id) and a next pointer. Based on the memory model the operations of the fine grained locking algorithm are defined. Similarly, based on a library specification of sets the abstract operations are defined. The predicates ABS, INV, and D, together with the status function (and the auxiliary runs functions) are defined here. Finally, we prove that the proof obligations as given in the second project are satisfied for the case study, which implies that the implementation of the stack is indeed linearizable.
• The fourth project is the case study described on lock-free stacks as described in our paper, but with an implementation that is based on the memory model of the previous project. This time memory cells are a pair of an element and a .nxt pointer. We define an abstract stack with push and pop operation (based on a library specification of lists), and the lock-free implementation. The relations ABS, INV, D and the necessary status function are defined here. Finally, we prove that the proof obligations as given in the second project are satisfied by the case study, which implies that the implementation of the stack is indeed linearizable.
• The fifth project is a second case study on a set implementation with fine grained locking as described in our paper. In this case study memory cells are a triple of an integer or infinity, a process id or none that is used for locking, and a .nxt reference. We define abstract sets with an insert and a remove operation (based on a library specification of sets), and the lock-free implementation. The relations ABS, INV, D and the necessary status function are defined here. Finally, we prove that the proof obligations as given in the second project are satisfied by the case study, which implies that the implementation of the stack is indeed linearizable.

• The basic KIV library with basic data types

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.

Bibliography

[Imprint] [Data Privacy Statement] [E-Mail]