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

representation of slots in the invariant

parent 904f1c47
......@@ -28,6 +28,9 @@
% Modulus operator.
\newcommand{\mmod}{\mathbin{\mathrm{mod}}}
% Tentative definition:
\newcommand{\tryeqdef}{\ensuremath{\mathrel{\stackrel{?}{=}}}}
\makeatletter
% An anonymous command, to give to higher-order commands.
......@@ -732,8 +735,10 @@
\newcommand{\isQueuePers}[1]{\fname{IsQueuePersistent}\;\queue\;{#1}}
\newcommand{\queueInv}{\fname{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}}
%\newcommand{\emptyCell}[2]{\fname{Available}\;\refelements\;\gtokens\;{#1}\;{#2}}
%\newcommand{\fullCell}[3]{\fname{Occupied}\;\refelements\;\gtokens\;{#1}\;{#2}\;{#3}}
\newcommand{\emptyCell}[2]{\fname{Available}\;{#1}\;{#2}}
\newcommand{\fullCell}[3]{\fname{Occupied}\;{#1}\;{#2}\;{#3}}
% canonical variable names:
\newcommand{\capacity}{\ensuremath{C}}
......
......@@ -74,7 +74,7 @@ involved CMRA uses two standard Iris constructions.
\item
For a given CMRA~$M$,%
\footnote{%
It is also required that $M$ possess an \emph{unit} element, but we can
It is also required that $M$ possess an unit element, but we can
always add such an element artificially, so we omit this technical detail
for the sake of clarity.
}
......@@ -272,6 +272,94 @@ we get the following:
Thus this assertion acts as a remainder that, at some point, the status of
slot~\offset\ stored the value~$\status$ and the view~$\sview$.
\subsubsection{Description of slots}
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}$
represents slot~$\modcap\idx$
being available for a future item of rank~$\idx+\capacity$;
%
the assertion $\fullCell \idx {\pair\status\sview} {\pair\elem\eview}$
represents slot~$\modcap\idx$
being occupied by the item of rank~$\idx$,
whose value is $\elem$ with the associated view $\eview$.
%
In these two abbreviations, the status field of the slot has value~$\status$ and
stores view~$\sview$.
%In both cases, we must own the memory cell.
Recall that in \hlog, $\nthpointstoNA\refelements{\modcap\idx}\elem$
is the pointsto assertion for the \emph{nonatomic} cell at index~$\modcap\idx$
of location~\refelements: it asserts the unique ownership of that cell, and
states that we have observed its latest write event, which wrote the value~$\elem$.
Unlike an atomic pointsto assertion, this one is \emph{subjective}: its truth
depends on the view of the subject thread. As a consequence, it cannot be put in
an invariant as is.
%
To share it, we have to make explicit some view which is enough to make the
assertion hold.
In \hlog, for any potentially subjective assertion~$\prop$, the objective
assertion~$\prop \opat \view$ has the meaning of $\prop$ under the condition
that the view of the subject thread contains~$\view$.
%
It can be understood as $\seen\view \wand \prop$ but, in addition, it is objective.
% TODO: figure pour rappeler la règle Split-Subjective-Objective
% (et peut-être que P @ V ⊣⊢ Objectively(↑V -∗ P) ?)
%At which view do we own the item cell? In our queue implementation, the status
%field of a given slot plays the role of a ``lock'' for the item field of that slot.
%Not only does its value~$\status$ indicate whether the slot is available or occupied,
%it also guarantees synchronization from an user of the slot to the next user,
%through the view~$\sview$ it stores.
At which view can we own a nonatomic memory cell?
At a view which contains the latest write event to that cell; for instance,
the view which was that of the last writer thread when it wrote.
%
Fortunately, in our case, any thread---enqueuer or dequeuer--which writes to the
nonatomic cell $\refelements[\modcap\idx]$ then writes to the atomic cell
$\refstatuses[\modcap\idx]$. Thus it adds its current view, including its own
write to the item field, to the view~$\sview$ stored by the status field.
%(Not so) Naively, one may try to represent the buffer as follows:
With that said, a first attempt at representing the buffer may end up as follows:
%
\[\begin{array}{rcl}
% invariant (inner) (wrong):
\queueInvInner
& \tryeqdef
& \ISep{\begin{array}{c@{}l}
\vdots
\\
\\ \displaystyle\Sep_{\head-\capacity \leq \idx < \tail}&
\emptyCell \idx {\nthStatusView{\modcap\idx}}
\\ \displaystyle\Sep_{\tail \leq \idx < \head}&
\fullCell \idx {\nthStatusView{\modcap\idx}} {\nthElemView\idx}
\end{array}}
\\
% predicate for available cells (wrong):
\emptyCell \idx {\pair\status\sview}
& \tryeqdef
& \status = 2(\idx + \capacity)
\isep (\nthpointstoNA\refelements{\modcap\idx}-) \opat \sview
\\
% predicate for occupied cells (wrong):
\fullCell \idx {\pair\status\sview} {\pair\elem\eview}
& \tryeqdef
& \status = 2\idx + 1 \hphantom{()\,}
\isep (\nthpointstoNA\refelements{\modcap\idx}{\elem}) \opat \sview
\isep \eview \viewleq \sview
\end{array}\]
% …
There are more properties that are invariant of the code, and thus can be added
......
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