Commit 71c99a3a authored by Glen Mével's avatar Glen Mével
Browse files

English fixes

parent 86021dc5
......@@ -121,7 +121,7 @@ elements stored in the queue satisfy some predicate~$\Phi$.
\end{array}\]
This is not satisfactory, as we lose most structural properties of a queue: the
same specification could also describe a stack, a bag.
same specification could also describe a stack or a bag.
%% or even (if $\Phi$ is
%% duplicable) a single memory cell always returning the same value.
% FP la remarque sur \Phi duplicable est un peu étrange, car a priori
......@@ -141,8 +141,8 @@ Unfortunately, $\enqueue$ and $\dequeue$ perform complex operations and are not
The idea of logical atomicity~\cite[\S7]{jung-slides-2019,iris-15} aims at addressing that difficulty.
When using this concept, instead of using ordinary Hoare triples, we use \emph{logically atomic triples}.
This kind of triple are like Hoare triples: they specify a program fragment, have a precondition and a postcondition.
The core difference being that they allow the opening of invariants around the triple: in a sense, when a function is specified using logically atomic triples, one states that said function behaves just like if it were atomic.
This kind of triples are like Hoare triples: they specify a program fragment, have a precondition and a postcondition.
The core difference is that they allow to open invariants around the triple: in a sense, when a function is specified using logically atomic triples, one states that said function behaves just like if it were atomic.
The definition of logically atomic triples is further discussed in
% TODO : référencer la section
and given with more all details in previous work~\cite[\S7]{jung-slides-2019,iris-15}.
......@@ -175,7 +175,7 @@ The use of such a specification in a concrete example will be detailed in
.
For now, note that it is easy to deduce from this specification a weaker specification such as the one described above where each element of the queue should satisfy a predicate $\Phi$.
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*[]. \isQueueSC\elemList \isep \Phi\,\nthElem{0} \isep \cdots \isep \Phi\,\nthElem{\nbelems-1}}$, which is trivial to initialize when holding $\isQueueSC{[]}$.
Then, for proving the weaker specification of $\enqueue$ and $\dequeue$, one simply has to open the invariant around the logically atomic triple.
Then, for proving the weaker specification of $\enqueue$ and $\dequeue$, one simply has to open the invariant around their logically atomic triples.
% TODO : faut-il en dire plus, ou est-ce compréhensible tel quel?
......@@ -212,9 +212,9 @@ 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).
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.
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 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
......@@ -249,7 +249,7 @@ The queue, however, does not guarantee any happens-before relationship from
a dequeuer to an enqueuer.%
%
\footnote{%
This is not entirely true: the implementation that we show later does create
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.
......
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