Commit 834c1074 authored by Glen Mével's avatar Glen Mével
Browse files

address some todos

parent 6e1c2f00
......@@ -189,15 +189,13 @@ not changed since we read it: the slot is still available.
We write the new item, then we update the status accordingly. This update must
come last, as it serves as a signal that the slot is now occupied with an item
and ready for dequeuers.
%Notice that, under weak memory, the order of these two writes matters: the
%
%Notice that, under weak memory, another reason why the order of these two writes matters is that the
%atomic write to \refstatuses must propagate the information that the nonatomic
%write to \refelements has taken place. Thus, a thread which dequeues this item
%(after reading its status) is certain to read a correct value from the array
%\refelements. This is a typical release/acquire idiom.
% TODO : JH : Ok, mais c'est aussi nécessaire dasn un modèle SC, puisque l'écriture du statut correspond au relacheemnt du lock : si on s'amusait à remplir la cellule après écrire dasn statut, alors le dequeuer pourrait commencer à lire le contenu de la cellule avant que celle-ci ait été remplie, non ? Pour moi, c'est une meilleure justification pour l'odre des opérations. Les questions de mémoire faible sont plus subtiles et nécessitent d'avoir compris un peu la spec.
Similarly, \dequeue repeatedly calls \trydequeue untils it succeeds;
the latter works analogously to \tryenqueue,%
%
......
......@@ -178,11 +178,9 @@ Indeed, one would simply define $\isQueuePers\Phi$ as the conjuction of $\queueI
\[
\knowInv{}{\Exists \nbelems, \elemList*[]. \isQueueSC\elemList \isep \Phi\,\nthElem{0} \isep \cdots \isep \Phi\,\nthElem{\nbelems-1}}
\]
This is trivial to produce at the creation of the queue, when \make hands us the assertions $\queueInv$ and $\isQueueSC{[]}$
% TODO: ça laisse penser qu’il faut ajouter la spec de make en SC (et en
% séquentiel, pour la symétrie).
This is trivial to produce at the creation of the queue, when \make hands us the assertions $\queueInv$ and $\isQueueSC{[]}$.
Then, for proving the weaker specification of $\enqueue$ and $\dequeue$, one would open the invariant around the associated logically atomic triples.
% TODO : faut-il en dire plus, ou est-ce compréhensible tel quel?
% JH: faut-il en dire plus, ou est-ce compréhensible tel quel?
% GLEN: ça me semble suffisant (j’ai ajouté qu’il faut garder l’invariant
% interne, \queueInv, à côté).
......
......@@ -12,6 +12,7 @@ is represented in separation logic with a assertion:
In a sequential setting, we can give a simple specification to the operations of
the queue, as presented in~\fref{fig:queue:specseq}. We use the standard Hoare
triple notation, with a partial correctness meaning.
% TODO: ref for Hoare triples?
%
If we own a queue~$\queue$, then we can $\enqueue$ some item~$\elem$
into~$\queue$; if this operation ever returns, then it must return the unit value~$\Unit$ and
......
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