Verification of Herlihy & Wing's Queue as an Instance of the Complete Refinement Theory for Linearizability
This page describes KIV proofs that verify Herlihy & Wing's queue (defined in [HeWi90]).
This queue implementation, though not of practical interest, is despite its algorithmic simplicity
a particularly hard example to prove linearizability. The original proof in [HeWi90] is rather complex. It uses
auxiliary data (a partial order), Owicki-Gries style reasoning and assumes without loss of generality, that all
queue elements are different. The latter assumption is particularly hard to imitate in a formal proof.
Our proof uses the refinement theory for linearizability described
here.
According to the completeness result given there, it should be possible to prove any linearizable
algorithm using backward simulation, and indeed our proof demonstrates that.
It constructs a backward simulation without using any auxiliary data.
Both the completeness proof for backward simulation and the verification of the queue
have been published in [CAV12].
To get an overview over the specifications, have a look at
the toplevel overview,
which shows the structure of the specifications as a development graph.
The following specification are important:
-
The algorithms are defined over the concrete state
is a tuple consisting of
- an (infinite) array AR, defined as a function from natural number to
elements,
that include a special 'empty' element.
- a back pointer (a natural number), that points to the highest element used.
- a local variable pcf(p) for every process p ∈ Proc, that gives
program counter value.
pcf(p) = N indicates, that process p is not running an operation.
- a local variable kf(p) for every process p ∈ Proc, that mimics the counter i of the for loop in dequeue in [HeWi90].
- a local variable lbackf(p) for every process p ∈ Proc, that stores the local copy of the back counter.
- a local variable lanf(p) for every process p ∈ Proc, that stores the element to enqueue in the enqueue algorithm,
and the dequeued element in the dequeue algorithm.
-
HWQ-COP
defines the individual steps of the enqueue and the dequeue algorithm as relations COp(p, j) over the state. p is the process
executing the step, and j is from this index set. The index set roughly corresponds to pc values, except that for if statements two operations (e.g. deq2t and deq2f)
are used and two additional invoking operations Enq0 and Deq0 are needed.
All steps of the algorithms are specified using a precondition (typically a test for being at the right pc value)
and an update function (called Enq0, .., Enq3, Deq0, ..., Deq6), which compute the modified state. The encoding of the algorithms
into operations should become clear from the followig pseudocode:
ENQUEUE(lan)
E1 : k := back, back := back +1 /* INCREMENT */
E2 : AR(k) := a /* STORE */
E3 : return
DEQUEUE
D1 : lback := back, k := 0, lan := empty
D2tf : if k < lback goto 3 else goto 1
D3 : a := AR(k), AR(k) := a /* SWAP */
D4tf : if lan = empty then goto 6 else goto 5
D5 : k := k + 1; goto 2
D6 : return(lan)
- The specification also contains three additional operations used by the abstraction function:
- NDeq(n, cs) computes the state, that would result from running the dequeue algorithm as one atomic step,
i.e. it deletes the lowest, nonempty element at position n in an array, if it exists.
preNDeq(n,cs) is its precondition. (eb(AR,m,n) states, that the array is empty between m and n).
- PDeq(p, n, cs) computes the state, that would result from running a "pending" dequeue process p to the end (in one step).
A pending dequeue process is one that has already initialized its local variables
(executed D1), but not yet dequeued an element (non-empty-swap at line D3).
It dequeues the next non-empty element AR(n) above kf(p). Precondition PrePDeq(p,n,cs)
is used to check, that p is indeed such a pending dequeue process, and n the right index.
- Similarly, PEnq(p, cs) executes a "pending" enqueue process to the end. An enqueue process p
is pending, when it has incremented back, but not yet inserted its element, i.e. when pcf(p) = E2.
The effect is the same as Enq3(Enq2(cs)).
- On the abstract level
two operations are used to atomically enqueue and dequeue an element from an
algebraic queue (which is just a renaming of lists: the empty queue is 'emq', enqueue operation 'enq(x,a)' attaches element 'a' to the end of the list, 'deq(x)' removes the first element).
- abs-runs defines the auxiliary function abs, which maps indices of concrete steps to the corresponding index (deqi or enqi) of the abstract operation
they implement (e.g. abs(deq2t) = deqi), and the auxiliary function runs, which maps pc values to enqi, deqi or SKIP.
- Specification INV defines an invariant INV for the system, which consists of several parts:
- first there are three technical invariants: the history is always legal (legal(H)), there is always a finite number
of running processes (nonidles(H, cs)) and the pending invokes of the history fit to the running processes (HINV(H,cs)):
process p runs the dequeue algorithm, iff history H contains a pending invoke inv(p, deqi, empty); it runs enqueue of an element
a (stored in lanf(p)), if there is a pending invoke inv(p, enqi, a).
- GINV(AR,back) simply states that the array AR is empty above back.
- CSINV(cs) is the main invariant: it consists of a local invariant LCSINV for every process p, and a disjointness property D
between the local states of two processes p and q. LCSINV contains simple properties of the local variables, e.g. lanf(p) is always nonempty,
when the process is in the enqueue algorithm at E1 or E2. Disjointness property D is more interesting: it says that no two processes
enqueue at the same place, and that a process p never enqueues at a place, where a dequeue process q has just dequeued
(i.e. if pcf(q) = D4 and lanf(q) is nonempty, or if pcf(q) = D6).
-
The invariance proof for INV
is proven as a theorem over the specification. The proof immediately splits into one case for each operation, and is rather simple.
We also prove that INV is
invariant in NDeq,
PDeq,
and PEnq.
- The difficult part to get right is the
abstraction relation
ABS(cs,es,x). ABS can be viewed as a function, that returns for every concrete state cs a set of pairs (es,x), where x is a possible
queue that the current state represents, and where es is the specific set of return events for processes, which must have linearized, to have
the current state represent the specific queue x. The following key observations are necessary:
- It is necessary to view all pending enqueue processes (pc = E2) as having potentially linearized (see the [FM2011] paper for a definition).
They have definitely linearized, after inserting their element (pc = E3).
- In contrast, dequeue operations definitely linearize at D3, when they swap with a non-empty array element.
- To get the possible current queues that a state represent, it is sufficient to compute all possible observations, that
can result from observing the current state by
- executing new dequeues (NDeq),
- executing pending dequeues to the end (PDeq),
- executing pending enqueues (PEnq).
- These operations must be executed in any order (nondeterministically), until the array is empty.
- For each such run, the observed results of dequeue operations (both PDeq and NDeq's) gives a possible current queue,
and the executed PEnq operations determine those enqueue operations, which have linearized.
- The definition of ABS is defined as a recursion following this idea:
- The base case is an empty array, which represents the empty queue.
The return events are for those processes that have definitely linearized.
These are computed by 'outs'. They contain all enqueues with pc = E3, and all dequeues (at D4 or D6),
which already have already successfully swapped.
- The three recursive cases are for executing the three cases NDeq, PDeq, and PEnq.
The recursion is well-founded, since each operations either decreases the number (#ne)
of nonempty array elements or the number of pending enqueues (#pw). The resulting
well-founded order #abs is shown to
decrease in NDeq
PDeq, and
PEnq.
- The potential linearization points for enqueue processes makes the definition of ABS asymmetric. If PEnq(p,cs) is executed,
the return event ret(p,enqi,empty) is added to the linearized operations, but the queue is not modified (since nothing is observed).
executing PDeq, however, does not add to the set es, since the dequeue process will linearize in the future.
Instead, PDeq and NDeq add to the queue, but leave the set of linearized return values unchanged.
- The main proofs that ABS indeed defines a backward simulation that satisfies the
proof obligations for linearizability are done over specification ABS.
The main proofs in the
theorem base of the toplevel specification mainly puts lemmas, proved in specifications below, together.
- The main proofs of backward simulation for every operation of the algorithms are named
deq0-corr, deq1-corr, ..., deq6-corr, enq0-corr, enq1-corr, ... enq3-corr in the
theorembase of ABS.
- All the proofs are by induction over #abs(cs). In most proofs the potential (x,es) pairs do not change,
since they are no linearization steps. For those we must prove that any pair (x',es') pair after the step
is a possible pair before the step. These proofs unwind ABS in the antecedent and succedent, which results
in 4 subgoals. Usually these can be immediately closed with the induction hypothesis, based on simple commutativity properties
for the operations of the algorithms (e.g. Deq1) with the operations NDeq, PDeq, PEnq.
As an example NDeq(n, Deq1(p, cs)) = Deq1(p, NDeq(n, cs)) holds. Most of these commutativity properties
are
in the theorembase of HWQ-COP, a few (that require INV) are in
the theorembase of INV. Most are applied automatically as rewrite rules.
- A few proofs are more difficult:
- For deq3-corr two complementary cases are proved:
deq3-nonemptyswap-corr proves the case where a nonempty element is swapped. Interestingly, this case is easy, it just
requires a
lemma, that an already linearized dequeue can be forward simulated too (for the case of the proof, where PDeq(p,...) with the same p is executed).
The hard case is that
of an empty swap. In particular, an empty swap at position n does not commute with PEnq for the same array element.
We first prove
the subcase, when no PEnq for position n exists. Based on that, we can prove the case PEnq(p0,Deq3(p,cs))
as a separate inductive lemma. The crucial lemmas are that
PDeq
as well as
Ndeq
commute suitably with PEnq;Deq3, such that either the induction hypothesis becomes applicable, or the lemma for the already
proved subcase closes the goal. The crucial arguments is, that there can not be a second pending enqueue process for the same array position.
-
enq2-corr is dual to the nonempty-swap case of deq3. It also needs a
lemma,
that ensures that executing Enq3 does not change the possible (x,es) pairs.
- The most complex proof is that for the increment operation Enq1(p,cs), where the enqueue algorithm potentially linearizes. We get two
cases. The
easy case
is the one where the operation does not linearize, i.e. when ABS computes a pair (y,es'), where es' does not contain
a return event for p. In the
hard case, ABS computes a queue y, where PEnq(p) has been executed.
Then the enqueued element 'a' can end up in various positions of the queue y computed by ABS.
The proof has to make sure, that the queue can be split up as 'y = x1 + x2' (where + concatenates),
such that x1 contains all the curent array elements (plus some pending enqueues, executed before the one for p),
while x2 starts with 'a' and contains elements only, that were enqueued
by other pending enqueues. Then x1 is a possible queue representation before the step and it is sufficient
to execute enqueue operations on the abstract level that enqueue the elements of x2 in sequence (with DPoss(...x1,...,y)).
The hard case is the one, where ABS executes PEnq for p,i.e. where PEnq(p,Enq1(p,cs)) has to be considered.
This case is proved separately (as always by induction over #abs). Two lemmas are needed, that
NDeq
and
PDeq
commute with Enq1; PEnq. These close the PDeq and the NDeq case of ABS.
The PEnq case is trivial, since two PEnq's always commute (they insert at different array positions).
The hard case now is the base case,
where the array is empty, defined as lemma
emptyAR-lem.
It says that for an empty array, the abstraction function can yield exactly all subsequences of elements, for which pending enqueues exist.
While this is perfectly intuitive, it is not provable by induction over #abs, since executing a PEnq would result in a nonempty
array, which prevents application of the induction hypothesis.
The right generalization is lemma lastq-is-AR-or-enq, which states that for any cs, if ABS(cs) returns a pair (enq(x,a),es), then either
- 'a' will be some array element, and removing this array element will result in (x,es) being a possible result of the abstraction
function, or
- 'a' is the element lanf(p0) of a pending enqueue p0 and the abstraction function can also return (x, es -- ret(p,enqi,empty)),
(where -- removes an element from a set).
With this lemma, the proof of emptyAR-lem is possible by induction over the length of the returned queue x,
using lastq-is-AR-or-enq as the induction step (and there is no need to unfold ABS).
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.