Proof of Quiescent Consistency of a Diffracting Tree Queue in KIV

This page describes the proofs of quiescent consistency of the blocking queue implementation with diffracting trees, as given in our submitted paper [FM14]. We have mechanized the essential parts of the coupled simulation proof for the queue in KIV: showing that a coupled simulation exists from the augmented data type B to the abstract data type A. Here is an overview of the KIV project, its central aspects are as follows:

The General Framework:

• The specifications use parts of our previously introduced general theory of linearizability with (legal, sequential, ...) histories of events (with predicates for invoke / return events, pending invokes, matching pairs, etc.) and concrete and abstract data types (see [TOPLAS10] for details).

The Queue Algorithms:

• The abstract queue data type A defines the atomic operations AOP that enqueue / dequeue elements from an abstract list of elements (queue). The intermediate queue data type B defines the queue algorithms BOP with diffraction trees (see Fig. 2 from the paper) that work on state bs, which contains the following auxilliary variables:
  
  
  • lastqf represents the two queues in the last quiescent state (QS, where all processes are idle) as a function from booleans to queues.
  • lastebit / lastdbit is the value of the ebit / dbit (used for diffraction of enqueue / dequeue operations) in the last QS, where bits are boolean values.
  • auxqf records the two queues since the last QS plus the elements that have been enqueued since then.
  • ef / df are two lists of process ids for the processes which have enqueued / dequeued elements on the two queues since the last QS.
  • auxH is the HISTORY of concurrent invoke and return events that have occured since the last QS. This corresponds to the concurrent history H from Definition 6 in the paper.
  
  The queue algorithms in B are given as a transition system with a program counter for each process (according to function pcf), where a process can either be idle (value N) or executing one of the three enqueue / dequeue operations. Executing the invoke operations from N to E1 / D1 and the return operations from E3 / D3 to N, implicitly adds an invoke / return event to a global history H of concurrent events that have occured since the initial state of the overall concurrent system, as given by the general theory. (To slightly simplify the specification of the central proof obligation, we define two weak return operations WRETENQ and WRETDEQ: Different from the full return operations RETBOP that reset the auxiliary variables when a QS is reached, the weak return operations ignore this reset.)

  The Invariants:

• The invariants that are part of the coupled simulation relation R (see Definition 6 in the paper), are defined in specification INV based on further definitions from specification helperINV. The central invariant predicate INV consists of the following parts:
  
  
  • Subpredicates HINV, legal and nonidles define generic properties that relate the current execution of each process with the global history H, e.g., running processes have a pending invoke event in H with an input element that is equal to the input elements elf from state bs. Moreover, we state that auxH corresponds to H from its last quiescent state, i.e., hsinceq(H) = auxH.
  • Subpredicate BSINV gives relevant information about the lists and queues from bs: E.g., the current queue (i.e., queuef in bs) results from executing # df dequeues on the auxiliary queue (auxqf); the queue in the last QS (lastqf) results from deleting the last # ef enqueued elements from the end of auxqf, etc. In particular, predicate lengthINV states that the length of two queues can never differ by more than 1, taking the number of pending enqueue and dequeue operations (see functions #pe and #pd) and the corresponding enqueue and dequeue bits into account. This property holds for the current queue (queuef) and for the last and the auxiliary queues (lastqf, auxqf), respectively. Similarly, predicate lengthEDINV states that the process lists ef and df can only differ in their length by at most 1.
  • Finally, predicates invperm / retperm state that the invoke / return events of completed enqueue / dequeue operations from the concurrent history auxH, are a permutation of events that can be constructed from the process lists ef / df and the auxiliary queue auxqf, respectively.
  
  (A weak invariant WINV is defined by just dropping the property hsinceq(H) = auxH from INV.)

  The Simulation Relation R and the Sequential History HS:

• The relation R (see Definition 6 in the paper) corresponds to predicate INV and an abstraction function qshuffle(bv, qf) that is defined in specification QCQ-Corr. This function computes an abstract queue from two diffraction queues qf, by shuffling the elements of the two queues starting with qf(bv). In particular, the abstract queue q of the last QS is q = qshuffle(lastdbit, lastqf) and the abstract queue q' of the current QS is q' = qshuffle(dbit, queuef), since the lastdbit / dbit dictates from where the next dequeue operation reads.
• Functions eshuffle(bv, ef, auxqf) / dshuffle(bv, df, auxqf) from specification QCQ-Corr compute sequential histories of pairs of invoke and return events of enqueue / dequeue operations as recorded in variables ef / df, and auxqf from the last QS on. (Again, parameter bv dictates that the recursion starts with the process list ef(bv) / df(bv) and the queue auxqf(bv), respectively.) With these functions, we can define the sequential history HS from the paper (Definition 6) simply as HS = eshuffle(¬ ebit, ...) + dshuffle(lastdbit, ...), i.e., we first execute all enqueues from the last QS, starting with ¬ ebit (which defines where the last element was enqueued, note that the recursion adds the events at the end of the list) followed by all dequeues starting with lastdbit (which defines where the first dequeue operation reads from).

The Proofs:

• The proof that predicate INV is invariant over every BOP-transition is given in the theorem base of specification INV as theorem BOP-preserves-INV.
• The proof of the big commuting diagram of coupled simulations (that implies quiescent consistency for the queue) are given in the theorem base of specification QCQ-Corr. The proofs assume that the current state is quiescent and WINV holds (here, the deletion of auxH, ef and df etc. is not yet performed which slightly simplifies the specification):
• Theorem QUIESCENT-CONS-PAOP-EDshuffle shows that q ' (see above) can be reached from q by a sequence of abstract operations PAOP(q, q', [], HS) that produces the sequential history HS above from an empty history [].
• Finally, theorem QUIESCENT-CONS-AUX-EDshuffle proves that the sequential history HS above is a permutation of the history auxH of concurrent events that occured since the last QS.

Bibliography