Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

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

ICFP21 paper: axiomatize tokens, don’t explain their implementation

parent 0a27e850
......@@ -64,7 +64,7 @@ Formally, the two assertions satisfy the following properties:
}{%
\tview = \tview'
\land \hview = \hview'
\land \Forall i. \val_i = \val'_i
\land \Forall i. \elem = \elem'_i
\land \eview_i = \eview'_i
}
......@@ -232,7 +232,7 @@ the following join-semilattice structure:
\end{cases}%
\end{array}\]%
\subsection{Description of slots}
\subsection{Available and occupied slots}
The last two lines of the invariant describe the state of each slot.
For clarity, we introduce two abbreviations:
......@@ -343,12 +343,14 @@ 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}
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. The 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
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
......@@ -360,7 +362,7 @@ part of the invariant:
\]%
We also maintain in existence one token for each rank from~$\head-\capacity$
to~$\head$. These tokens are exclusive assertions, and there never exist two tokens
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$.
%
......@@ -405,25 +407,82 @@ 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.
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}.
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
{\tokenR\idx \ISEP \tokenR{\idx'}}
{\modcap\idx \neq \modcap{\idx'}}
\infer
{\tokenR\idx \ISEP \tokenW{\idx'}{\pair{\elem'}{\eview'}}}
{\modcap\idx \neq \modcap{\idx'}}
\infer
{\tokenW\idx{\pair\elem\eview} \ISEP \tokenW{\idx'}{\pair{\elem'}{\eview'}}}
{\modcap\idx \neq \modcap{\idx'}}
\\
% this rule is not really needed:
\infer
{\ownGhost\gtokens{\authfull m} \ISEP \tokenR\idx}
{\maplookup{m}\idx = \Unit}
\infer
{\ownGhost\gtokens{\authfull m} \ISEP \tokenW\idx{\pair\elem\eview}}
{\maplookup{m}\idx = \pair\elem\eview}
\\
\infer
{\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
{\ownGhost\gtokens{\authfull m} \ISEP \tokenW\idx{\pair\elem\eview}}
{\upd
\ownGhost\gtokens{\authfull \mapupdate{m} \idx \Unit} \ISEP \tokenR\idx}
%
\end{mathpar}
%
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$.
%
Likewise, the last rule 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) of rank~$\idx$, that rank 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}.
%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$.
%
......@@ -439,8 +498,8 @@ Read~tokens and write~tokens are then defined as shown in~\fref{fig:queue:inv}.
% ------------------------------------------------------------------------------
There are more properties that are invariants, and thus could be stated
as part of our invariant and verified. However, these properties are not needed to
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.
......
......@@ -215,7 +215,7 @@ Section Spec.
Notation Zlength ls := (Z.of_nat (length ls)) (only parsing).
(* ICFP21: This is the definition of the ghost state representing slot tokens
(Section 4.4 of the paper).
(Section 4.5 of the paper).
Whereas the paper uses finite maps over Z, here we model them using lists.
There isnt really a technical advantage in doing so, to be honest, and it
requires careful shifting so that no negative index is involved. *)
......
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