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

ICFP21 paper: name ghost state rules

parent 7f79f2c1
......@@ -687,7 +687,6 @@
\newcommand{\basecasfailure}{\RULE{\namebasecasfailure}}
% Names of rules in \hlog.
\newcommand{\nameseenzero}{Seen-Zero}
\newcommand{\nameseentwo}{Seen-Two}
\newcommand{\namesplitso}{Split-Subjective-Objective}
......@@ -824,11 +823,31 @@
%\newcommand{\modcap}[1]{\overline{{#1}}}
\newcommand{\modcap}[1]{\widehat{{#1}}}
% name of rules:
\newcommand{\rulenametryenqueue}{queue-TryEnqueue}
\newcommand{\rulenametrydequeue}{queue-TryDequeue}
\newcommand{\ruletryenqueue}{\RULE{\rulenametryenqueue}}
\newcommand{\ruletrydequeue}{\RULE{\rulenametrydequeue}}
% names of rules about the ghost state:
\newcommand{\rulenameIsQueueAg}{IsQueue-Agree}
\newcommand{\rulenameIsQueueUpd}{IsQueue-Update}
\newcommand{\rulenameWitnessPers}{Witness-Persistent}
\newcommand{\rulenameWitnessOrder}{Witness-Order}
\newcommand{\rulenameWitnessUpd}{Witness-Update}
\newcommand{\rulenameTokenExclRR}{Token-Exclusive-RR}
\newcommand{\rulenameTokenExclRW}{Token-Exclusive-RW}
\newcommand{\rulenameTokenExclWW}{Token-Exclusive-WW}
\newcommand{\rulenameTokenRAg}{TokenR-Agree}
\newcommand{\rulenameTokenWAg}{TokenW-Agree}
\newcommand{\rulenameTokenUpdRW}{Token-Update-RW}
\newcommand{\rulenameTokenUpdWR}{Token-Update-WR}
\newcommand{\ruleIsQueueAg}{\RULE{\rulenameIsQueueAg}}
\newcommand{\ruleIsQueueUpd}{\RULE{\rulenameIsQueueUpd}}
\newcommand{\ruleWitnessPers}{\RULE{\rulenameWitnessPers}}
\newcommand{\ruleWitnessOrder}{\RULE{\rulenameWitnessOrder}}
\newcommand{\ruleWitnessUpd}{\RULE{\rulenameWitnessUpd}}
\newcommand{\ruleTokenExclRR}{\RULE{\rulenameTokenExclRR}}
\newcommand{\ruleTokenExclRW}{\RULE{\rulenameTokenExclRW}}
\newcommand{\ruleTokenExclWW}{\RULE{\rulenameTokenExclWW}}
\newcommand{\ruleTokenRAg}{\RULE{\rulenameTokenRAg}}
\newcommand{\ruleTokenWAg}{\RULE{\rulenameTokenWAg}}
\newcommand{\ruleTokenUpdRW}{\RULE{\rulenameTokenUpdRW}}
\newcommand{\ruleTokenUpdWR}{\RULE{\rulenameTokenUpdWR}}
% ------------------------------------------------------------------------------
% Notations for the pipeline.
......
......@@ -58,7 +58,7 @@ Formally, the two assertions satisfy the following properties:
%
\begin{mathpar}
%
\infer{%
\infer[\rulenameIsQueueAg]{%
\ownGhost\gqueue{\authfull \tuple{\tview, \hview, \elemViewList}}
\ISEP \isQueue {\tview'} {\hview'} \elemViewListB
}{%
......@@ -68,7 +68,7 @@ Formally, the two assertions satisfy the following properties:
\LAND \eview_i = \eview'_i
}
\infer{%
\infer[\rulenameIsQueueUpd]{%
\ownGhost\gqueue{\authfull \tuple{\tview, \hview, \elemViewList}}
\ISEP \isQueue \tview \hview \elemViewList
}{%
......@@ -79,9 +79,9 @@ Formally, the two assertions satisfy the following properties:
%
\end{mathpar}
%
The first property asserts that the state known to the invariant (first premise) is identical to that known to the representation predicate (second premise).
Rule~\ruleIsQueueAg asserts that the state known to the invariant (first premise) is identical to that known to the representation predicate (second premise).
%
The second property asserts that, whenever we own both the representation predicate and its authoritative counterpart, we can update the public state to any other value by taking a \emph{ghost update} step. The symbol~$\upd$ is an Iris modality which represents such a ghost update.
Rule~\ruleIsQueueUpd asserts that, whenever we own both the representation predicate and its authoritative counterpart, we can update the public state to any other value by taking a \emph{ghost update} step. The symbol~$\upd$ is an Iris modality which represents such a ghost update.
We achieve these properties by using an adequate CMRA for the values of the ghost variable~$\gqueue$.
We build this CMRA by composing several classical Iris constructs; namely, the exclusive CMRA $\exm(S)$ where $S$ is a set, and the authoritative CMRA $\authm(M)$ where $M$ is a CMRA\@.
......@@ -164,16 +164,16 @@ We thus have the following properties:
%
\begin{mathpar}
%
\infer{~}{\persistent{\monoWitness \offset {\pair\status\sview}}}
\infer[\rulenameWitnessPers]{~}{\persistent{\monoWitness \offset {\pair\status\sview}}}
\infer{%
\infer[\rulenameWitnessOrder]{%
\ownGhost \gmonos {\mapsingleton\offset{\authfull \pair\status\sview}}
\ISEP \monoWitness \offset {\pair{\status'}{\sview'}}
}{%
\pair{\status'}{\sview'} \sqsubseteq \pair\status\sview
}
\infer{%
\infer[\rulenameWitnessUpd]{%
\ownGhost \gmonos {\mapsingleton\offset{\authfull \pair\status\sview}}
\ISEP \pair\status\sview \sqsubseteq \pair{\status'}{\sview'}
}{%
......@@ -184,9 +184,9 @@ We thus have the following properties:
%
\end{mathpar}
%
The first property is the persistency just mentioned. The second property is the fact that a witness gives a lower bound on what the status cell currently stores.
Rule~\ruleWitnessPers is the persistency just mentioned. Rule~\ruleWitnessOrder asserts that a witness gives a lower bound on what the status cell currently stores.
%
The last property asserts that we can update a status cell to any larger or equal content, and obtain a witness for that content.
Rule~\ruleWitnessUpd asserts that we can update a status cell to any larger or equal content, and obtain a witness for that content.
We achieve these properties by constructing an adequate CMRA for the values taken by the ghost variable~$\gmonos$. Again, we will not explain standard Iris constructs here, except for one point.
%
......@@ -415,28 +415,28 @@ The assertions satisfy the following properties:
%
\begin{mathpar}
%
\infer
\infer[\rulenameTokenExclRR]
{\tokenR\idx \ISEP \tokenR{\idx'}}
{\modcap\idx \neq \modcap{\idx'}}
\infer
\infer[\rulenameTokenExclRW]
{\tokenR\idx \ISEP \tokenW{\idx'}{\pair{\elem'}{\eview'}}}
{\modcap\idx \neq \modcap{\idx'}}
\infer
\infer[\rulenameTokenExclWW]
{\tokenW\idx{\pair\elem\eview} \ISEP \tokenW{\idx'}{\pair{\elem'}{\eview'}}}
{\modcap\idx \neq \modcap{\idx'}}
\\
% this rule is not really needed:
\infer
\infer[\rulenameTokenRAg]
{\ownGhost\gtokens{\authfull m} \ISEP \tokenR\idx}
{\maplookup{m}\idx = \Unit}
\infer
\infer[\rulenameTokenWAg]
{\ownGhost\gtokens{\authfull m} \ISEP \tokenW\idx{\pair\elem\eview}}
{\maplookup{m}\idx = \pair\elem\eview}
\\
\infer
\infer[\rulenameTokenUpdRW]
{\ownGhost\gtokens{\authfull m} \ISEP \tokenR{(\idx-\capacity)}}
{\upd
\ownGhost\gtokens{\authfull \mapupdate{\mapupdate{m}
......@@ -445,7 +445,7 @@ The assertions satisfy the following properties:
}
\ISEP \tokenW\idx{\pair\elem\eview}}
\\
\infer
\infer[\rulenameTokenUpdWR]
{\ownGhost\gtokens{\authfull m} \ISEP \tokenW\idx{\pair\elem\eview}}
{\upd
\ownGhost\gtokens{\authfull \mapupdate{m} \idx \Unit} \ISEP \tokenR\idx}
......@@ -456,9 +456,9 @@ The first three properties say that tokens are exclusive.
%
The next two say that tokens agree with the authoritative counterpart, hence with the public state.
%
The sixth rule corresponds to step~\ref{item:token1} in the list above, where we create a write~token of rank~$\idx$ by destructing a read~token of rank~$\idx-\capacity$.
Rule~\ruleTokenUpdRW corresponds to step~\ref{item:token1} in the list above, where we create a write~token of rank~$\idx$ by destructing a read~token of rank~$\idx-\capacity$.
%
Likewise, the last rule corresponds to step~\ref{item:token3}, where we turn a write~token into a read~token of the same rank.
Likewise, rule~\ruleTokenUpdWR corresponds to step~\ref{item:token3}, where we turn a write~token into a read~token of the same rank.
Lastly, the finite map described in the internal invariant is such that,
whenever we own a read~token (respectively a write~token), the rank of this token necessarily lies in the range~$[\head-\capacity, \tail)$ (respectively $[\tail, \head)$), where $\tail$ and $\head$ are the values of $\reftail$ and $\refhead$ which are existentially quantified in the invariant.
......@@ -484,18 +484,6 @@ Thanks to that property, at step~\ref{item:token4} (respectively~\ref{item:token
% so we take for~$M\sub{write}$ the product set $\typeVal\times\typeView$.
%Read~tokens and write~tokens are then defined as shown in~\fref{fig:queue:inv}.
%In other words, it needs to know that its own rank~$\idx$ is still in the range~$[\tail, \head)$, whereas $\tail$ and $\head$ may be greater than when the thread has been attributed rank~$\idx$.
%
%\begin{mathpar}%
%%
% \infer{%
% \tokenR \idx \ISEP ...
% }{%
% \head-\capacity \leq \idx < \tail
% }
%%
%\end{mathpar}%
% ------------------------------------------------------------------------------
There are more properties that are invariants of the queue, and thus could be stated
......
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