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

Weak memory.

parent f485aa75
......@@ -6,14 +6,14 @@
Up to now, we ignored 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.
We will use the separation logic Cosmo~\citecosmo:
We will use the separation logic \hlog{}~\citecosmo:
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.
Because \hlog{} 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.
However, as such, this specification is of little value in a weakly consistent context.
Indeed, as we explained in~\sref{sec:queue:spec:sc}, 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.
But, in \hlog{}, 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$.
......@@ -28,18 +28,19 @@ In particular, our library guarantees \emph{happens-before} relationships betwee
\end{enumerate}%
These happens-before relationships are important to use the queue in practice.
For example, imagine that thread~$A$ enqueues a complex data structure in the queue (say, a hash table).
For example, imagine that thread~$A$ enqueues a pointer to a complex data structure in the queue (say, a hash table).
Then, when thread~$B$ dequeues the corresponding item, one naturally expects that thread~$B$ is able to access the data structure as if it were its unique owner (provided, of course, that thread~$A$ did not access the data structure once enqueued).
In a weakly consistent memory model, this is only possible if there is a happens-before relationship between enqueuing and dequeuing: otherwise, nothing guarantees that thread~$B$ has seen all the changes made by thread~$A$ to the data structure.
% TODO : il faut expliquer quelque part comment les relations happens-before s'expriment par des transferts de vues
In \hlog{}, happens-before relationship can be expressed as \emph{transpher of views}.
In this logic, views (noted in this paper using calligraphic capital letters, such as $\mathcal{T,H,V,S}$) are abstract values denoting the knowledge of a thread of the current state of the global shared memory.
They are equipped with a lattice structure: larger views correspond to more recent knowledge.
In \hlog{}, when $\view$ is a view, the persistent assertion $\seen\view$ denotes that the current thread has the knowledge contained in $\view$.
In order to specify a happens-before relationship between two program points of two threads, we simply have to give the client the ability to transfer any such assertion between the two program points: this correspond to saying that the destination program point has all the knowledge the source program point had on the shared memory.
As is usual in \hlog{}~\cite{mevel-jourdan-pottier-20} and seen later with the example of the pipeline, % FP pointeur?
this can be used for transferring subjective resources from a sender to a receiver.
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
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:
%
......@@ -68,7 +69,7 @@ a dequeuer to an enqueuer.%
This is not entirely true: the implementation that we study does create
a happens-before relationship 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.
We choose to not reveal this in the specification, since the constant $C$ is hidden from the specification.
}
%
Hence, by contrast with a sequential queue that would
......@@ -81,10 +82,11 @@ retains an interesting behavior that should suffice for many use cases.
% 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?
% JH : Je ne suis pas sûr de l'usage précis dans la littérature, mais, dans ce paragraphe, on commence par dire que c'est linéarisable, puis on finit par dire que cela ne l'est pas.
% Ce que je propose (mais je ne sais pas si c'est standard) : dire que /linéarisable/, c'est qu'il existe un ordre total sur les accès, et que ces accès respectent cet ordre (i.e., agissent uniquement sur l'état courant dans cet ordre). Donc notre queue est linéarisable. Par contre, elle n'est pas /séquentiellement consistente/, puisqu'elle ne garantit pas tout ce qu'elle pourrait en terme d'happens-before
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
just presented, capturing the mentioned happens-before relationships as follows.
Interestingly, \hlog{} is able to express this subtle difference between the behavior of our library and that of lock-based implementation: the full specification under weak memory is shown in~\fref{fig:queue:spec}.
It extends the previous specification (\fref{fig:queue:specsc}) with views, capturing the mentioned happens-before relationships as follows.
\begin{enumerate}%
......
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