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

more about the repr. of slots in the invariant

parent 309bd849
......@@ -145,6 +145,9 @@ $\nthpointstoAT\reftail0{\mkval\tail\tview}$.
Pointsto assertions for atomic cells are objective and can freely be put in the
invariant.
% TODO: rappeler les triplets pour les accès atomiques ?
% TODO: dire que la vue de \reftail / \refhead est celle de l’état public
Apart from this physical state, the invariant also stores ghost state. It owns
the authority on all three ghost variables, $\gqueue$, $\gmonos$ and $\gtokens$.
%
......@@ -294,6 +297,7 @@ 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$.
% TODO: rappeler les triplets pour les accès atomiques ?
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.
......@@ -360,6 +364,21 @@ With that said, a first attempt at representing the buffer may end up as follows
\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$.
Indexes from~$\head-\capacity$ to~$\tail$ correspond to available slots,
while indexes 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 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$.
% …
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