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

rephrase weakly consistent behavior spec

parent 9ac3aa9d
......@@ -24,3 +24,4 @@
\caption{A specification of the ``queue'' data structure under sequential consistency}
\label{fig:queue:specsc}
%\end{figure}
% JH : TODO : serait-ce pertinent de mentionner ici la timelessness de isQueue et la persistence de queueInv? Cela fait partie de la spec, à mon sens.
......@@ -98,3 +98,4 @@
\caption{A specification of the ``queue'' data structure}
\label{fig:queue:spec}
\end{figure}
% JH : TODO : serait-ce pertinent de mentionner ici la timelessness et l'objectivité de isQueue et la persistence de queueInv? Cela fait partie de la spec, à mon sens.
......@@ -46,6 +46,7 @@ enqueued. % (by some other thread).
\end{figure}
\subsubsection{Specification under sequential consistency}
\label{sec:sc-spec}
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?
......@@ -186,24 +187,32 @@ Then, for proving the weaker specification of $\enqueue$ and $\dequeue$, one sim
\input{figure-queue-spec}
We now consider as a framework the weak memory model of \mocaml{}.
Up to now, we ignore the weakly consistent behavior of the semantics of \mocaml{}.
In this section, we lift this restriction, and propose a more precise specification for our concurrent queue implementation, which takes into account this aspect.
% TODO: introduce Cosmo
We will use the separation logic Cosmo~\cite{TODO}% TODO
: this framework has been designed on top of Iris in order to provide a powerful proof framework for the weak memory model of \mocaml{}.
Because Cosmo is based on Iris, logically atomic triples can also be defined in this logic.
In fact, the specification shown in~\fref{fig:queue:specsc} still applies.
The implementation we consider takes care of using atomic cells in some
places, ensuring thread safety. As a consequence, the specification shown
in~\fref{fig:queue:specsc} still applies.
%
However, under weak memory, our implementation also achieves some
synchronization, and we can reflect this with a stronger specification.
Namely, there are happens-before relationships:
However, as such, this specification is of little value in a weakly consistent context.
Indeed, as we explained in \sref{sec:sc-spec}, that specification is designed so that the representation predicate $\isQueueSC\elemList$ should be shared among threads by using an invariant.
But, in Cosmo, invariants are restricted to a special class of assertions, called \emph{objective} assertions.
As a result, the specification shown in~\fref{fig:queue:specsc} is useful in a weakly consistent context only if the representation predicate $\isQueueSC\elemList$ is objective.
Hence, the first addition in our specification to take into account weakly consistent behaviors is the objectiveness of $\isQueueSC\elemList$.
This correspond to asserting that the use of atomic accesses in the concurrent queue library is sufficient to maintain its linearizability.
In a weakly consistent context, the concurent queue library is not only linearizable: calls to the concurrent queue library also provides guarantees for memory accesses \emph{outside} of the queue.
In particular, our library guarantees \emph{happens-before} relationships between some function calls:
\begin{enumerate}%
\item from an enqueuer to the dequeuer that obtains the corresponding item;
\item from an enqueuer to the next enqueuer;
\item from a dequeuer to the next dequeuer.
\item from an enqueuer to the following enqueuers;
\item from a dequeuer to the following dequeuers.
\end{enumerate}%
% TODO : il faut expliquer quelque part comment les relations happens-before s'expriment par des transferts de vues
We are able to express and prove these relationships within \hlog{} as transfers
of views. As seen later with the example of the pipeline, % FP pointeur?
this can be used for
......
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