@@ -10,5 +10,5 @@ More precisely, $\pipelineInv R$ join together the queue invariant $\queueInv$ w

In addition, $\pipelineF R \curf\refXArray\xElemList$ and $\pipelineG R \curg\refZArray\zElemList$ are loop invariants used in the two computing threads.

The pipeline invariant uses the ghost variables $\gcurf$ and $\gcurg$ to agree with the loop invariants on their position, and, in addition to owning the exclusive ownership of the queue, states that each element of the queue is associated with a weakest precondition assertion at the element's view allowing to execute the function $g$ on this element.

Once the invariants are stated and initialized, the proof is a straightforward induction over the length of the input stream: at each step of each thread, we execute either $f$ or $g$, we open the global pipeline invariant around the logically atomic triple of the enqueing or dequeueing operation.

Once the invariants are stated and initialized, the proof is a straightforward induction over the length of the input sequence: at each step of each thread, we execute either $f$ or $g$, we open the global pipeline invariant around the logically atomic triple of the enqueing or dequeueing operation.

When this invariant is opened, the state of the queue can be updated, and we perform an update on the ghost variables $\gcurf$ or $\gcurg$ to reflect the state change in the corresponding thread.