Commit 2046802e authored by Glen Mével's avatar Glen Mével
Browse files

ICFP21 paper: use the theorem env for the pipeline proof

parent 2021d9ed
......@@ -5,7 +5,13 @@
% TODO : écrit à l'arrache, améliorer.
The proof of the presented specification for the pipeline uses the invariants presented in \fref{fig:pipeline:inv}.
We know prove the following result.
The code shown in~\fref{fig:pipeline:impl} satistfies the specification appearing in~\fref{fig:pipeline:spec}.
The proof uses the invariants presented in \fref{fig:pipeline:inv}.
More precisely, $\pipelineInv R$ join together the queue invariant $\queueInv$ with the pipeline internal invariant $\pipelineInvInner R$.
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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment