@@ -187,7 +187,7 @@ Then, for proving the weaker specification of $\enqueue$ and $\dequeue$, one sim

\input{figure-queue-spec}

Up to now, we ignore the weakly consistent behavior of the semantics of \mocaml{}.

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~\cite{TODO}% TODO

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).

Then, when thread $B$ dequeues the corresponding cells, 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 enqueueing 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

We are able to express and prove these relationships within \hlog{} as transfers