Commit f1ead547 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

..

parent a68c0812
......@@ -63,7 +63,7 @@
\LetRecIn\var{\var,\ldots,\var}\expr\expr
& \text{--- definitions of recursive functions} \\
&\mid &
\LetIn\var[\var,\ldots,\var]\expr\expr
\LetIn\var[\ldots,\var]\expr\expr
\mid \expr ; \expr
& \text{--- sequencing} \\
&\mid &
......
......@@ -39,3 +39,8 @@ There is syntactic sugar for single-cell locations, or ``references'':
$\AllocANY\val$ allocates a location of length~one, $\ReadANY\loc$ reads at
offset~zero, $\WriteANY\loc\val$ writes at offset~zero and
$\CAS\loc{\val_1}{\val_2}$ performs compare-and-set at offset~zero.
% JH : TODO :
% - ne serait-il pas pertinent de mettre un at aussi pour le CAS des tableaux ?
% - en OCaml, c'est <- pour les tableaux et := pour les référence. Pourquoi fait-on l'inverse ici ?
% - Il y a une ambiguïté dans la syntaxe des CAS pour les tableaux "CAS a[b] c d" peut à la fois parler du CAS dans un tableau mais aussi du CAS d'une référence stockée dans un tableau
......@@ -32,7 +32,7 @@ into~$\queue$; if this operation ever returns, then it must return the unit valu
give us back the ownership of~$\queue$, where $\elem$ has been appended at the head.
%
Conversely, if we own a queue~$\queue$, then we can $\dequeue$ from~$\queue$; if
this operation ever returns, then it must return some item~$\elem$ which was in fact the item~$\elem_0$ found at
this operation ever returns, then it must return the first item~$\elem_0$ found at
the tail of~$\queue$, and it gives us back the ownership of~$\queue$, where that
first item has been removed. This specification implies that $\dequeue$ cannot possibly return when the queue is empty
($\nbelems = 0$); in this case, it must loop forever.
......@@ -52,7 +52,7 @@ enqueued. % (by some other thread).
\subsubsection{Specification under sequential consistency}
We now allow for several threads to run concurrently. Let’s assume for now that
We now consider the case where several threads access the queue concurrently. Let’s assume for now that
the memory model is sequentially consistent. % FP ajouter une référence?
%
We may retain the exact same specification as is presented
......@@ -82,24 +82,28 @@ Both $\enqueue$ and $\dequeue$ have a 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
describe the state of the queue (ghost state).
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$.
not require its exclusive ownership. In this context, it is important that the
ownership of the queue data structure can be shared among several threads.
%% 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
%% describe the state of the queue (ghost state).
One possibility to address this constraint is to use persistent assertions in order to replace the representation predicate $\isQueueSEQ\elemList$ of the queue.
With this choice, 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 guaranteeing only that all of the
elements stored in the queue satisfy some predicate~$P$.
......@@ -121,15 +125,20 @@ elements stored in the queue satisfy some predicate~$P$.
\end{array}\]
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.
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 description of the state that
resists operations by other threads.
There is a common technique used in Iris-like logics to keep a precise description of the state that is stable in the face of interference by other threads : one would typically place the (exclusive) ownership of the state in an invariant which is agreed upon by all the threads.
Then, when one of the threads needs to access the shared resource, it can \emph{open} the invariant, perform the shared state operations it needs, reestablish the invariant, and finally close it.
However, in order to be sound, the use of invariants in Iris need to follow a strict constraint: they can only stay opened for an \emph{atomic} duration (i.e., during an atomic instruction, or be closed immediately after being opened).
Unfortunately, $\enqueue$ and $\dequeue$ perform complex operations and are not atomic.
% 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.
......@@ -138,7 +147,12 @@ resists operations by other threads.
% \cite[\S7]{iris-15}
% \cite{jung-slides-2019}
Logical atomicity allows to write the specification shown
The idea of logical atomicity~\cite[\S7]{jung-slides-2019,iris-15} aims at addressing that difficulty.
When using this concept, instead of using ordinary Hoare triples, we use \emph{logically atomic triples}.
This kind of triple are like Hoare triples: they specify a program fragment, have a precondition and a postcondition.
The core difference being that they allow the opening of invariants around the triple
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
......
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