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

Nitpicks in spec.

parent 081e5117
...@@ -50,7 +50,7 @@ operation on the shared state, reestablish the invariant, and finally close it. ...@@ -50,7 +50,7 @@ operation on the shared state, reestablish the invariant, and finally close it.
However, to ensure soundness in the face of concurrency, the use of invariants However, to ensure soundness in the face of concurrency, the use of invariants
in Iris obeys a strict constraint: they can remain open during at most a single in Iris obeys a strict constraint: they can remain open during at most a single
step of execution. Unfortunately, $\enqueue$ and $\dequeue$ are complex step of execution. Unfortunately, $\enqueue$ and $\dequeue$ are complex
operations which, a~priori, take more than one step of execution. Hence a client operations which, \emph{a~priori}, take more than one step of execution. Hence a client
would be unable to open their invariant around the triples shown would be unable to open their invariant around the triples shown
in~\fref{fig:queue:spec:seq}. in~\fref{fig:queue:spec:seq}.
Yet these operations are ``atomic'' in some empirical sense. Yet these operations are ``atomic'' in some empirical sense.
...@@ -58,7 +58,7 @@ Yet these operations are ``atomic'' in some empirical sense. ...@@ -58,7 +58,7 @@ Yet these operations are ``atomic'' in some empirical sense.
The idea of logical atomicity~\cite[\S7]{jung-slides-2019,iris-15} aims at addressing that difficulty. 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}. When using this concept, instead of using ordinary Hoare triples, we use \emph{logically atomic triples}.
This kind of triples are like Hoare triples: they specify a program fragment, have a precondition and a postcondition. 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 core difference is that they allow opening 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 The definition of logically atomic triples is further discussed in
% TODO : référencer la section % TODO : référencer la section
and given with detail in previous work~\cite[\S7]{jung-slides-2019,iris-15}. and given with detail in previous work~\cite[\S7]{jung-slides-2019,iris-15}.
...@@ -159,7 +159,7 @@ where the boxed assertion is an Iris invariant: ...@@ -159,7 +159,7 @@ where the boxed assertion is an Iris invariant:
\[ \[
\isQueuePers\Phi \isQueuePers\Phi
\;\eqdef\; \;\eqdef\;
\ISep{% \Exists\gqueue. \ISep{%
\queueInv \queueInv
\\ \knowInv{}{\Exists \nbelems, \elemList*[]. \isQueueSC\elemList \isep \Phi\,\nthElem{0} \isep \cdots \isep \Phi\,\nthElem{\nbelems-1}} \\ \knowInv{}{\Exists \nbelems, \elemList*[]. \isQueueSC\elemList \isep \Phi\,\nthElem{0} \isep \cdots \isep \Phi\,\nthElem{\nbelems-1}}
} }
......
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