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

make invariant more readable

parent 7d705ec1
\begin{figure}
\[\begin{array}{rcl}
% public state:
\gqueue
& : &
\authm(\exm(\typeView \times \typeView \times \typeList(\typeVal \times \typeView)))
\\
\isQueue \tview \hview \elemViewList
&\eqdef&
\ownGhost\gqueue{\authfrag \tuple{\tview, \hview, \elemViewList}}
\\
\hline
% monotonicity of statuses:
\gmonos
& : &
\listm(\authm(\statusViewBotLat))
% public state:
\gqueue
& :
& \authm(\exm(\typeView \times \typeView \times \typeList(\typeVal \times \typeView)))
\\
\monoWitness{\idx}{\pair\status\sview}
&\eqdef&
\ownGhost\gmonos{\mapsingleton{\idx}{\authfrag \pair\status\sview}}
\isQueue \tview \hview \elemViewList
& \eqdef
& \ownGhost\gqueue{\authfrag \tuple{\tview, \hview, \elemViewList}}
\\ \hline
% monotonicity of statuses:
\gmonos
& :
& \listm(\authm(\statusViewBotLat))
\\
\hline
% tokens:
\gtokens
& : &
\authm(\finmapm{\Z}{\exm(\typeUnit) + \exm(\typeVal \times \typeView)})
\monoWitness{\idx}{\pair\status\sview}
& \eqdef
& \ownGhost\gmonos{\mapsingleton{\idx}{\authfrag \pair\status\sview}}
\\ \hline
% tokens:
\gtokens
& :
& \authm(\finmapm{\Z}{\exm(\typeUnit) + \exm(\typeVal \times \typeView)})
\\
\tokenR\idx
&\eqdef&
\ownGhost\gtokens{\authfrag \mapsingleton{\idx}{\Unit}}
\tokenR\idx
& \eqdef
& \ownGhost\gtokens{\authfrag \mapsingleton{\idx}{\Unit}}
\\
\tokenW\idx{\pair\elem\eview}
&\eqdef&
\ownGhost\gtokens{\authfrag \mapsingleton{\idx}{\pair\elem\eview}}
% hide the injection \exinj and left/right injections
\tokenW\idx{\pair\elem\eview}
& \eqdef
& \ownGhost\gtokens{\authfrag \mapsingleton{\idx}{\pair\elem\eview}}
% hide the injection \exinj and left/right injections
\\ \hline
% invariant (outer):
\queueInv
& \eqdef
& \Exists \gmonos, \gtokens. \knowInv{}{\queueInvInner}
\\
\hline
% invariant:
\queueInv
&\eqdef&
\left\{
\begin{array}{l}
\Exists \gmonos, \gtokens, \reftail, \refhead, \refstatuses, \refelements.
\\\quad
\ISep{%
\queue = \Tuple{\reftail, \refhead, \refstatuses, \refelements}
\cr \knowInv{}{\queueInvInner}
}% end of \ISep
\end{array}
\right.
% invariant (inner):
\queueInvInner
& \eqdef
\\
\queueInvInner
&\eqdef&
\left\{
\begin{array}{l}
\Exists \tail, \head, \tview, \hview, \elemViewListWithLenInv,
\\ \phantom{\exists}\statusViewListWithLen.
\\\quad
\ISep{%
% pure assertions:
0 \le \tail \le \head \le \tail + \capacity
%\cr \length{\statusViewList} = \capacity
%\cr \length{\elemViewList} = \head - \tail
% pointsto assertions:
\cr \pointstoAT\reftail{\mkval\tail\tview}
\cr \pointstoAT\refhead{\mkval\head\hview}
\cr \arraypointstoAT\refstatuses\statusViewList
% authoritative ghost state assertions:
\cr \ownGhost\gqueue{\authfull \tuple{\tview, \hview, \elemViewListInv}}
\cr \ownGhost\gmonos{\mkDotList{\ANON{\authfull \nthStatusView{#1}}}\idx\capacity}
\cr \ownGhost\gtokens{%
\authfull
\left(\begin{array}{lll}
% authority for read tokens:
& \{
\mapbinding \idx \Unit
& \mid
\head-c \leq \idx < \tail
\}
\\ \uplus
% authority for write tokens:
& \{
\mapbinding \idx {\nthElemView{\idx-\tail}}
& \mid
\tail \leq \idx < \head
\}
\end{array}\right)
}
% cells which are empty or being emptied:
\cr \displaystyle\Sep_{\head-\capacity \leq \idx < \tail}
% cell bearing no value, available for next round:
\emptyCell \idx {\nthStatusView{\modcap\idx}}
\lor
% cell being emptied by a dequeuer:
\status_{\modcap\idx} = 2\idx + 1
% NOTE: here we can add 0 ≤ i to the invariant, but it is unneeded
% cells which are full or being filled:
\cr \displaystyle\Sep_{\tail \leq \idx < \head}
% cell bearing a value:
\fullCell \idx {\nthElemView{\idx-\tail}} {\nthStatusView{\modcap\idx}}
\lor
% cell being filled with a value by an enqueuer:
\status_{\modcap\idx} = 2\idx
}%end of the main \ISep of the invariant
\end{array}
\right.
\multicolumn{3}{r}{%
\left\{\begin{array}{l}
\Exists \reftail, \refhead, \refstatuses, \refelements.
\\ \Exists \tail, \tview, \head, \hview, \elemViewListWithLenInv, \statusViewListWithLen.
\\ \quad \ISep{%
% pure assertions:
\queue = \Tuple{\reftail, \refhead, \refstatuses, \refelements}
\cr 0 \le \tail \le \head \le \tail + \capacity
%\cr \length{\statusViewList} = \capacity
%\cr \length{\elemViewList} = \head - \tail
% pointsto assertions:
\cr \pointstoAT\reftail{\mkval\tail\tview}
\cr \pointstoAT\refhead{\mkval\head\hview}
\cr \arraypointstoAT\refstatuses\statusViewList
% authoritative ghost state assertions:
\cr \ownGhost\gqueue{\authfull \tuple{\tview, \hview, \elemViewListInv}}
\cr \ownGhost\gmonos{\mkDotList{\ANON{\authfull \nthStatusView{##1}}}\idx\capacity}
\cr \ownGhost\gtokens{%
\authfull
\left(\begin{array}{lllr@{\;}l}
% authority for read tokens:
& \{
\mapbinding \idx \Unit
&\mid&
\head-\capacity &\leq \idx < \tail
\}
\\ \uplus
% authority for write tokens:
& \{
\mapbinding \idx {\nthElemView{\idx-\tail}}
&\mid&
\tail &\leq \idx < \head
\}
\end{array}\right)
}
\cr \begin{array}{@{\!\!}c@{}l@{\;}c@{\;}l} % array for aligning the formulas of the two big-stars
% cells which are empty or being emptied:
\displaystyle\Sep_{\head-\capacity \leq \idx < \tail}&
% cell bearing no value, available for next round:
\emptyCell \idx {\nthStatusView{\modcap\idx}}
&\lor&
% cell being emptied by a dequeuer:
\status_{\modcap\idx} = 2\idx + 1
% NOTE: here we can add 0 ≤ i to the invariant, but it is unneeded
% cells which are full or being filled:
\\ \displaystyle\Sep_{\tail \leq \idx < \head}&
% cell bearing a value:
\fullCell \idx {\nthElemView{\idx-\tail}} {\nthStatusView{\modcap\idx}}
&\lor&
% cell being filled with a value by an enqueuer:
\status_{\modcap\idx} = 2\idx
\end{array}% end of array used to align the two big-stars
}%end of the main \ISep of the invariant
\end{array}\right.% end of the definition of \queueInvInner
}% end of \multicolumn
\\
% predicate for empty cells:
\emptyCell \idx {\pair\status\sview}
&\eqdef&
\ISep{
\status = 2(\idx + \capacity)
\cr (\nthpointstoNA\refelements{\modcap\idx}-) \opat \sview
\cr \tokenR\idx
}
% predicate for available cells:
\emptyCell \idx {\pair\status\sview}
& \eqdef
& \ISep{%
\status = 2(\idx + \capacity)
\cr (\nthpointstoNA\refelements{\modcap\idx}-) \opat \sview
\cr \tokenR\idx
}
\\
% predicate for full cells:
\fullCell \idx {\pair\elem\eview} {\pair\status\sview}
&\eqdef&
\ISep{
\status = 2\idx + 1
\cr (\nthpointstoNA\refelements{\modcap\idx}{\elem}) \opat \sview
\cr \tokenW\idx{\pair\elem\eview}
\cr \eview \viewleq \sview
}
\end{array}\]
% predicate for occupied cells:
\fullCell \idx {\pair\elem\eview} {\pair\status\sview}
& \eqdef
& \ISep{%
\status = 2\idx + 1
\cr (\nthpointstoNA\refelements{\modcap\idx}{\elem}) \opat \sview
\cr \tokenW\idx{\pair\elem\eview}
\cr \eview \viewleq \sview
}
\end{array}\]
\Description{Internal invariant of the bounded queue.}
\caption{Internal invariant of the bounded queue}
\label{fig:queue:invariant}
......
......@@ -619,9 +619,9 @@
\newcommand{\isQueueSC}[1]{\ISQUEUE\;\gqueue\;{#1}}
\newcommand{\isQueue}[3]{\ISQUEUE\;\gqueue\;{#1}\;{#2}\;{#3}}
\newcommand{\queueInv}{\fname{queueInv}\;\queue\;\gqueue}
\newcommand{\queueInvInner}{\fname{queueInvInner}\;\gqueue\;\gmonos\;\gtokens\;}%\reftail\;\refhead\;\refstatuses\;\refelements}
\newcommand{\emptyCell}[2]{\fname{available}\;{#1}\;{#2}}
\newcommand{\fullCell}[3]{\fname{occupied}\;{#1}\;{#2}\;{#3}}
\newcommand{\queueInvInner}{\fname{queueInvInner}\;\queue\;\gqueue\;\gmonos\;\gtokens}
\newcommand{\emptyCell}[2]{\fname{available}\;\refelements\;\gtokens\;{#1}\;{#2}}
\newcommand{\fullCell}[3]{\fname{occupied}\;\refelements\;\gtokens\;{#1}\;{#2}\;{#3}}
% canonical variable names:
\newcommand{\capacity}{\ensuremath{C}}
......
Supports Markdown
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