% ------------------------------------------------------------------------------
% Proof of the bounded queue.
\section{Proof of the Specification for the Ring Buffer}
\label{sec:queue:proof}
\input{figure-queue-inv}
We now turn to proving the following.
\begin{theorem}%
The implementation shown in \fref{fig:queue:impl} (\sref{sec:queue:impl})
satisfies the functional specification appearing in \fref{fig:queue:spec:weak}
(\sref{sec:queue:spec:weak}).
\end{theorem}%
In the Iris methodology, which \hlog{} is based on, concurrent protocols are established thanks to \emph{ghost state} and \emph{invariants}.
Ghost state in Iris is a flexible tool for defining custom resources.
It takes values from algebraic structures called CMRAs;
for the purpose of this paper, it is enough to think of a CMRA as a set
equipped with a binary composition operation $(\mtimes)$ that is partial,
associative and commutative.
Ghost state values are assigned to ghost variables.
The separation logic assertion~$\ownGhost\gname{a}$, where $a$ is an element of
some CMRA, intuitively means that we own a fragment of the ghost variable
$\gname$ and that this fragment has value~$a$.
Unlike what happens with a traditional pointsto assertion, the ownership \emph{and value} of
a ghost variable can be split into fragments according to the composition
operation of the CMRA:
\(
\ownGhost\gname{a \mtimes b} \iequiv \ownGhost\gname{a} \isep \ownGhost\gname{b}
\).
In \hlog, ghost state is objective, as it is independent from the physical state
of the memory.%
%% \footnote{%
%% In fact, the physical memory is itself encoded as a piece of ghost state.
%% }
Ghost state can be coupled with invariants such as the ones presented in \sref{sec:queue:spec:sc} to describe protocols that threads must follow to access shared resources.
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}
%\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.
%
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 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).
%
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\@.
We do not explain the construction in more detail; the interested reader may refer to the documentation of Iris~\cite{iris}.
It is worth remarking that this construction makes the representation predicate exclusive: it is absurd to own simultaneously two assertions of the form $\isQueue - - -$.
\subsection{Internal invariant}
Along with the exclusive representation predicate $\isQueue\tview\hview\elemViewList$,
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
to the user of the queue but needed internally. Thus they are
existentially quantified in this persistent assertion. We will explain the
purpose and meaning of these ghost variables in a moment. For now, we look at
the internal invariant, $\queueInvInner$.
This invariant owns most of the physical locations of the queue: \reftail,
\refhead, \refstatuses, and some parts of the array \refelements.
Recall that pointsto assertions for atomic cells are objective and can be placed inside an invariant.
%
The array-pointsto assertion $\arraypointstoAT\refstatuses\statusViewList$ is
a shorthand for the following iterated conjunction:
\[
\Sep_{0 \leq \offset < \capacity} \nthpointstoAT\refstatuses\offset{\mkval{\status_\offset}{\sview_\offset}}
\]
%
%Recall that in \hlog, $\nthpointstoAT\refstatuses\offset{\mkval{\status_\offset}{\sview_\offset}}$
%is the pointsto assertion for the atomic cell at index~\offset\ of
%location~\refstatuses: it asserts the unique ownership of that cell, and states
%that it currently contains the value $\status_\offset$ and the view
%$\sview_\offset$ (or a larger view).
%
Also, since we encode references as arrays of length~one,
we write $\pointstoAT\reftail{\mkval\tail\tview}$ as a shorthand for
$\nthpointstoAT\reftail0{\mkval\tail\tview}$.
Apart from this physical state, the invariant also stores ghost state. It owns
the authority on all three ghost variables, $\gqueue$, $\gmonos$ and $\gtokens$.
%
The authority of $\gqueue$ is simple: it simply ties internal values to the
public state of the queue, as explained earlier.
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.
%
More precisely, they are \emph{strictly} monotonic: every write to a status cell necessarily increases its value. As a consequence, as long as the value of a status cell has not increased, we know that no write happened to it and, in particular, that the view that it stores has not increased either.
%
In other words, we have the monotonicity of the value-view pair stored in a status cell, for the lexicographic order where the order on views is reversed:
%
\[
\pair{\status_1}{\sview_1}
\sqsubseteq
\pair{\status_2}{\sview_2}
\mathlop{\Longleftrightarrow}
\status_1 < \status_2 \lor \left( \status_1 = \status_2 \land \sview_1 \viewgeq \sview_2 \right)
\]
%
This stronger monotonicity property will be used in the proof---specifically, when verifying \trydequeue---and specifying it is thus an additional requirement of working with a weak memory model.
To reflect monotonicity of the status of offset~$\offset$,
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
of the form $\ownGhost \gmonos {\mapsingleton\offset{\authfull -}}$ cannot hold simultaneously.
%
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 properties summarized in~\fref{fig:queue:axioms:witness}.
%
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~\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.
%
The construction involves building a CMRA
whose carrier set is $\Z \times \typeView$, the set of status-view pairs,
and whose inclusion order%
\footnote{%
For two elements $a$ and $b$ of a CMRA~$M$,
we say that $b$ is included in $a$
if there exists some~$c$ such that $a = b \mtimes c$.
}
coincides with the desired order $\sqsubseteq$.
%
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 join-semilattice structure whose definition appears in~\fref{fig:queue:cmra:statlat}.
\subsection{Available and occupied slots}
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}$
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$.
%
These abbreviations are also where we keep the ownership of the \emph{nonatomic} cell $\refelements[\modcap\idx]$, via a pointsto assertion.
%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$.
%
Recall that, in \hlog, unlike an atomic pointsto assertion, a nonatomic pointsto assertion is \emph{subjective}: its truth
depends on the view of the subject thread. As a consequence, it cannot be placed in
an invariant as is.
%
In order to share this assertion,
we must explicitly indicate at which view it holds.
This is the purpose of the $\opat$ connective.
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 of the last writer thread when that write occurred.
%
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 knowledge, including its own
write to the item field, to the view~$\sview$ stored by the status field.
With all this said, a first attempt at representing the buffer might look as follows:
%
\[\begin{array}{rcl}
% invariant (inner) (wrong):
\queueInvInner
& \tryeqdef
& \isepV{\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}\]
% GLEN: à partir d’ici, on omet "included / excluded" dans les intervalles…
That is, we describe the $\capacity$~slots by ranging from~$\head-\capacity$ to~$\head$.
The indices from~$\head-\capacity$ to~$\tail$ correspond to available slots,
while indices from~$\tail$ to~$\head$ correspond to slots occupied by the items of the queue.
In both cases, we own the item field at the view~$\sview$ which is stored in the corresponding status field.
The item field of an available slot stores an arbitrary value,
while for an occupied slot it stores the item~$\elem$.
An occupied slot should also carry the view~$\eview$ which the queue is supposed
to transfer from the enqueuer to the dequeuer alongside item~$\elem$.
This again relies on the view~$\sview$: the enqueuer adds $\eview$ to $\sview$
when updating the status, and the dequeuer adds~$\sview$ into its own view when
reading the status; so, to retrieve $\eview$, it is enough to state the inclusion
$\eview \viewleq \sview$.
The tentative invariant stated above, however, is not correct: while an
invariant has to hold at any point of the execution, the assertion above is
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: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;
slots from~$\tail$ to~$\head$ are either occupied or in a temporary state where
they appear as available ($\status_{\modcap\idx} = 2\idx$), until an enqueuer
finishes filling them.
When an enqueuer or dequeuer moves a slot into a temporary state, it takes
ownership of its item field, so that it can write to it. Hence the invariant
does not have the corresponding pointsto assertion. The thread must give it back
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
attributed rank~$\idx$, and the moment when it returns the updated slot to the
invariant. An enqueuer needs the assurance that the queue has not gotten too
far and attributed the slot on which it was working to a dequeuer, or
to another enqueuer in a subsequent cycle.
To this effect, we start by stating how advances of the \refhead and \reftail
are limited with respect to one another; indeed, we prove these inequalities as
part of the invariant:
%
\[%
0 \leq \tail \leq \head \leq \tail+\capacity
\]%
We also maintain in existence one token for each rank from~$\head-\capacity$
to~$\head$. These tokens are exclusive assertions, and there cannot exist two tokens
whose ranks are congruent modulo~$\capacity$. Hence the token of rank~$\idx$ is
enough to grant unique write access to slot~$\modcap\idx$.
%
We use it as follows.
%
\begin{enumerate}%
\item \label{item:token1}
When an enqueuer is attributed rank~$\idx$, it borrows a newly created token
of the same rank.
\item \label{item:token2}
When returning the updated slot to the invariant, the enqueuer also returns
the token; from that moment the token is thus kept in the assertion
$\fullCell \idx {\pair\status\sview} {\pair\elem\eview}$.
\item \label{item:token3}
When a dequeuer is attributed rank~$\idx$, it claims that assertion and
borrows the token.
\item \label{item:token4}
When returning the updated slot to the invariant, the dequeuer also returns
the token; from that moment the token is thus kept in the assertion
$\emptyCell \idx {\pair\status\sview}$.
\end{enumerate}%
In step~\ref{item:token1}, the token is created while destructing the token of
rank~$\idx-\capacity$ taken from the assertion $\emptyCell {(\idx-\capacity)} -$,
which represents the available cell that the thread claims for enqueuing.
To be able to distinguish between the two temporary states (enqueuing and
dequeuing), we give the token a flavor:
from steps~\ref{item:token1} to~\ref{item:token2} it is a \emph{write~token};
from steps~\ref{item:token3} to~\ref{item:token4} it is a \emph{read~token}.
At any moment, there are read~tokens from rank~$\head-\capacity$ to~$\tail$, and
write~tokens from~$\tail$ to~$\head$.
We have a last requirement: when an enqueuer is attributed rank~$\idx$, the new
item is added to the public state immediately---the CAS operation on \refhead
is the commit point of enqueuing---even though the enqueuer has not
actually written the item yet. When it finally returns the updated slot, the
enqueuer has lost track of the public state, which may have continued to
progress in the meantime. At that moment, it thus needs a reminder that the item
it just wrote is indeed the one it was expected to write.
%
We implement this by adding the value~$\elem$---and view~$\eview$---of the item
as a payload to the write~token.
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 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.
%
The next two say that tokens agree with the authoritative counterpart, hence with the public state.
%
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, rule~\ruleTokenUpdWR corresponds to step~\ref{item:token3}, where we turn a write~token into a read~token of the same rank.
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.
%To implement a token in ghost state, we again use an authority over an exclusive
%value.
%%The authority states the existence of the token.
%The authority represents the duplicate of the token.
%As we want one token for each rank in some range, we again use a finite partial
%function; however, this time its domain $[\head-\capacity, \head)$ is not fixed,
%so we apply the authority on the function itself. Hence, the CMRA of~$\gtokens$
%is $\authm\left(\finmapm{\Z}{\exm(M)}\right)$,
%where $M$ is a CMRA for the payload of the tokens.
%The token of rank~$\idx$, bearing the payload~$x \in M$, is
%$\ownGhost\gtokens{\authfrag \mapsingleton\idx x}$.
%
%To achieve the distinction between read~tokens and write~tokens, $M$ is
%a disjoint sum $M\sub{read} + M\sub{write}$.
%Read~tokens do not carry a payload,
% so we take for~$M\sub{read}$ the singleton set, $\typeUnit$.
%Write~tokens carry as their payload an item, that is, a value and a view,
% 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}.
% ------------------------------------------------------------------------------
There are more properties that are invariants of the queue, and thus could be stated
and verified. However, they are not needed to
prove that the code satisfies its specification. For example, the fact that \reftail and \refhead are
strictly monotonic, and the fact that statuses are non-negative, are not explicitly used.
\subsection{Logical atomicity}
\label{sec:queue:proof:la}
The specification that we wish to prove is a logically atomic Hoare triple.
The definition of such triples is given by~\citet[\S7]{iris-15} and
further refined by~\citet{jung-slides-2019}. We do not attempt to replicate
their explanation and full definition. An approximate definition that suffices to
capture the essence of logical atomicity, and to understand our proof, is:
%
\[\begin{array}{rcl}%
\lahoare{P}{e}{\pred}
&\eqdef&
\Forall \predB,
\left[ \pvs[\top][\emptyset] \Exists x.
P \ISEP \left(\Forall v. \pred\;v \WAND\pvs[\emptyset][\top] \predB\;v\right)
\right]
\WAND
\wpre e \predB
\end{array}\]%
In this formula,
the variable~$P$ is a Cosmo assertion (of type $\typeVProp$);
the variables~$\pred$ and~$\predB$ are predicates on values (of type $\typeVal \ra \typeVProp$);
$P$ and $\pred$ may refer to the name~$x$.
%
The assertion $\wpre e \predB$ is the weakest precondition for program~$e$ and
postcondition~$\predB$
(in Iris, Hoare triples are syntactic sugar for weakest preconditions).
The purpose of a logically atomic triple is to give a specification to a non-atomic program $e$ \emph{as if it were atomic}.
In practice, we require that the proof of $e$ accesses the precondition and turns it into the postcondition in \emph{one atomic step} only, which we call the commit point of this logically atomic program.
That is, if $e$ satisfies the triple $\lahoare{P}{e}{\pred}$, then it can perform several steps of computation but, as soon as it accesses the resource~$P$, it must return the resource~$\pred$ in the same step of computation.\footnote{The full definition of logically atomic triples allows to access the precondition atomically before the commit point, hence without turning it into the postcondition. This is called \emph{aborting}; it is not needed in our proof, and out of the scope of this paper.}
Once it has done so, $e$ can perform further computation steps but $P$ is not available anymore.
As explained in \sref{sec:queue:spec:sc}, thanks to this constraint, the client of this specification can open invariants around $e$ as if $e$ were atomic.
To capture this atomicity requirement, we ask the proof of the logically atomic triple for $e$ to be valid for any postcondition $\predB$ chosen by the client.
Given that $\predB$ is arbitrary, the only means of establishing this postcondition is to use the premise $\pvs[\top][\emptyset] \Exists x. P \ISEP (\Forall v. \pred\;v \WAND\pvs[\emptyset][\top] \predB\;v)$, which is known as an \emph{atomic update}.
When desired, this atomic update gives access to the precondition~$P$ for some value of $x$, and, in exchange for the postcondition $\pred$ of the logically atomic triple, it returns the resource $\predB$, which can then be used to finish the proof.
Crucially, the \emph{masks} $\emptyset$ and $\top$ annotating the \emph{fancy updates} $\pvs[\top][\emptyset]$ and $\pvs[\emptyset][\top]$ require that the atomic update be used during one atomic step only, as required.
Using the invariant rules of Iris~\cite{iris}, it is easy to show that atomic updates can be used to open and close invariants.
Rule~\rulelainv follows as a corollary, rule~\rulelahoare is immediate.
\subsection{Proof of \tryenqueue}
\label{sec:queue:proof:tryenqueue}
We now outline the proof that \tryenqueue satisfies its specification
from~\fref{fig:queue:spec:weak}.
%
The proof for \trydequeue is similar; those for \enqueue and \dequeue are
deduced from the previous two by an obvious induction; and the proof of \make is
simply a matter of initializing the ghost state.
%
The interested reader may
find these proofs, conducted in the Coq proof assistant, in our repository~\citep{repo}.
Recalling here the specification in~\fref{fig:queue:spec:weak}, and unfolding
the definition of $\queueInv$, we ought to prove the following assertion:
%
\[\begin{array}{@{}l@{}}
\infer{%
%\queueInv
\knowInv{}{\queueInvInner}
}{%
\lahoareV
{\begin{array}{@{}l@{}}
\lahoarebinder{\tview, \hview, \nbelems, \elemViewList*[]}
\\ \hspace{2.9em}
\isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList
\hphantom{, \pair\elem\view}
\ISEP \seen\view
\end{array}}
{\tryenqueue~\queue~\elem}
{\Lam \boolval.
\matchwithnobinder{\boolval}
{\False}{\isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList}
{\True }{%
\isQueue \tview {(\hview \sqcup \view)} {\elemListSnoc \elemViewList {\pair\elem\view}}
\ISEP \seen\hview
}
}
}
\end{array}\]
After unfolding the logically atomic triple, we must prove
$\wpre {(\tryenqueue\;\queue\;\elem)} \predB$ for any~$\predB$,
when in the proof context
we have the internal invariant of the queue (with ghost variables~$\gqueue, \gmonos, \gtokens$)
as well as the atomic update whose precondition and postconditions are that of the triple above.
We then step through the program using usual weakest-precondition calculus.
The first interesting step is the atomic read of \refhead. The ownership of that
reference is shared in the invariant of the queue. Hence, to access it, we must
open the invariant; then we get the pointsto assertion, we can step through the
read operation, return the pointsto assertion and close the invariant again.
After we have done so, and thus forgotten all the quantities which are
existentially quantified inside that invariant, we learn little about the value
that has just been read,
excepted that it is a nonnegative integer, say~$\idx$.
The second interesting step is the atomic read at index~$\modcap\idx$
of the array~\refstatuses. Again the invariant owns this cell, so we open it
around the read instruction. This read yields some value~$\status^1$ and,
since it is atomic, it also augments our current (thread) view with the
view~$\sview^1$ which, at this moment, is stored in this cell. In other words, we
gain the (persistent) assertion $\seen\sview^1$.
% (previously, the read to \refhead also augmented our current view, but we chose
% to ignore that fact as it is not useful in the proof).
We can remember more information before closing the invariant:
indeed, from the authority of~$\gmonos$ found in the invariant, we derive a
witness for the strict monotonicity of the status that we just read:
$\monoWitness {\modcap\idx} {\pair{\status^1}{\sview^1}}$.
Next, the program tests whether $\status^1 = 2\idx$. If the test fails, then
the program returns $\False$. In this case, we have to provide as postcondition
of the logically atomic triple the untouched representation predicate that is
in its precondition ($\isQueue \tview \hview \elemViewList$). We do this by
committing the atomic update in a trivial way, then conclude the proof.
If $\status^1 = 2\idx$, the program proceeds to performing
$\CAS \refhead \idx {(\idx+1)}$.
To access \refhead, we open the invariant again.
If that operation fails, the program also returns $\False$ and, after closing
the invariant without having updated ghost state, we conclude as before.
If the CAS succeeds, then a number of things happen logically.
First, if $\head$ and $\tail$ are the values of \refhead and \reftail at the
moment of the CAS, then $\head = \idx$.
Second, we deduce that the buffer is not full, i.e.\ $\head < \tail+\capacity$.
Indeed, the invariant directly gives us $\head \leq \tail+\capacity$;
if we had $\head = \tail+\capacity$, then in particular,
$\tail \leq \idx-\capacity < \head$, so the invariant would own the following
for slot~$\modcap{\idx-\capacity}$:
%
\[%
\fullCell {(\idx-\capacity)} {\nthStatusView{\modcap{\idx-\capacity}}} {\nthElemView{\idx-\capacity}}
\LOR
\status_{\modcap{\idx-\capacity}} = 2(\idx-\capacity)
\]%
%
Because $\modcap{\idx-\capacity} = \modcap\idx$, this implies:
%
\[%
\status_{\modcap\idx} = 2(\idx-\capacity) + 1
\LOR
\status_{\modcap\idx} = 2(\idx-\capacity)
\]%
%
In either case, we get $\status_{\modcap\idx} < 2\idx = \status^1$,
which contradicts the monotonicity of the status of that slot. We derive the
contradiction by combining the assertion
$\monoWitness {\modcap\idx} {\pair{\status^1}{\sview^1}}$
that we had since we read the status,
and the authority
$\ownGhost \gmonos {\authfull \nthStatusView{\modcap\idx}}$
that is found in the invariant.
Third, we thus know that $\head-\capacity \leq \idx-\capacity < \tail$, so
that the invariant gives us:
%
\[%
\emptyCell {(\idx-\capacity)} {\nthStatusView{\modcap{\idx-\capacity}}}
\LOR
\status_{\modcap{\idx-\capacity}} = 2(\idx-\capacity)+1
\]%
%
Again the second disjunct is absurd because the status is monotonic. Hence the slot we are claiming is available indeed.
%
From this
%$\emptyCell {(\idx-\capacity)} {\nthStatusView{\modcap\idx}}$,
we get
$\status_{\modcap\idx} = 2\idx = \status^1$,
the pointsto assertion $(\nthpointstoNA\refelements{\modcap\idx}-) \opat \sview_{\modcap\idx}$
and the read~token of rank~$\idx-\capacity$.
The sets of read~tokens and write~tokens depend on the value of \reftail and
\refhead, and we have just incremented the latter, to $\idx+1$, so we
destruct the read~token of rank~$\idx-\capacity$ and create a write~token of
rank~$\idx$ instead, giving it as payload the item~$\pair\elem\eview$ that we
are trying to enqueue.
This is also when the \emph{strict} monotonicity of the status comes into play:
because $\status_\idx = \status^1$, it gives us
$\sview_\idx \viewleq \sview^1$. But we have $\seen\sview^1$ in our proof
context, so we obtain the pointsto assertion as a subjective assertion:
$\nthpointstoNA\refelements{\modcap\idx}-$.
We commit the atomic update now. Indeed the successful CAS is the commit
point of \tryenqueue. We know that the program will return $\True$, so we must
provide the corresponding postcondition of the logically atomic triple, where
our item~$\pair\elem\eview$ has been appended to the public state of the queue.
Thus we take a ghost step to update this public state.
By committing, we finally obtain the assertion $\predB\;\True$
that will serve at the end of the proof,
since $\True$ is the return value of the operation.
Along the way, we also collect the persistent assertion $\seen\eview$ from the
precondition of the logically atomic triple.
Finally, we keep on our side the write~token, the nonatomic pointsto assertion
$\nthpointstoNA\refelements{\modcap\idx}-$,
we reconstruct the invariant, updated for the new value of \refhead, and we close it.
The next step of the program writes the value~$\elem$ to the nonatomic item field,
which is easy since we have the pointsto assertion at hand. This assertion then becomes
$\nthpointstoNA\refelements{\modcap\idx}\elem$.
We turn it back to an objective assertion, which gives us a view~$\viewB$ and
two assertions $\seen\viewB$ and
$(\nthpointstoNA\refelements{\modcap\idx}\elem) \opat \viewB$.
The last step of the program is to update the (atomic) status of the slot.
Once more we open the invariant.
If we again note $\head$ and $\tail$ the current values of \refhead and \reftail
(potentially different from the last time we opened the invariant),
then owning a write~token for rank~$\idx$ teaches us that $\tail \leq \idx < \head$.
The invariant then gives us for slot~$\modcap\idx$:
%
\[%
\fullCell \idx {\nthStatusView{\modcap\idx}} {\nthElemView\idx}
\LOR
\status_{\modcap\idx} = 2\idx
\]%
%
The left disjunct would own our write~token, but we already have it and it is exclusive;
hence we are in the right disjunct, $\status_{\modcap\idx} = 2\idx = s^1$.
We perform the atomic write with value~$\status^2 \eqdef 2\idx+1$ (strict
monotonicity is respected),
and since we have both $\seen\eview$ and $\seen\viewB$ in context, we can push
the view~$\sview^2 = \eview \viewjoin \viewB$ to this atomic location while
writing.
We then switch to the left disjunct, by constituting the assertion:
%
\[%
\fullCell \idx {\pair{\status^2}{\sview^2}} {\pair\elem\eview}
\;\iequiv\;
\isepV{%
\status^2 = 2\idx + 1
\cr (\nthpointstoNA\refelements{\modcap\idx}{\elem}) \opat \sview^2
\cr \tokenW\idx{\pair\elem\eview}
\cr \eview \viewleq \sview^2
}
\]%
%
Hence we return the nonatomic pointsto assertion and the write~token to the
invariant before closing it.
% FP: ça me paraît bien, tout ça.
% Il faudra sans doute numéroter les lignes du code
% et faire référence à des numéros précis dans le texte.