Commit 4af0200b authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Small tweaks and comments.

parent 01412586
......@@ -43,12 +43,16 @@ in the presence of concurrency,
where it makes sense for $\dequeue$ to wait until an item is
enqueued. % (by some other thread).
% FP peut-être pourrais-tu noter aussi que cette spec peut décrire une
% queue de capacité bornée; dans ce cas il faut aussi que enqueue
% boucle quand la capacité est atteinte.
\subsubsection{Specification under sequential consistency}
\input{figure-queue-spec-sc}
We now allow for several threads to run concurrently. Let’s assume for now that
the memory model is sequentially consistent.
the memory model is sequentially consistent. % FP ajouter une référence?
%
We may retain the exact same specification as is presented
in~\fref{fig:queue:specseq}, recalling that $\isQueueSEQ\elemList$ is an
......@@ -64,13 +68,29 @@ to operate on the queue.
The resource would be transferable between threads via some mean of
synchronization: for instance, we may use a lock to guard all operations on the
shared queue.
However the implementation that we seek to prove correct is already thread-safe.
% FP noter que c'est l'approche de la logique de séparation concurrente
% traditionnelle, pioneered by \citet{ohearn-07}
% FP as-tu annoncé plus tôt à quelle implémentation tu t'intéresses?
% sinon, tu pourrais écrire, de façon plus abstraite, que "some
% implementations of concurrent queues are thread-safe by design,
% so that they do not need to be protected by a lock".
However the implementation that we wish to prove correct is already thread-safe.
Both $\enqueue$ and $\dequeue$ have a linearization point.
% FP Je ne sais pas forcément ce que signifie "linearization point",
% surtout que l'on parle d'une structure qui n'est pas (forcément)
% linéarisable, me semble-t-il. Supprimer cette ligne?
Hence we can achieve finer-grain concurrency, where operating on a queue does
not require its exclusive ownership. In this context, the queue data~structure
will be described by an \emph{invariant}. It is a persistent assertion, that can
be freely duplicated and holds true for all threads.
% FP il me semble que "invariant" et "ghost state" sont des outils techniques
% qui participent à la preuve, mais ici on est en train de discuter la spec.
% Au niveau de la spec, il faut surtout pointer d'abord qu'on va avoir besoin
% de partager l'accès à la queue, donc 1- isQueue ne peut plus être exclusif;
% il doit être partagé d'une façon ou d'une autre (il pourrait être
% fractionnel ou persistant, par exemple) et 2- un participant ne peut
% plus espérer connaître avec certitude le contenu actuel de la queue.
%
We will denote our invariant as $\queueInv$; it connects the physical
queue~$\queue$ with a logical-level variable~$\gqueue$, which will be used to
......@@ -80,8 +100,8 @@ An issue is then how to describe the state of the queue. Since any thread can
change it at any moment, no thread can know the current state to be some list
$\elemList$.
%
We may give a weaker specification by only guaranteeing, for example, that
elements stored within the queue all satisfy some predicate~$P$.
We may give a weaker specification by guaranteeing only that all of the
elements stored in the queue satisfy some predicate~$P$.
\[\begin{array}{lcr}
......@@ -116,22 +136,31 @@ elements stored within the queue all satisfy some predicate~$P$.
This is not satisfactory, as we lose most structural properties of a queue: the
same specification could also describe a stack, a bag or even (if $P$ is
duplicable) a single memory cell always returning the same value.
% FP la remarque sur P duplicable est un peu étrange, car a priori
% la file est polymorphe en P donc ne peut pas avoir ce comportement.
% de plus une cellule mémoire unique = une file de capacité 1,
% donc ce n'est pas vraiment un exemple différent des précédents.
It is not obvious how to keep a precise enough description of the state that
It is not obvious how to keep a precise description of the state that
resists operations by other threads.
% FP "resists" c'est pas mal, mais on pourrait écrire aussi
% "that is stable in the face of interference by other threads",
% ça évoquerait une terminologie standard.
% TODO: explain logical atomicity
% \cite[\S7]{iris-15}
% \cite{jung-slides-2019}
Logical atomicity allows to write the specification shown
in~\fref{fig:queue:specsc}. It closely resembles that of the sequential setting
(\fref{fig:queue:specseq}). Differences are that the assertion describing the
state of the queue ($\isQueueSC\elemList$) now talks about the ghost
name~$\gqueue$, that the invariant of the queue ($\queueInv$) is an additional
precondition of both operations (repeating it in postcondition is unneeded,
precondition of both operations (repeating it in the postcondition is unneeded,
as it is persistent) and that \emph{atomic} Hoare triples are used.
%
The ``forall'' quantifier ($\forall \nbelems, \elemList {.}$) is part of the
syntax of the triple: it binds the following variables in the precondition as
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.
\subsubsection{Specification under weak memory}
......
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