Commit 95b581b0 authored by Glen Mével's avatar Glen Mével
Browse files

move the weak persistent spec as an example, after the general LA spec

parent da83549c
......@@ -13,11 +13,11 @@ Iris~\cite{iris}, a modular framework for building separation logics.
In a derivative of \CSL, we may retain the exact same specification as is presented
in~\fref{fig:queue:spec:seq}, recalling that $\isQueueSEQ\elemList$ is an
exclusive assertion:
a thread that has this assertion could safely assume to be the only one allowed
a thread that has this assertion can safely assume to be the only one allowed
to operate on the queue.
%
The assertion would be transferable between threads via some means of
synchronization: for instance, we may use a lock to guard all operations on the
A client application can transfer this assertion between threads via some means of
synchronization: for instance, it may use a lock to guard all operations on the
shared queue, following the approach of \CSL.
%
However this coarse grain concurrency has a run-time penalty,
......@@ -29,87 +29,31 @@ to prove the correctness of a MRMW~queue implementation, which should thus
ensure, by itself, thread safety.
%
Hence we can achieve finer-grain concurrency, where operating on a queue does
not require its exclusive ownership. In this context, it is important that the
ownership of the queue can be shared among several threads.
One option to address this constraint in our specification is to provide the client
with a persistent assertion, instead of an exclusive representation predicate.
A challenge is then to describe the public state of the queue tightly enough so
that any client application can reason about it.
It is impossible for a thread to know exactly the current list of items, as any
thread can change it any moment.
For example, a possible but rather weak specification would only guarantee that
all of the elements stored in the queue satisfy some predicate~$\Phi$. This is
not satisfactory in the general case, as we lose most structural properties of
a queue: the same specification could also describe a stack or a bag.
not require its exclusive ownership.
In this context, another option is for the client to share this ownership among
several threads, logically. In an Iris-like logic, one would typically place the
exclusive ownership in an \emph{invariant}.
%---alongside the properties about the public state which are needed by the particular application.
An invariant is an assertion which is agreed upon by all threads, and is owned
by anyone; it remains true forever.
%
\begin{mathpar}
As the public state of the queue---the list $\elemList$ of currently stored
items---would only be known from that invariant, the client would also express
in there the properties about this state that their particular application
needs.
%
%\infer{}{%
% \persistent{\isQueuePers\Phi}
%}
%
\infer{%
\isQueuePers\Phi
}{%
\hoare
{\Phi\,\elem}
{\enqueue~\queue~\elem}
{\Lam \Unit. \TRUE}
}
\infer{%
\isQueuePers\Phi
}{%
\hoare
{\TRUE}
{\dequeue~\queue}
{\Lam \elem. \Phi\,\elem}
}
Then, when one of the threads needs to access the shared resource, it can
\emph{open} the invariant, get the assertions it contains, perform the desired
operation on the shared state, reestablish the invariant, and finally close it.
%
\end{mathpar}
% GLEN: j’ai reformulé les paragraphes présentant ces deux options, j’espère ne
% pas les avoir dénaturés. Si j’ai bien compris ce dont tu voulais parler,
% l’invariant dont on parle dans la 2e option n’est pas l’invariant interne de
% la structure de données (\queueInv), donc j’insiste ici sur le fait qu’on
% parle du côté client.
% Il me semble que dans cette présentation, la 2e option, avant qu’on parle de
% remplacer les triplets normaux par des triplets logiquement atomiques,
% consiste à garder la spec séquentielle telle quelle; c’est un peu étrange
% comme progression du discours, on a déjà dit au début de la sous-section qu’on
% pouvait le faire mais que ça n’était pas utilisable tel quel (il faudrait par
% exemple protéger la structure de données par un verrou) et qu’on voulait faire
% mieux. Du coup, la 1re option vient un peu comme une digression.
% Parler de la 1re option est-il nécessaire ?
% On pourrait dire quelque chose comme:
% la queue est représentée par une ressource exclusive (qui confère sa
% possession). Pour autoriser plusieurs participants, soit on transfère la
% ressource d’un thread à l’autre via des synchros (physiques, telles qu’un
% verrou), soit on la partage entre tous les threads via un invariant
% (opération purement logique).
% La 2e méthode n’est pas toujours applicable car, dans un cadre concurrent,
% un invariant ne peut être ouvert qu’autour d’un fragment de programme
% "atomique" dans un certain sens. Pour les invariants standards d’Iris, la
% définition des programmes "atomiques" est trop restreinte (syntaxique
% / opérationnelle) et ne s’applique pas ici.
% Pourtant notre queue est thread-safe, enqueue et dequeue réalisent une
% certaine forme empirique d’atomicité (de façon comparable à une section
% 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.
% => TODO : déplacer ceci en tant qu'exemple à la fin de la spec SC
Another option is to keep exposing a specification akin to that of~\fref{fig:queue:spec:seq}, 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
: one would typically place the exclusive ownership of the queue in an \emph{invariant}.
An invariant is an assertion which is agreed upon by all threads, and is owned by anyone; it remains true forever.
In this invariant, the client would also express which properties about the public state their particular application needs.
Then, when one of the threads needs to access the shared resource, it can \emph{open} the invariant, perform the shared state operations it needs, reestablish the invariant, and finally close it.
However, in order to be sound in the face of concurrency, the use of invariants in Iris needs to obey a strict constraint: they can remain open during at most a single step of execution.
Unfortunately, $\enqueue$ and $\dequeue$ perform complex operations that take more than one step of execution.
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
step of execution. Unfortunately, $\enqueue$ and $\dequeue$ are complex
operations which, a~priori, take more than one step of execution. Hence a client
would be unable to open their invariant around the triples shown
in~\fref{fig:queue:spec:seq}.
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.
When using this concept, instead of using ordinary Hoare triples, we use \emph{logically atomic triples}.
......@@ -165,15 +109,63 @@ That splitting is an artifact of our correctness proof techniques which we detai
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$ is persistent and therefore freely duplicated and shared among threads.
% TODO : pour après la soumission : expliquer pourquoi QueueInv n'est pas caché dans isQueeu (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 use of such a specification in a concrete example will be detailed in \sref{sec:pipeline:proof}.
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, one would simply define $\isQueuePers\Phi$ as the conjuction of $\queueInv$ and of the following Iris invariant:
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.
% ------------------------------------------------------------------------------
\subsubsection{A Persistent Specification}
If it were not for logical atomicity, and we still wanted to share the ownership
of the queue, we would have little choice left than renouncing to an exclusive
representation predicate. Only a persistent assertion would be provided, because
the description of the public state has to be stable in the face of interference
by other threads. The resulting specification would be much weaker.
%
For example, we may merely specify that all of the elements stored in the queue
satisfy some predicate~$\Phi$. In doing so, we lose most structural properties
of a queue: the same specification could also describe a stack or a bag.
%
\begin{mathpar}
%
\infer{~}{%
\persistent{\isQueuePers\Phi}
}
\quad
\infer{%
\isQueuePers\Phi
}{%
\hoare
{\Phi\,\elem}
{\enqueue~\queue~\elem}
{\Lam \Unit. \TRUE}
}
\quad
\infer{%
\isQueuePers\Phi
}{%
\hoare
{\TRUE}
{\dequeue~\queue}
{\Lam \elem. \Phi\,\elem}
}
%
\end{mathpar}
To derive these Hoare triples from the ones of~\fref{fig:queue:spec:sc},
one simply defines the persistent assertion as follows,
where the boxed assertion is an Iris invariant:
%
\[
\knowInv{}{\Exists \nbelems, \elemList*[]. \isQueueSC\elemList \isep \Phi\,\nthElem{0} \isep \cdots \isep \Phi\,\nthElem{\nbelems-1}}
\isQueuePers\Phi
\;\eqdef\;
\ISep{%
\queueInv
\\ \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{[]}$.
Then, for proving the weaker specification of $\enqueue$ and $\dequeue$, one would open the invariant around the associated logically atomic triples.
%% 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
%% $
This assertion 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.
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