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

ICFP21 paper: group ghost state defs and axioms in figures and subfigures

parent a147cb4c
\begin{subfigure}[H]{\textwidth}
\begin{mathpar}
%
\infer[\rulenameIsQueueAg]{%
\ownGhost\gqueue{\authfull \tuple{\tview, \hview, \elemViewList}}
\ISEP \isQueue {\tview'} {\hview'} \elemViewListB
}{%
\tview = \tview'
\LAND \hview = \hview'
\mathlop{\mathord\land \Forall i.} \elem = \elem'_i
\LAND \eview_i = \eview'_i
}
\infer[\rulenameIsQueueUpd]{%
\ownGhost\gqueue{\authfull \tuple{\tview, \hview, \elemViewList}}
\ISEP \isQueue \tview \hview \elemViewList
}{%
\upd
\ownGhost\gqueue{\authfull \tuple{\tview', \hview', \elemViewListB}}
\ISEP \isQueue {\tview'} {\hview'} \elemViewListB
}
%
\end{mathpar}
\Description{Properties of the representation predicate.}
\caption{Properties of the representation predicate}
\label{fig:queue:axioms:isqueue}
\end{subfigure}
\begin{subfigure}[H]{\textwidth}
\begin{mathpar}
%
\infer[\rulenameTokenExclRR]
{\tokenR\idx \ISEP \tokenR{\idx'}}
{\modcap\idx \neq \modcap{\idx'}}
\infer[\rulenameTokenExclRW]
{\tokenR\idx \ISEP \tokenW{\idx'}{\pair{\elem'}{\eview'}}}
{\modcap\idx \neq \modcap{\idx'}}
\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[\rulenameTokenRAg]
{\ownGhost\gtokens{\authfull m} \ISEP \tokenR\idx}
{\maplookup{m}\idx = \Unit}
\infer[\rulenameTokenWAg]
{\ownGhost\gtokens{\authfull m} \ISEP \tokenW\idx{\pair\elem\eview}}
{\maplookup{m}\idx = \pair\elem\eview}
\\
\infer[\rulenameTokenUpdRW]
{\ownGhost\gtokens{\authfull m} \ISEP \tokenR{(\idx-\capacity)}}
{\upd
\ownGhost\gtokens{\authfull \mapupdate{\mapupdate{m}
{\idx-\capacity} \bot }
\idx {\pair\elem\eview}
}
\ISEP \tokenW\idx{\pair\elem\eview}}
\\
\infer[\rulenameTokenUpdWR]
{\ownGhost\gtokens{\authfull m} \ISEP \tokenW\idx{\pair\elem\eview}}
{\upd
\ownGhost\gtokens{\authfull \mapupdate{m} \idx \Unit} \ISEP \tokenR\idx}
%
\end{mathpar}
\Description{Properties of tokens.}
\caption{Properties of tokens}
\label{fig:queue:axioms:token}
\end{subfigure}
\begin{subfigure}[H]{\textwidth}
\begin{mathpar}
%
\infer[\rulenameWitnessPers]{~}{\persistent{\monoWitness \offset {\pair\status\sview}}}
\infer[\rulenameWitnessOrder]{%
\ownGhost \gmonos {\mapsingleton\offset{\authfull \pair\status\sview}}
\ISEP \monoWitness \offset {\pair{\status'}{\sview'}}
}{%
\pair{\status'}{\sview'} \sqsubseteq \pair\status\sview
}
\infer[\rulenameWitnessUpd]{%
\ownGhost \gmonos {\mapsingleton\offset{\authfull \pair\status\sview}}
\ISEP \pair\status\sview \sqsubseteq \pair{\status'}{\sview'}
}{%
\upd
\ownGhost \gmonos {\mapsingleton\offset{\authfull \pair{\status'}{\sview'}}}
\ISEP \monoWitness \offset {\pair{\status'}{\sview'}}
}
%
\end{mathpar}
\Description{Properties of witnesses.}
\caption{Properties of witnesses}
\label{fig:queue:axioms:witness}
\end{subfigure}
\begin{figure}
\[\begin{array}{rcl}
% public state:
\newcolumntype{R}{>{\raggedleft$}p{.45\textwidth}<{$}}
\newcolumntype{L}{>{$}p{.45\textwidth}<{$}}
% public state:
\begin{subfigure}{\textwidth}
\[\begin{array}{@{}RcL@{}}
\gqueue
& :
& \authm(\exm(\typeView \times \typeView \times \typeList(\typeVal \times \typeView)))
......@@ -12,11 +16,47 @@
& \eqdef
& \ownGhost\gqueue{\authfrag \tuple{\tview, \hview, \elemViewList}}
% we omit the injection of \exm (\exinj)
\end{array}\]
\Description{Ghost state describing the public state.}
\caption{Ghost state describing the public state}
\label{fig:queue:inv:isqueue}
\end{subfigure}%
% lattice of status-view pairs:
\\ \hline
\begin{subfigure}{\textwidth}
\[\begin{array}{@{}RcL@{}}%
%\toprule
\statusViewLat
& \eqdef
& (\Z \times \typeView, \sqsubseteq, \sqcup)
\\
\pair{\status_1}{\sview_1}
\sqsubseteq
\pair{\status_2}{\sview_2}
& \eqdef
& \status_1 < \status_2 \lor \left( \status_1 = \status_2 \land \sview_1 \viewgeq \sview_2 \right)
\\
\pair{\status_1}{\sview_1}
\sqcup
\pair{\status_2}{\sview_2}
& \eqdef
& \begin{cases}%
\pair{\status_2}{\sview_2} & \text{if }\status_1 < \status_2 \\
\pair{\status }{\sview_1 \viewmeet \sview_2} & \text{if }\status_1 = \status_2 = \status \\
\pair{\status_1}{\sview_1} & \text{if }\status_1 > \status_2 \\
\end{cases}%
\end{array}\]
\Description{Semi-lattice defining an order on status-view pairs.}
\caption{Semi-lattice defining an order on status-view pairs}
\label{fig:queue:cmra:statlat}
\end{subfigure}%
% monotonicity of statuses:
% monotonicity of statuses:
\begin{subfigure}{\textwidth}
\[\begin{array}{@{}RcL@{}}
%\toprule
\gmonos
& :
& \finmapm{\Z}{\authm(\statusViewLat)}
......@@ -25,11 +65,18 @@
\monoWitness{\offset}{\pair\status\sview}
& \eqdef
& \ownGhost\gmonos{\mapsingleton{\offset}{\authfrag \pair\status\sview}}
\end{array}\]
\\ \hline
\Description{Ghost state reflecting the monotonicity of statuses.}
\caption{Ghost state reflecting the monotonicity of statuses}
\label{fig:queue:inv:witness}
\end{subfigure}%
% tokens:
% tokens:
\begin{subfigure}{\textwidth}
\[\begin{array}{@{}RcL@{}}
%\toprule
\gtokens
& :
& \authm\left(\finmapm{\Z}{\exm(\typeUnit\;+\;\typeVal \times \typeView)}\right)
......@@ -42,15 +89,25 @@
& \eqdef
& \ownGhost\gtokens{\authfrag \mapsingleton{\idx}{\pair\elem\eview}}
% we omit the injections of \exm (\exinj) and of the sum (\cinl and \cinr)
\end{array}\]
\Description{Ghost state implementing tokens.}
\caption{Ghost state implementing tokens}
\label{fig:queue:inv:token}
\end{subfigure}%
\\ \hline
% invariant:
\begin{subfigure}{\textwidth}
\[\begin{array}{@{}RcL@{}}
%\toprule
% invariant (outer):
\queueInv
& \eqdef
& \Exists \gmonos, \gtokens. \knowInv{}{\queueInvInner}
%
\\
% invariant (inner):
......@@ -69,7 +126,7 @@
\cr 0 \le \tail \le \head \le \tail + \capacity
% pointsto assertions:
\cr \pointstoAT\reftail{\mkval\tail\tview}
\cr \pointstoAT\refhead{\mkval\head\hview}
\ISEP \pointstoAT\refhead{\mkval\head\hview}
\cr \arraypointstoAT\refstatuses\statusViewList
% authoritative ghost state assertions:
\cr \ownGhost\gqueue{\authfull \tuple{\tview, \hview, \elemViewListInv<\tail><\head>}}
......@@ -130,10 +187,10 @@
& \eqdef
& \isepV{%
\status = 2(\idx + \capacity)
\cr (\nthpointstoNA\refelements{\modcap\idx}-) \opat \sview
\ISEP (\nthpointstoNA\refelements{\modcap\idx}-) \opat \sview
\cr \tokenR\idx
}
%
\\
% predicate for occupied cells:
......@@ -141,14 +198,20 @@
\fullCell \idx {\pair\status\sview} {\pair\elem\eview}
& \eqdef
& \isepV{%
\status = 2\idx + 1
\cr (\nthpointstoNA\refelements{\modcap\idx}{\elem}) \opat \sview
\status = 2\idx + 1 \hphantom{()\,}
\ISEP (\nthpointstoNA\refelements{\modcap\idx}{\elem}) \opat \sview
\cr \tokenW\idx{\pair\elem\eview}
\cr \eview \viewleq \sview
\ISEP \eview \viewleq \sview
}
%
\end{array}\]
\Description{Internal invariant of the bounded queue.}
\caption{Internal invariant of the bounded queue}
\Description{Internal invariant of the queue.}
\caption{Internal invariant of the queue}
\label{fig:queue:inv:inv}
\end{subfigure}%
\Description{Definitions of assertions intervening in the proof of the bounded queue.}
\caption{Definitions of assertions intervening in the proof of the bounded queue}
\label{fig:queue:inv}
\end{figure}
......@@ -19,6 +19,7 @@
% \usepackage{stmaryrd}
\usepackage{xspace}
\usepackage{footmisc} % recall a footnote with \footref
\usepackage{caption,subcaption} % subfigures
% Respect the order of papers inside a \cite command.
\setcitestyle{nosort}
......
......@@ -749,7 +749,7 @@
%\newcommand{\latm}{\textmon{Lattice}}
% the lattice of (status,view) pairs:
\newcommand{\statusViewLat}{\textmon{StatusView}}
\newcommand{\statusViewLat}{\textmon{StatusWithView}}
\newcommand{\statusViewBotLat}{\ensuremath{\statusViewLat_\latbot}}
\newcommand{\latbot}{\bot}
......@@ -770,7 +770,8 @@
\newcommand{\isQueueSC}[1]{\ISQUEUE\;\gqueue\;{#1}}
\newcommand{\isQueue}[3]{\ISQUEUE\;\gqueue\;{#1}\;{#2}\;{#3}}
\newcommand{\isQueuePers}[1]{\fname{QueuePersistent}\;\queue\;{#1}}
\newcommand{\queueInv}{\fname{QueueInv}\;\queue\;\gqueue}
\newcommand{\QUEUEINV}{\fname{QueueInv}}
\newcommand{\queueInv}{\QUEUEINV\;\queue\;\gqueue}
\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}}
......
......@@ -42,9 +42,22 @@ Ghost state can be coupled with invariants such as the ones presented in \sref{s
In \fref{fig:queue:inv}, one can see how this methodology is used for describing the internal protocol of the queue: the persistent predicate $\queueInv$ is in fact an invariant; the exclusive representation predicate $\isQueue\tview\hview\elemViewList$ is defined using ghost state, as are several internal resources.
We detail these definitions in the following sections.
\begin{figure}
\input{figure-queue-axioms-isqueue}
\mbox{}\vfil\mbox{}
\input{figure-queue-axioms-witness}
\mbox{}\vfil\mbox{}
\input{figure-queue-axioms-token}
\Description{Axiomatic description the ghost state of the queue.}
\caption{Axiomatic description of the ghost state of the queue}
\label{fig:queue:axioms}
\end{figure}
\subsection{Public state}
The assertion $\isQueue\tview\hview\elemViewList$ exposes to the user the public
%\input{figure-queue-ghost-isqueue}
The assertion $\isQueue\tview\hview\elemViewList$, defined in~\fref{fig:queue:inv:isqueue}, exposes to the user the public
state of the queue. This public state, as motivated in \sref{sec:queue:spec:weak},
is composed of the tail view, the head view, and the list of current items with
their views.
......@@ -53,31 +66,8 @@ It is tied to the internal state of the queue via the use of an authoritative
ghost state, stored in a ghost variable~$\gqueue$.
%
More precisely, the public state is kept in sync with the values which appear in an authoritative assertion $\ownGhost\gqueue{\authfull \tuple{\tview, \hview, \elemViewList}}$, the latter being owned by the internal invariant.
%
Formally, the two assertions satisfy the following properties:
%
\begin{mathpar}
%
\infer[\rulenameIsQueueAg]{%
\ownGhost\gqueue{\authfull \tuple{\tview, \hview, \elemViewList}}
\ISEP \isQueue {\tview'} {\hview'} \elemViewListB
}{%
\tview = \tview'
\LAND \hview = \hview'
\mathlop{\mathord\land \Forall i.} \elem = \elem'_i
\LAND \eview_i = \eview'_i
}
\infer[\rulenameIsQueueUpd]{%
\ownGhost\gqueue{\authfull \tuple{\tview, \hview, \elemViewList}}
\ISEP \isQueue \tview \hview \elemViewList
}{%
\upd
\ownGhost\gqueue{\authfull \tuple{\tview', \hview', \elemViewListB}}
\ISEP \isQueue {\tview'} {\hview'} \elemViewListB
}
%
\end{mathpar}
Formally, the two assertions satisfy the properties shown in~\fref{fig:queue:axioms:isqueue}.
%
Rule~\ruleIsQueueAg asserts that the state known to the invariant (first premise) is identical to that known to the representation predicate (second premise).
%
......@@ -92,7 +82,7 @@ It is worth remarking that this construction makes the representation predicate
\subsection{Internal invariant}
Along with the exclusive representation predicate $\isQueue\tview\hview\elemViewList$,
we provide the user with the persistent assertion $\queueInv$. It contains the
we provide the user with a persistent assertion $\queueInv$ defined in~\fref{fig:queue:inv:inv}. It contains the
internal invariant governing the queue~$\queue$, whose public state is exposed
via the ghost variable~$\gqueue$. In addition to the public state, there are
two more ghost variables, named $\gmonos$ and $\gtokens$, which are hidden
......@@ -130,6 +120,9 @@ We now explain the other two pieces of ghost state.
\subsection{Monotonicity of statuses}
%\input{figure-queue-ghost-witness}
%\input{figure-queue-cmra-statlat}
The purpose of the ghost variable~$\gmonos$ is to reflect the fact that statuses
are monotonic.
%
......@@ -152,6 +145,7 @@ we use two assertions,
$\ownGhost \gmonos {\mapsingleton\offset{\authfull \pair\status\sview}}$
and $\monoWitness \offset {\pair\status\sview}$,
connected via a ghost variable~$\gmonos$.
Relevant definitions appear in~\fref{fig:queue:inv:witness}.
%
The first assertion, owned by the invariant of the queue is connected by the invariant to the value-view pair stored in the status cell.
In addition, it is exclusive: for any offset~$\offset$, two assertions
......@@ -160,31 +154,11 @@ of the form $\ownGhost \gmonos {\mapsingleton\offset{\authfull -}}$ cannot hold
The second assertion $\monoWitness \offset {\pair\status\sview}$ means that the value-view pair stored in the status cell is at least $\pair\status\sview$.
Importantly, a witness assertion is persistent: once it has been established, it remains true forever and can be duplicated at will.
We thus have the following properties:
%
\begin{mathpar}
%
\infer[\rulenameWitnessPers]{~}{\persistent{\monoWitness \offset {\pair\status\sview}}}
\infer[\rulenameWitnessOrder]{%
\ownGhost \gmonos {\mapsingleton\offset{\authfull \pair\status\sview}}
\ISEP \monoWitness \offset {\pair{\status'}{\sview'}}
}{%
\pair{\status'}{\sview'} \sqsubseteq \pair\status\sview
}
\infer[\rulenameWitnessUpd]{%
\ownGhost \gmonos {\mapsingleton\offset{\authfull \pair\status\sview}}
\ISEP \pair\status\sview \sqsubseteq \pair{\status'}{\sview'}
}{%
\upd
\ownGhost \gmonos {\mapsingleton\offset{\authfull \pair{\status'}{\sview'}}}
\ISEP \monoWitness \offset {\pair{\status'}{\sview'}}
}
We thus have the properties summarized in~\fref{fig:queue:axioms:witness}.
%
\end{mathpar}
Rule~\ruleWitnessPers is the persistency just mentioned.
%
Rule~\ruleWitnessPers is the persistency just mentioned. Rule~\ruleWitnessOrder asserts that a witness gives a lower bound on what the status cell currently stores.
Rule~\ruleWitnessOrder asserts that a witness gives a lower bound on what the status cell currently stores.
%
Rule~\ruleWitnessUpd asserts that we can update a status cell to any larger or equal content, and obtain a witness for that content.
......@@ -204,37 +178,11 @@ A general recipe for deriving a CMRA structure with a given inclusion order, if
that order admits binary joins, consists in taking the join operation as the
composition of the CMRA\@~\cite{timany2021monotonicity}.
In this case, we equip the product set \(\Z \times \typeView\) with
the following join-semilattice structure:
%
\[\begin{array}{@{}rcl@{}}%
\statusViewLat
&\eqdef&
(
\Z \times \typeView,
\sqsubseteq,
\sqcup
)
\\
\pair{\status_1}{\sview_1}
\sqsubseteq
\pair{\status_2}{\sview_2}
&\eqdef&
\status_1 < \status_2 \lor \left( \status_1 = \status_2 \land \sview_1 \viewgeq \sview_2 \right)
\\
\pair{\status_1}{\sview_1}
\sqcup
\pair{\status_2}{\sview_2}
&\eqdef&
\begin{cases}%
\pair{\status_2}{\sview_2} & \text{if }\status_1 < \status_2 \\
\pair{\status }{\sview_1 \viewmeet \sview_2} & \text{if }\status_1 = \status_2 = \status \\
\pair{\status_1}{\sview_1} & \text{if }\status_1 > \status_2 \\
\end{cases}%
\end{array}\]%
the join-semilattice structure whose definition appears in~\fref{fig:queue:cmra:statlat}.
\subsection{Available and occupied slots}
The last two lines of the invariant describe the state of each slot.
In~\fref{fig:queue:inv:inv}, the last two lines of the invariant describe the state of each slot.
For clarity, we introduce two abbreviations:
%
the assertion $\emptyCell \idx {\pair\status\sview}$
......@@ -330,7 +278,7 @@ temporarily invalidated when a thread enqueues or dequeues.
Specifically, the thread breaks the assertion when it increments \refhead or
\reftail, thus commiting to enqueuing or dequeuing, until it updates the status
of the corresponding slot. It is thus necessary to represent slots which are in
a temporary state. In the actual invariant shown in~\fref{fig:queue:inv},
a temporary state. In the actual invariant shown in~\fref{fig:queue:inv:inv},
slots from~$\head-\capacity$ to~$\tail$ are either available or in a temporary
state where they appear as occupied ($\status_{\modcap\idx} = 2\idx + 1$), until
a dequeuer finishes emptying them;
......@@ -345,6 +293,8 @@ when updating the status.
\subsection{Slot tokens}
%\input{figure-queue-ghost-token}
This time frame is also when the last piece of ghost state, stored in the ghost
variable~$\gtokens$, intervenes.
Other threads can make the queue progress between the moment when an enqueuer is
......@@ -411,46 +361,8 @@ The read~token of rank~$\idx$ is denoted by $\tokenR\idx$,
while the write~token of rank~$\idx$ with payload $\elem$ and $\eview$ is denoted by $\tokenW\idx{\pair\elem\eview}$.
Their authoritative counterpart, owned by the invariant, is an assertion of the form $\ownGhost \gtokens {\authfull m}$ where $m$ is a finite map.
Its domain is the range~$[\head-\capacity, \head)$ of ranks which have a token, and its images are the payload (considering that read~tokens bear a payload of $\Unit$). In the invariant, the value of the map is connected to that of the public state.
The assertions satisfy the following properties:
%
\begin{mathpar}
%
\infer[\rulenameTokenExclRR]
{\tokenR\idx \ISEP \tokenR{\idx'}}
{\modcap\idx \neq \modcap{\idx'}}
\infer[\rulenameTokenExclRW]
{\tokenR\idx \ISEP \tokenW{\idx'}{\pair{\elem'}{\eview'}}}
{\modcap\idx \neq \modcap{\idx'}}
\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[\rulenameTokenRAg]
{\ownGhost\gtokens{\authfull m} \ISEP \tokenR\idx}
{\maplookup{m}\idx = \Unit}
\infer[\rulenameTokenWAg]
{\ownGhost\gtokens{\authfull m} \ISEP \tokenW\idx{\pair\elem\eview}}
{\maplookup{m}\idx = \pair\elem\eview}
\\
\infer[\rulenameTokenUpdRW]
{\ownGhost\gtokens{\authfull m} \ISEP \tokenR{(\idx-\capacity)}}
{\upd
\ownGhost\gtokens{\authfull \mapupdate{\mapupdate{m}
{\idx-\capacity} \bot }
\idx {\pair\elem\eview}
}
\ISEP \tokenW\idx{\pair\elem\eview}}
\\
\infer[\rulenameTokenUpdWR]
{\ownGhost\gtokens{\authfull m} \ISEP \tokenW\idx{\pair\elem\eview}}
{\upd
\ownGhost\gtokens{\authfull \mapupdate{m} \idx \Unit} \ISEP \tokenR\idx}
%
\end{mathpar}
The assertions are defined in~\fref{fig:queue:inv:token} and satisfy the properties in~\fref{fig:queue:axioms:token}.
%
The first three properties say that tokens are exclusive.
%
......@@ -460,7 +372,7 @@ Rule~\ruleTokenUpdRW corresponds to step~\ref{item:token1} in the list above, wh
%
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,
In addition to these rules, 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.
Thanks to that property, at step~\ref{item:token4} (respectively~\ref{item:token2}), when a dequeuer (respectively an enqueuer) returns the token, it knows that the rank it has been operating on is still in the right range---in other words, that the queue has not advanced too far while the thread was working.
......
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