Commit 3fa82058 authored by Glen Mével's avatar Glen Mével
Browse files

more consistent naming of figures

parent 9c0889e8
......@@ -79,5 +79,5 @@
\end{array}\]
\Description{Internal invariants of the pipeline.}
\caption{Internal invariants of the pipeline}
\label{fig:pipeline:invariant}
\label{fig:pipeline:inv}
\end{figure}
......@@ -155,5 +155,5 @@
\end{array}\]
\Description{Internal invariant of the bounded queue.}
\caption{Internal invariant of the bounded queue}
\label{fig:queue:invariant}
\label{fig:queue:inv}
\end{figure}
......@@ -27,5 +27,5 @@
\end{mathpar}
\Description{A specification of the ``queue'' data structure in a sequentially consistent model.}
\caption{A specification of the ``queue'' data structure in a sequentially consistent memory model}
\label{fig:queue:specsc}
\label{fig:queue:spec:sc}
%\end{figure}
......@@ -19,5 +19,5 @@
\end{mathpar}
\Description{A specification of the ``queue'' data structure in a sequential setting.}
\caption{A specification of the ``queue'' data structure in a sequential setting}
\label{fig:queue:specseq}
\label{fig:queue:spec:seq}
%\end{figure}
......@@ -108,7 +108,7 @@
\end{array}\]
\Description{A specification of the ``queue'' data structure.}
\caption{A specification of the ``queue'' data structure}
\label{fig:queue:spec}
\label{fig:queue:spec:weak}
\end{figure}
% JH : TODO : serait-ce pertinent de mentionner ici la timelessness et l'objectivité de isQueue et la persistence de queueInv? Cela fait partie de la spec, à mon sens.
% GLEN: la persistance oui, la timelessness c’est peut-être trop technique ?
......
......@@ -11,9 +11,9 @@
We now turn on proving that the implementation shown in \sref{sec:queue:impl}
satisfies the functional specification of \sref{sec:queue:spec:weak} and
\fref{fig:queue:spec}. The internal invariant $\queueInv$, as well as other
\fref{fig:queue:spec:weak}. The internal invariant $\queueInv$, as well as other
assertions that are useful in the proof, are shown in
\fref{fig:queue:invariant}. It features several pieces of ghost state.
\fref{fig:queue:inv}. It features several pieces of ghost state.
Ghost state in Iris takes values from algebraic structures called CMRAs.
For the purpose of this paper, it is enough to think of a CMRA as a set
......@@ -258,7 +258,7 @@ the following join-semilattice structure:
Finally, the ghost variable~$\gmonos$ takes its values from the CMRA
$\finmapm{\Z}{\authm(\statusViewLat)}$ and, with the assertion
$\monoWitness\offset{\pair\status\sview}$ defined as in \fref{fig:queue:invariant},
$\monoWitness\offset{\pair\status\sview}$ defined as in \fref{fig:queue:inv},
we get the following:
%
\begin{mathpar}
......
......@@ -11,7 +11,7 @@ This logic spawned a variety of descendants; in this work, we use
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:specseq}, recalling that $\isQueueSEQ\elemList$ is an
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
to operate on the queue.
......@@ -102,7 +102,7 @@ a queue: the same specification could also describe a stack or a bag.
% 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: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%
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.
......@@ -151,8 +151,8 @@ This linearization point being atomic, it allows the opening of invariants just
% 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:specsc}.
It closely resembles that of the sequential setting (\fref{fig:queue:specseq}).
in~\fref{fig:queue:spec:sc}.
It closely resembles that of the sequential setting (\fref{fig:queue:spec:seq}).
The first difference that can be seen is the use of angle brackets $\anglebracket{\ldots}$ denoting logically atomic triples instead of curly brackets $\curlybracket{\ldots}$ for ordinary Hoare triples.
Another difference is the presence of embedded universal quantifiers ($\lahoarebinder{\nbelems, \elemList*[]}$) in the syntax of logically atomic triples.
......
......@@ -19,7 +19,7 @@ resources that may alias parts of our queue. In particular, the representation
predicate cannot be duplicated; we say that it is \emph{exclusive}.
The operations of the queue admit a simple sequential specification which is
presented in~\fref{fig:queue:specseq}. We use the standard Hoare
presented in~\fref{fig:queue:spec:seq}. We use the standard Hoare
triple notation, with a partial correctness meaning.
The asterisk~$(\ast)$ is the separating conjunction.
......
......@@ -9,12 +9,12 @@ In this section, we lift this restriction, and propose a more precise specificat
We will use the separation logic \hlog{}~\citecosmo:
this framework has been designed on top of Iris in order to provide a powerful proof framework for the weak memory model of \mocaml{}.
Because \hlog{} is based on Iris, logically atomic triples can also be defined in this logic.
In fact, the specification shown in~\fref{fig:queue:specsc} still applies.
In fact, the specification shown in~\fref{fig:queue:spec:sc} still applies.
However, as such, this specification is of little value in a weakly consistent context.
Indeed, as we explained in~\sref{sec:queue:spec:sc}, that specification is designed so that the representation predicate $\isQueueSC\elemList$ should be shared among threads by using an invariant.
But, in \hlog{}, invariants are restricted to a special class of assertions, called \emph{objective} assertions.
As a result, the specification shown in~\fref{fig:queue:specsc} is useful in a weakly consistent context only if the representation predicate $\isQueueSC\elemList$ is objective.
As a result, the specification shown in~\fref{fig:queue:spec:sc} is useful in a weakly consistent context only if the representation predicate $\isQueueSC\elemList$ is objective.
% FP voilà les grandes lignes de ce que je dirais sur la linéarisabilité:
......@@ -108,8 +108,8 @@ retains an interesting behavior that suffices for many use cases.
% Ce que je propose (mais je ne sais pas si c'est standard) : dire que /linéarisable/, c'est qu'il existe un ordre total sur les accès, et que ces accès respectent cet ordre (i.e., agissent uniquement sur l'état courant dans cet ordre). Donc notre queue est linéarisable. Par contre, elle n'est pas /séquentiellement consistente/, puisqu'elle ne garantit pas tout ce qu'elle pourrait en terme d'happens-before
% TODO : comprendre/prendre une décision sur le mot linearizable
Interestingly, \hlog{} is able to express this subtle difference between the behavior of our library and that of lock-based implementation: the full specification under weak memory is shown in~\fref{fig:queue:spec}.
It extends the previous specification (\fref{fig:queue:specsc}) with views, capturing the mentioned happens-before relationships as follows.
Interestingly, \hlog{} is able to express this subtle difference between the behavior of our library and that of lock-based implementation: the full specification under weak memory is shown in~\fref{fig:queue:spec:weak}.
It extends the previous specification (\fref{fig:queue:spec:sc}) with views, capturing the mentioned happens-before relationships as follows.
\begin{enumerate}%
......
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