Commit 8c88eb47 authored by Glen Mével's avatar Glen Mével
Browse files

ICFP21 paper: more comments about Iris

parent 4057e42d
......@@ -59,8 +59,10 @@ Yet these operations are ``atomic'' in some empirical sense.
The concept of logical atomicity~\cite[\S7]{jacobs2011expressive,jung-slides-2019,iris-15} aims at addressing that difficulty.
To use it, we substitute ordinary Hoare triples with \emph{logically atomic triples}.
Two important reasoning rules for logically atomic triples are given in \fref{fig:latriples}.
Following Iris notations, $\knowInv{}{I}$ is an invariant whose content is the assertion~$I$, and $\later$ is a step-indexing modality, a technicality of Iris that we can ignore in this paper.
Two important reasoning rules for logically atomic triples are given in \fref{fig:latriples}.%
\footnote{%
Following Iris notations, $\knowInv{}{I}$ is an invariant whose content is the assertion~$I$, and $\later$ is a step-indexing modality, a technicality of Iris that we can ignore in this paper.
}
A logically atomic triple is denoted with angle brackets~$\anglebracket{\ldots}$.
Just like an ordinary triple, it specifies a program fragment with a precondition and a postcondition.
In fact, as witnessed by rule \RULE{LAHoare}, one can deduce an ordinary Hoare triple from a logically atomic triple.
......@@ -93,18 +95,6 @@ Because it is atomic, invariants can be opened around that commit point.
\label{fig:latriples}
\end{figure}
% TODO: faire référence aux règles ci-dessus dans le texte.
% => JH
% mentionner qu’un triplet log. atomique implique le triplet usuel ? (1re règle)
% peut-être enlever le binder à cet endroit.
% TODO : expliquer la syntaxe des invariants, dire que \later est une technicité d'Iris
% 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
Using logically atomic triples, the specification can be written as shown
in~\fref{fig:queue:spec:sc}.
It closely resembles that of the sequential setting (\fref{fig:queue:spec:seq}).
......@@ -124,17 +114,28 @@ covering every possible shared state at the commit point.
The last departure from the sequential specification
is that the representation predicate is split into two parts:
a persistent assertion~$\queueInv$ and an exclusive assertion $\isQueueSC\elemList$,
connected by a ghost name~$\gqueue$.
a persistent%
\footnote{%
In Iris terms, \emph{persistent} qualifies an assertion that is duplicable.
Once established, such an assertion holds forever.
}
assertion~$\queueInv$ and an exclusive assertion $\isQueueSC\elemList$,
connected by a ghost name%
\footnote{%
Ghost names in Iris are identifiers for pieces of ghost state. We say more on this in~\sref{sec:queue:proof}.
}%
~$\gqueue$.
That splitting is an artifact of our correctness proof technique,
which we detail in~\sref{sec:queue:proof}.
% TODO : GLEN: 1re fois qu’on parle d’assertions persistantes , définir le terme ici.
%
Note that this does not complicate the use of the queue by the client:
both assertions are produced when creating the queue,
and while the exclusive component can be put in an invariant as before,
the persistent component can be directly duplicated and distributed to all threads.
% TODO : pour après la soumission : expliquer pourquoi QueueInv n'est pas caché dans IsQueue (footnote pour les experts d'Iris : ça rendrait IsQueue non timeless, et on aurait une étape "abort" au début de enqueue/dequeue => pas impossible, mais plus compliqué)
the persistent component can be directly duplicated and distributed to all threads.%
\footnote{%
An Iris expert may want to conceal the queue invariant, $\queueInv$, inside $\isQueueSC\elemList$. However, we need to access this invariant at various places other than the commit point. This is feasible with a more elaborate definition of logically atomic triples than the one given in this paper, so that they support \emph{aborting}~\cite{jung-slides-2019}.
Another drawback is that we would lose the timelessness of the representation predicate.
}
The use of such a specification in a concrete example will be detailed in~\sref{sec:pipeline:proof}.
For now, we illustrate how a weaker specification can be easily deduced from this one.
......
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