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

Comments

parent 856f11d1
......@@ -116,6 +116,7 @@ a queue: the same specification could also describe a stack or a bag.
% critique protégée par un verrou). On introduit donc des triplets
% logiquement atomiques, qui permettent d’ouvrir des invariants autour de
% tels programmes.
% JH : Oui, je ne tiens pas à garder la première option. En fait, à vrai dire, je l'avais laissée parce que je pensais que tu y tenais. Ce que tu propose me semble très bien.
Another option is to keep exposing a specification akin to that of~\fref{fig:queue:specseq}, that relies on an exclusive representation predicate allowing for the most exact description of the public state, and let clients share it themselves by applying a technique commonly used in Iris-like logics%
%to keep a precise description of the state that is stable in the face of interference by other threads
......@@ -159,6 +160,12 @@ This linearization point being atomic, it allows the opening of invariants just
% I doit pouvoir parler de x, il me semble ?
% peut-être enlever le binder à cet endroit.
% JH : le mieux, c'est peut-être de mettre ces règles dasn une figure, et de s'y référer à plusieurs endroits:
% 1- regardez, on peut ouvrir des invariants autour d'un triplet logiquement atomique (oubliez le binder pour l'instant)
% 2- maintenant que je vous ai expliqué ce que c'est ce binder, vous voyez, il apparaît dans la syntax
% 3- tout à la fin de 2.2.2, on peut parler de transformer un triplet logiquement atomique en triplet de Hoare au moment où on parle de déduire la spec à base de \Phi.
% 3bis- Si on décide de ne pas parler de la spec à base de \Phi au début du paragraphe, soit on en parle à la fn de 2.2.2, parce que ça fait un bon exemple, soit on en parle pas du tout, et il faut parler de la trasformation d'un triplet log. atom. en triplet de Hoare en agitant les mains.
Using logically atomic triples, the specification can be written as shown
in~\fref{fig:queue:specsc}.
It closely resembles that of the sequential setting (\fref{fig:queue:specseq}).
......@@ -173,11 +180,7 @@ The last difference of the sequentially consistent concurrent specification is t
That splitting is an artifact of our correctness proof techniques which we detail in
% TODO : section de la preuve de la queue.
.
Note that this does not complicate the use of the queue by the client: both parts of the representation predicate are produced at the same time when creating the queue, and the part $\queueInv$, which the client cannot share using an invariant (since it is mentioned as a general premise rather than in the pre/postconditions of the logically atomic triples) is persistent and therefore freely duplicated and shared among threads.
% GLEN: "which the client cannot share using an invariant" --> confusant ?
% il "peut", mais alors il ne sera pas en mesure d’utiliser les triplets
% logiquement atomiques qu’on lui fournit.
Note that this does not complicate the use of the queue by the client: both parts of the representation predicate are produced at the same time when creating the queue, and the part $\queueInv$, which is not adapted to sharing using an invariant (since it is mentioned as a general premise rather than in the pre/postconditions of the logically atomic triples) is persistent and therefore freely duplicated and shared among threads.
The use of such a specification in a concrete example will be detailed in
% TODO : référence Section pipeline
......@@ -189,9 +192,6 @@ Indeed, one would simply define $\isQueuePers\Phi$ as the conjuction of $\queueI
\]
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.
% 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é).
%% Indeed, after creating the queue (and getting the assertions $\isQueueSC{[]}$ and $\queueInv$), one simply has to create the new Iris invariant $\knowInv{}{\Exists \nbelems, \elemList*. A%% \isQueueSC\elemList
%% %% \isep \displaystyle\Sep_{0 \leq i < \nbelems} \Phi %% \nthElem\idx
......
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