Commit d260f4ba authored by POTTIER Francois's avatar POTTIER Francois
Browse files

A few typos and comments.

parent 4af0200b
......@@ -163,6 +163,15 @@ The universal quantifier ($\forall \nbelems, \elemList {.}$) is part of the
syntax of an atomic triple: it binds the following variables in the precondition as
well as in the postcondition.
% FP on peut se demander ce que signifie intuitivement cette spec,
% et surtout comment elle peut être exploitée utilement par un
% client.
% FP il serait sans doute bon d'affirmer (et d'expliquer) que
% que cette spec avec des triplets logiquement atomiques
% permet de retrouver la spec faible où tous les éléments
% satisfont un prédicat P
\subsubsection{Specification under weak memory}
\input{figure-queue-spec}
......@@ -186,8 +195,12 @@ Namely, there are happens-before relationships:
\end{enumerate}%
We are able to express and prove these relationships within \hlog{} as transfers
of views. As seen later with the example of the pipeline, this can be used for
transferring subjective resources from a sender to a receiver. To reflect this,
of views. As seen later with the example of the pipeline, % FP pointeur?
this can be used for
transferring subjective resources from a sender to a receiver.
% FP as-tu expliqué l'idée de subjective resource? la notion de vue?
% et comment transférer une vue permet de transférer une ressource?
To reflect this,
the representation predicate now takes more parameters:
\[
......@@ -209,18 +222,25 @@ the representation predicate now takes more parameters:
\end{enumerate}%
The queue, however, does not guarantee any happens-before relationship from
a dequeuer to an enqueuer%
a dequeuer to an enqueuer.%
%
\footnote{%
This is not entirely true: the implementation that we show later does achieve
an happens-before from the dequeuer of rank~$\idx$ to the enqueuer of
rank~$\idx+\capacity$ (hence to all enqueuers of subsequent ranks).
We will not reflect it in the specification.
This is not entirely true: the implementation that we show later does create
a happens-before relation from the dequeuer of rank~$\idx$ to the enqueuer of
rank~$\idx+\capacity$ (hence also to all enqueuers of subsequent ranks).
We choose to not reveal this in the specification.
}%
%
. Hence, by contrast with a sequential queue that would
Hence, by contrast with a sequential queue that would
be guarded by a lock, the concurrent queue is not linearizable, even though it
retains an interesting behavior that should suffice for many use cases.
% FP ce serait bien de donner un exemple de scénario où le comportement
% de la queue est conforme à la spec et néanmoins non linéarisable;
% sinon ça reste vague, je trouve
% FP "that should suffice for many use cases" n'est pas très convaincant.
% a-t-on une idée plus claire, un argument plus convaincant? quel
% serait le type de situation où cette queue ne convient pas et on
% a absolument besoin d'une queue linéarisable?
The full specification under weak memory is shown in~\fref{fig:queue:spec}.
It extends the previous specification (\fref{fig:queue:specsc}) with views as
......@@ -231,17 +251,20 @@ just presented, capturing the mentioned happens-before relationships as follows.
\item When a thread with a local view at least~$\view$ (in other words, with
$\seen\view$ as a precondition) $\enqueue$s an item~$\elem$, it pairs it
with the view~$\view$.
% FP il faudra ré-expliquer les notations Cosmo, et peut-être le principe
% de certaines règles de preuve, en particulier le fait que les lectures
% et écritures dans une case atomique transfèrent une vue
%
Afterwards, when another thread $\dequeue$s that same item~$\elem_0$, it
merges the view~$\eview_0$ that was paired with it into its own local view
(in other words, it obtains $\seen\eview_0$ as a postcondition).
\item When a thread $\enqueue$s an item, it also obtain the head~view~$\hview$
\item When a thread $\enqueue$s an item, it also obtains the head~view~$\hview$
left by the previous enqueuer (in other words, it obtains $\seen\hview$ as
a postcondition), and it adds its own view~$\view$ to the head~view (which
becomes $\hview \viewjoin \view$).
\item When a thread $\dequeue$s an item, it also obtain the tail~view~$\tview$
\item When a thread $\dequeue$s an item, it also obtains the tail~view~$\tview$
left by the previous dequeuer (in other words, it obtains $\seen\tview$ as
a postcondition), and it adds its own view~$\view$ to the tail~view (which
becomes $\tview \viewjoin \view$).
......
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