figure-pipeline-inv.tex 2 KB
 Glen Mével committed Mar 01, 2021 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 \begin{figure} $\begin{array}{rcl} % the queue: \gqueue & : & ... % \authm requires an unitary cmra; here we omit \optionm \\ % cursors of f and g: \gcurf,\;\gcurg & : & \authm(\exm(\nat)) % \authm requires an unitary cmra; here we omit \optionm \\ \hline % invariant (outer): \pipelineInv R & \eqdef & \Exists \queue, \gqueue, \gcurf, \gcurg. \queueInv \isep \knowInv{}{\pipelineInvInner R} \\ % invariant (inner): \pipelineInvInner R & \eqdef & %\\ %\multicolumn{3}{r}{% \left\{\begin{array}{l} \Exists \curf, \curg, \yElemViewListInv<\curg><\curf>*[]. \\ \quad \ISep{% \curg \leq \curf \isep \ownGhost \gcurf {\authfull \curf} \isep \ownGhost \gcurg {\authfull \curg} \cr \isQueue \emptyview \emptyview {\yElemViewListInv<\curg><\curf>} \cr \displaystyle\Sep_{\curg \leq \idx < \curf} \left(\wpre {g\;\yElem_\idx} {\Lam z. R\;\idx\;z}\right) \opat \view_\idx }%end of the main \ISep of the invariant \end{array}\right.% end of the definition of \queueInvInner %}% end of \multicolumn \\ \hline % invariant local to thread f: \pipelineF R \curf \refXArray \xElemList & \eqdef & \ISep{% \curf \leq \nbelems \isep \ownGhost \gcurf {\authfull \curf} \cr \arraypointstoNA \refXArray \xElemList \cr \displaystyle\Sep_{\curf \leq \idx < \nbelems} \wpre {f\;x_\idx} {\Lam y. \wpre {g\;y} {\Lam z. R\;\idx\;z}} } \\ \hline % invariant local to thread g: \pipelineG R \curg \refZArray \zElemList & \eqdef & \ISep{% \curg \leq \nbelems \isep \ownGhost \gcurg {\authfull \curg} \cr \arraypointstoNA \refZArray \zElemList \cr \displaystyle\Sep_{0 \leq \idx < \curg} R\;\idx\;z_\idx } \end{array}$  Jacques-Henri Jourdan committed Mar 01, 2021 80 81 \Description{Internal invariants of the pipeline.} \caption{Internal invariants of the pipeline}  Glen Mével committed Mar 02, 2021 82 \label{fig:pipeline:inv}  Glen Mével committed Mar 01, 2021 83 \end{figure}