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

ICFP21 paper: rewrote the section about the proof of the pipeline

parent 5cebdd9e
......@@ -9,11 +9,6 @@ REM: nouvelle limite = 27 pages sans la biblio
preuve est important parce que XXX. à ce moment, on dispose de YYY et il
faut prouver ZZZ. ça marche parce que ΩΩΩ »
- étoffer section pipeline
- remarque: dans le pipeline on n’utilise que la synchro écrivain → lecteur
- utiliser \begin{theorem}\end{theorem} ailleurs dans l’article
(p.ex. dans la section Pipeline)
RELATED WORK:
......
......@@ -3,18 +3,44 @@
\input{figure-pipeline-inv}
% TODO : écrit à l'arrache, améliorer.
We know prove the following result.
\begin{theorem}%
The code shown in~\fref{fig:pipeline:impl} satisfies the specification appearing in~\fref{fig:pipeline:spec}.
\end{theorem}%
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.
The proof relies on the assertions presented in \fref{fig:pipeline:inv}.
The persistent assertion $\pipelineInv R$ join together the internal invariant of the queue with that of the pipeline.
The two assertions $\pipelineF R \curf \refXArray \xElemList$ and $\pipelineG R \curg \refZArray \zElemList$ are owned by the threads which compute $f$ and $g$, respectively, and describe their loop invariants.
We again associate the queue to a ghost variable~$\gqueue$.
In addition, we use two ghost variables $\gcurf$ and~$\gcurg$ whose values are the current positions $\curf$ and~$\curg$ of the loops computing $f$ and~$g$, respectively. This ghost state allows both threads, while in their respecting loops, to agree with the shared invariant on these values.
At any time, we have $0 \leq \curg \leq \curf \leq \nbelems$.
\begin{itemize}
\item Indices in the range $[\curf, \nbelems)$ have not been processed by~$f$ yet. Hence, for these indices, we still have the weakest-precondition assertions~$\wpre {f\;x_\idx} {-}$ initially provided to the pipeline.
These assertions can be regarded as a permission to run $f$ once on the corresponding items.
The thread computing~$f$ owns these assertions, and it also owns the array~$\refXArray$ containing the input items.
\item Indices in the range $[\curg, \curf)$ have been processed by~$f$ but are yet to be processed by~$g$. Hence, we have consumed their initial weakest-precondition assertions, and have obtained weakest-precondition assertions $\wpre {g\;y_\idx} {-}$ as a result.
These assertions are stored in the shared invariant. The invariant also owns the queue~$\refYQueue$, whose contents are the intermediate items for exactly this range of indices.
\item Indices in the range $[0, \curg)$ have been processed by both $f$ and~$g$. Hence, we have consumed their intermediate weakest-precondition assertions, and have obtained postconditions $R\;\idx\;z_\idx$ as a result.
These are owned by the thread computing~$g$, along with the array~$\refZArray$ which contains the output items.
\end{itemize}
The key point is that the assertion $\wpre {g\;y_\idx} {-}$ has been given by the thread computing~$f$ to the invariant when enqueuing the corresponding item, and will be taken by the thread computing~$g$ when dequeuing that item.
This assertion is thus exchanged between two threads with differing views of the shared memory, and transits via a neutral ground: an objective invariant.
We make the assertion objective by specifying at which view it holds: namely, the view~$\view_\idx$ which the enqueuer had and which the dequeuer will acquire.
Therefore, we rely crucially on the enqueuer-to-dequeuer synchronization guaranteed by the queue.
With these invariant assertions correctly stated, the proof is rather straightforward.
%
When creating the pipeline, we have $0 = \curg = \curf$ and assertions~$\fname{PipeInvInner}$ and~$\fname{PipeG}$ hold trivially (the queue is empty and there are no output items computed yet);
the assertion~$\fname{PipeF}$ is constituted exactly from the preconditions of the pipeline~(\fref{fig:pipeline:spec}), and is given by the main thread to the child thread that will compute~$f$.
%
When the pipeline has completed its work, we have $\curg = \curf = \nbelems$ and the assertion~$\fname{PipeG}$ provides exactly the postcondition of the pipeline.
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 enqueuing or dequeuing 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.
Thanks to the logically atomic triples in the specification of the queue, when enqueuing (respectively, dequeuing), we can open the invariant of the pipeline and move assertions to it (respectively, from it) as already explained.
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