figure-pipeline-inv.tex 2 KB
Newer Older
Glen Mével's avatar
Glen Mével committed
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's avatar
Jacques-Henri Jourdan committed
80
81
\Description{Internal invariants of the pipeline.}
\caption{Internal invariants of the pipeline}
82
\label{fig:pipeline:inv}
Glen Mével's avatar
Glen Mével committed
83
\end{figure}