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

Changes.

parent 38944cdb
......@@ -33,6 +33,7 @@ modifications selon réponse aux rapporteurs:
- EXPLICATION ATOMICITÉ LOGIQUE? déjà bien couvert dans S 2.2 + 4.5…
+ JH va revoir S 4.5
* on n’a pas besoin de Abort
FAIT
- INTRO À IRIS ET À L’ÉTAT FANTÔME (au début de la S 4):
+ « c’est une manière flexible de définir une notion personnalisée de
......
......@@ -19,8 +19,6 @@
& \text{--- values} \\
& \mid& \None \mid \Some\val
\mid \Tuple{\val,\ldots,\val} \\
% GLEN: j’ai ajouté les tuples aux valeurs. Je ne sais plus si
% c’était volontaire de les en avoir enlevés.
{\AnyOp}& \IN & \{ \mathord{\PAnd}, \mathord{\POr},
\mathord+, \mathord\times, \mathord{\PMod}, \ldots \,\}
& \text{--- operators} \\
......
......@@ -11,8 +11,6 @@
\infer{~}{\persistent{\queueInv}}
\and
\infer{~}{\objective{\isQueue \tview \hview \elemViewList}}
% JH : mentionner que isQueue est timeless? Cela fait partie de la spec, à mon sens.
% GLEN: trop technique ?
\and
\hoareV
{\seen\view_0}
......
......@@ -119,12 +119,9 @@ so as to ensure that the consumer acquires the producer's view of this piece of
Our specification faithfully captures a subtle behavior of the implementation:
even though operations are totally ordered by logical atomicity,
not all operations are ordered by happens-before---but \emph{some} are.
% GLEN: la dernière phrase est déjà dite (en plus vague) au début de cet \item.
% Cet \item est peut-être trop détaillé ? On redit tout ça dans l’article.
\item We use the Coq proof assistant~\cite{coq} to formally verify our proofs.
Our development is available from our repository~\citep{repo}.
\end{itemize}
% TODO : d'autres challenges/contributions à faire figurer ici ?
We believe our approach, whose key ingredients are Cosmo and logical atomicity,
scales to other memory models and other data structures.
......
......@@ -166,3 +166,9 @@
url = {https://cs.au.dk/~timany/publications/files/2021_CPP_monotone.pdf}
}
@techreport{fraser2004practical,
title={Practical lock-freedom},
author={Fraser, Keir},
year={2004},
institution={University of Cambridge, Computer Laboratory}
}
......@@ -2,3 +2,28 @@
\label{sec:pipeline:impl}
\input{figure-pipeline-impl}
The code of the application is presented in~\fref{fig:pipeline:impl}.
It provides a single function, \pipeline, which takes as arguments two
functions~$g$ and~$f$, a stream~$\refXArray$, and returns a stream
obtained by applying $g \circ f$ to each item of the input stream.
The functions~$g$ and~$f$ need not be pure: they can have side effects and rely
on some state.
For simplicity, input and output streams are encoded as (nonatomic) arrays,
whose length can be obtained via a primitive operation $\Length -$.
However the implementation can be modified to consume and produce lists of
unknown length, or even infinite streams, provided an encoding of such
data~structures; we would then use a sentinel value in the queue to signal the
end of stream.
The code is straightforward: we create a concurrent queue~\refYQueue, then
we fork a thread.
The queue is shared between the main thread and the forked thread, while
\refXArray is transmitted to the forked thread.
The forked thread reads items from~\refXArray in turn, applies $f$ to them
and enqueues the results.
The main thread creates a new (nonatomic) array~\refZArray to store the output;
then, it dequeues $\nbelems$~items, where $\nbelems$ is the number of items in
the input stream, applies $g$ to them, and adds the results to \refZArray.
Finally, it returns~\refZArray.
......@@ -2,3 +2,13 @@
\label{sec:pipeline:proof}
\input{figure-pipeline-inv}
% TODO : écrit à l'arrache, améliorer.
The proof of the presented specification for the pipeline uses the invariants presented in \fref{fig:pipeline:inv}.
More precisely, $\pipelineInv R$ join together the queue invariant $\queueInv$ with the pipeline internal invariant $\pipelineInvInner R$.
In addition, $\pipelineF R \curf \refXArray \xElemList$ and $\pipelineG R \curg \refZArray \zElemList$ are loop invariants used in the two computing threads.
The pipeline invariant uses the ghost variables $\gcurf$ and $\gcurg$ to agree with the loop invariants on their position, and, in addition to owning the exclusive ownership of the queue, states that each element of the queue is associated with a weakest precondition assertion at the element's view allowing to execute the function $g$ on this element.
Once the invariants are stated and initialized, the proof is a straightforward induction over the length of the input stream: at each step of each thread, we execute either $f$ or $g$, we open the global pipeline invariant around the logically atomic triple of the enqueing or dequeueing operation.
When this invariant is opened, the state of the queue can be updated, and we perform an update on the ghost variables $\gcurf$ or $\gcurg$ to reflect the state change in the corresponding thread.
......@@ -2,3 +2,35 @@
\label{sec:pipeline:spec}
\input{figure-pipeline-spec}
A possible specification for this pipeline is shown in~\fref{fig:pipeline:spec}.
It is higher-order, and expressed using the weakest-precondition predicate.
In postcondition we obtain one assertion~$R\;k\;z_k$ for each item of the
stream, related to its position~$k$ (in particular, $R$ may relate the output
value~$z_k$ to the input value~$x_k$).
In the precondition, essentially, we want to state that for some
predicates~$P$ and $Q$,
we have the assertions~$P\;k\;x_k$ for all items of the input stream,
and functions~$f$ and~$g$ satisfy Hoare triples of the form:
\begin{align*}%
\hoare {P\;k\;x} {f\;x} {\Lam y. Q\;k\;y}
\\
\hoare {Q\;k\;y} {g\;y} {\Lam z. R\;k\;z}
\end{align*}%
so that, by the chaining rule, the composition satifies:
\[%
\hoare {P\;k\;x} {g\;(f\;x)} {\Lam z. R\;k\;z}
\]%
By using weakest preconditions instead of Hoare triples, we avoid mentioning
the predicate~$P$;
by taking advantage of the higher-order nature of Iris, we can nest the triples
so as to conceal the intermediate predicate~$Q$.
We use the primitive Cosmo assertion $\haslength\refXArray\nbelems$ to stipulate
that the length of a given array is~$\nbelems$ (recall that the array-pointsto
assertion is shorthand for a separating conjunction of pointsto assertions
for cells of the array in some range of indices, but it does not state that
there are no cells beyond those mentioned).
\section{A Simple Pipeline} % TODO: better title: producer-consumer stream?
\section{A Simple Pipeline}
\label{sec:pipeline}
% TODO JH : stream -> sequence
We now demonstrate the use of our specification in Cosmo of a concurrent queue
library with a simple client application, that chains two treatments on a stream
of data, where each treatment is applied by a separate thread. Thus the
......@@ -10,77 +12,6 @@ using a concurrent queue.
\input{pipeline-impl}
The code of the application is presented in~\fref{fig:pipeline:impl}.
It provides a single function, \pipeline, which takes as arguments two
functions~$g$ and~$f$, a stream~$\refXArray$, and returns a stream
obtained by applying $g \circ f$ to each item of the input stream.
% GLEN: souligner que f et g n’ont pas à être des fonctions pures ?
The functions~$g$ and~$f$ need not be pure: they can have side effects and rely
on some state.
For simplicity, input and output streams are encoded as (nonatomic) arrays,
whose length can be obtained via a primitive operation $\Length -$.
However the implementation can be modified to consume and produce lists of
unknown length, or even infinite streams, provided an encoding of such
data~structures; we would then use a sentinel value in the queue to signal the
end of stream.
% GLEN: très gros agitage de mains, l’invariant n’est sans doute pas immédiat
% à adapter…
The code is straightforward: we create a concurrent queue~\refYQueue, then
we fork a thread.
The queue is shared between the main thread and the forked thread, while
\refXArray is transmitted to the forked thread.
The forked thread reads items from~\refXArray in turn, applies $f$ to them
and enqueues the results.
The main thread creates a new (nonatomic) array~\refZArray to store the output;
then, it dequeues $\nbelems$~items, where $\nbelems$ is the number of items in
the input stream, applies $g$ to them, and adds the results to \refZArray.
Finally, it returns~\refZArray.
\input{pipeline-spec}
A possible specification for this pipeline is shown in~\fref{fig:pipeline:spec}.
It is higher-order, and expressed using the weakest-precondition predicate.
In postcondition we obtain one assertion~$R\;k\;z_k$ for each item of the
stream, related to its position~$k$ (in particular, $R$ may relate the output
value~$z_k$ to the input value~$x_k$).
In the precondition, essentially, we want to state that for some
predicates~$P$ and $Q$,
we have the assertions~$P\;k\;x_k$ for all items of the input stream,
and functions~$f$ and~$g$ satisfy Hoare triples of the form:
\begin{align*}%
\hoare {P\;k\;x} {f\;x} {\Lam y. Q\;k\;y}
\\
\hoare {Q\;k\;y} {g\;y} {\Lam z. R\;k\;z}
\end{align*}%
so that, by the chaining rule, the composition satifies:
\[%
\hoare {P\;k\;x} {g\;(f\;x)} {\Lam z. R\;k\;z}
\]%
By using weakest preconditions instead of Hoare triples, we avoid mentioning
the predicate~$P$;
by taking advantage of the higher-order nature of Iris, we can nest the triples
so as to conceal the intermediate predicate~$Q$.
% GLEN: est-ce qu’emboîter les WP n’est pas juste une façon compliquée
% d’écrire le WP de la composition ?
We use the primitive Cosmo assertion $\haslength\refXArray\nbelems$ to stipulate
that the length of a given array is~$\nbelems$ (recall that the array-pointsto
assertion is shorthand for a separating conjunction of pointsto assertions
for cells of the array in some range of indices, but it does not state that
there are no cells beyond those mentioned).
\input{pipeline-proof}
% TODO : écrit à l'arrache, améliorer.
The proof of the presented specification for the pipeline use the invariants presented in \fref{fig:pipeline:inv}.
More precisely, $\pipelineInv R$ join together the queue invariant $\queueInv$ with the pipeline internal invariant $\pipelineInvInner R$, and $\pipelineF R \curf \refXArray \xElemList$ and $\pipelineG R \curg \refZArray \zElemList$ are loop invariants used in the two computing threads.
The pipeline invariants uses the ghost variables $\gcurf$ and $\gcurg$ for agreeing with the loop invariant on their position, and, in addition to owning the exclusive ownership or the queue, states that each element of the queue is associated with a weakest precondition assertion at the element's view allowing to execute the function $g$ on this element.
Once the invariants are stated and initialized, the proof is a straightforward induction over the length of the input stream: at each step of each thread, we execute $f$ or $g$, we open the global pipeline invariant around the logically atomic triple of the enqueing or dequeueing operation.
When this invariant is opened, the state of the queue can be updated, and we perform an update on the ghost variables $\gcurf$ or $\gcurg$ to reflect the state change in the corresponding thread.
......@@ -78,45 +78,6 @@ property of the queue is:
0 \leq \tail \leq \head \leq \tail+\capacity
\]
%% We say that the buffer is \emph{full} when slot~$\modcap\head$ has
%% a status less than $2\head$; in other words, the next slot at which to enqueue
%% is still in use for a rank less than~\head.%
%% \footnote{%
%% Either the slot has status $2(\head-\capacity)$ and some thread
%% is in the process of enqueuing the item of rank~$\head-\capacity$,
%% or it has status $2(\head-\capacity)+1$ and is occupied by that item.
%% }
%% %
%% This is implied by, but is weaker than, the equation $\head = \tail+\capacity$.%
%% \footnote{%
%% Some thread may have commited to dequeue the item of rank~$\head-\capacity$
%% without having completed that task yet; \reftail would be greater than
%% $\head-\capacity$ but the slot would still appear as occupied for that rank.
%% }
%% We say that the buffer is \emph{empty} when slot~$\modcap\tail$ has a status
%% less than $2\tail+1$; in other words, the next slot from which to dequeue is
%% still in use for a rank less than~\tail.%
%% \footnote{%
%% Either the slot has status $2(\tail-\capacity)+1$ and some thread
%% is in the process of dequeuing the item of rank~$\tail-\capacity$,
%% or it has status $2\tail$ and is available for a future item of rank~\tail.
%% }
%% %
%% This is implied by, but is weaker than, the equation $\head = \tail$.%
%% \footnote{%
%% Some thread may have commited to enqueue an item of rank~$\tail$
%% without having completed that task yet; \refhead would be greater than
%% $\tail$ but the slot would still appear as available.
%% }
% GLEN: la terminologie "buffer vide/plein" est impropre: on dit que le buffer
% est "plein" quand la prochaine case où ajouter n’est pas encore vidée, mais
% il se peut que d’autres cases plus loin aient déjà été vidées (idem pour
% "vide").
\subsection{Explanation of the code}
\label{sec:queue:impl:code}
......@@ -205,8 +166,7 @@ Hence in favorable situations%
there are no enqueuer-dequeuer competitions
beyond ones between an enqueuer and a dequeuer of the same rank.
A weakness of this implementation, however, is that it is not non-blocking:
A weakness of this implementation, however, is that it does not enjoy any non-blocking property~\cite[Chapter 2]{fraser2004practical}:
if an enqueuer or a dequeuer halts after it has been attributed a rank but before
it updates the corresponding slot, then after some time, any other thread trying
to enqueue or dequeue fails.
% TODO : citer la thèse de Keir Fraser
......@@ -256,14 +256,15 @@ 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 placed in
an invariant as is.
%
In order to share this assertion,
we must explicitly indicate at which view it holds.
%
That is precisely the purpose of the $\opat$ connective.
% TODO : déplacer plus haut là où on introduit P@V
In \hlog, for any potentially subjective assertion~$\prop$, the objective
assertion~$\prop \opat \view$ means that $\prop$ holds \emph{provided}
that the view of the subject thread contains~$\view$.
......@@ -271,9 +272,6 @@ that the view of the subject thread contains~$\view$.
It can be roughly understood as $\seen\view \wand \prop$, but,
unlike this implication, it is objective.
% TODO: figure pour rappeler la règle Split-Subjective-Objective
% (et peut-être que P @ V ⊣⊢ Objectively(↑V -∗ P) ?)
%At which view do we own the item cell? In our queue implementation, the status
%field of a given slot plays the role of a ``lock'' for the item field of that slot.
%Not only does its value~$\status$ indicate whether the slot is available or occupied,
......@@ -585,8 +583,7 @@ If $\status^1 = 2\idx$, the program proceeds to performing
$\CAS \refhead \idx {(\idx+1)}$.
To access \refhead, we open the invariant again.
If that operation fails, the program also returns $\False$ and, after closing
the invariant unchanged, we conclude as before.
% GLEN: "invarant unchanged" maladroit
the invariant without having updated ghost state, we conclude as before.
If the CAS succeeds, then a number of things happen logically.
First, if $\head$ and $\tail$ are the values of \refhead and \reftail at the
......
......@@ -87,6 +87,7 @@ because it is an atomic instruction.
\end{mathpar}
% TODO: faire référence aux règles ci-dessus dans le texte.
% => JH
% mentionner qu’un triplet log. atomique implique le triplet usuel ? (1re règle)
% peut-être enlever le binder à cet endroit.
% TODO : expliquer la syntaxe des invariants, dire que \later est une technicité d'Iris
......@@ -120,7 +121,7 @@ a persistent assertion~$\queueInv$ and an exclusive assertion $\isQueueSC\elemLi
connected by a ghost name~$\gqueue$.
That splitting is an artifact of our correctness proof technique,
which we detail in~\sref{sec:queue:proof}.
% GLEN: 1re fois qu’on parle d’assertions persistantes , définir le terme ici.
% TODO : GLEN: 1re fois qu’on parle d’assertions persistantes , définir le terme ici.
%
Note that this does not complicate the use of the queue by the client:
both assertions are produced when creating the queue,
......
......@@ -16,8 +16,7 @@ which provides a proof framework for the weak memory model of \mocaml{}.
This memory model has been described by~\citet{dolan-18}
under the form of a small-step operational semantics.
Following previous authors, such as~\citet{kaiser-17},
the semantics features a notion of \emph{view}
% GLEN: in Dolan et al.’s paper, views are called "frontiers".
the semantics features a notion of \emph{view}\footnote{\citet{dolan-18} call these views \emph{frontiers}.}
which captures the essence of weak memory,
namely,
the fact
......@@ -78,9 +77,6 @@ synchronization between some of its concurrent accesses.
For example, imagine that thread~$A$ enqueues a pointer to a complex data structure (say, a hash table).
Then, when thread~$B$ dequeues this pointer, $B$ should obtain the unique ownership
of the hash table
(provided, of course, that $A$ did not access it once enqueued)
% TODO parenthèse discutable, car le fait qu'une permission soit transférée ou non
% est une décision statique et ne dépend pas du comportement dynamique du thread $A$
and be able to access it accordingly.
In a weakly consistent memory model, $B$ expects to see all of the changes that $A$ has made to the data~structure.
This is guaranteed only if there is a \emph{happens-before} relationship from
......@@ -102,7 +98,7 @@ In \hlog{}, happens-before relationships can be expressed as \emph{transfers of
To the user of this logic, views (denoted in this paper by calligraphic capital letters, such as $\mathcal{T,H,V,S}$) are abstract values
equipped with lattice structure:
the least view~$\emptyview$ is the empty view,
and larger views correspond to more recent knowledge. % TODO ou bien: more knowledge?
and larger views correspond to more recent knowledge.
If $\view$ is a view, the persistent assertion~$\seen\view$ indicates that the current thread has the knowledge contained in~$\view$.
\hlog{} provides reasoning rules about these assertions, shown in~\fref{fig:hlog:axioms}. We explain rule~\splitso in the next paragraph.
......
......@@ -26,7 +26,6 @@ fixed memory size. A motivation for that trait is that items may be enqueued
more frequently than they are dequeued; in this situation, a bounded queue has no risk of
exhausting system memory; instead, if the maximum size is reached,
enqueuing either blocks or fails.
% TODO: ref for bounded pools/queues: Herlihy & Shavit 10.1
% FP ce n'est pas seulement une question de limiter l'occupation mémoire
% de la file, mais aussi une façon de forcer les producteurs à attendre
% une fois que la file est pleine; donc c'est un mécanisme de contrôle
......
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