From 6e00aa3402b729fb58e5dd0c95d18156ca70c3a2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 7 Dec 2016 18:07:57 +0100
Subject: [PATCH] docs: finalize non-atomic invariants
---
docs/derived.tex | 49 +++++++++++++++++++++---------------------
docs/iris.sty | 13 +++++------
docs/program-logic.tex | 18 ++++++++--------
3 files changed, 40 insertions(+), 40 deletions(-)
diff --git a/docs/derived.tex b/docs/derived.tex
index 7be98440a..55cea6798 100644
--- a/docs/derived.tex
+++ b/docs/derived.tex
@@ -1,63 +1,62 @@
\section{Derived constructions}
-\subsection{Non-atomic invariants}
+\subsection{Non-atomic (``thread-local'') invariants}
Sometimes it is necessary to maintain invariants that we need to open non-atomically.
-Clearly, for this mechanism to be sound we need something that prevents us from opening the same invariant twice.
-Access to these \emph{non-atomic invariants} is thus guarded by tokens that take the role that masks play for ``normal'', atomic invariants.
-
-One way to think about them is as ``thread-local invariants''.
-For every thread, we have a set of \emph{tokens}.
-By giving up a token, you can obtain the invariant, and vice versa.
-Such invariants can only be opened by their respective thread, and as a consequence they can be kept open around any sequence of expressions (\ie there is no restriction to atomic expressions).
-To tie the threads and the tokens together, every thread is assigned a \emph{thread ID}.
-Note that these thread IDs are completely fictional, there is no operational aspect to them.
-In principle, the tokens could move between threads; that's not an issue at all.
+Clearly, for this mechanism to be sound we need something that prevents us from opening the same invariant twice, something like the masks that avoid reentrancy on the ``normal'', atomic invariants.
+The idea is to use tokens\footnote{Very much like the tokens that are used to encode ``normal'', atomic invariants} that guard access to non-atomic invariants.
+Having the token $\NaTokE\pid\mask$ indicates that we can open all invariants in $\mask$.
+The $\pid$ here is the name of the \emph{invariant pool}.
+This mechanism allows us to have multiple, independent pools of invariants that all have their own namespaces.
+
+One way to think about non-atomic invariants is as ``thread-local invariants'',
+where every pool is a thread.
+Every thread thus has its own, independent set of invariants.
+Every thread threads through all the tokens for its own pool, so that each invariant can only be opened in the thread it belongs to.
+As a consequence, they can be kept open around any sequence of expressions (\ie there is no restriction to atomic expressions) -- after all, there cannot be any races with other threads.
Concretely, this is the monoid structure we need:
\begin{align*}
-\textdom{TId} \eqdef{}& \nat \\
-\textmon{TTok} \eqdef{}& \textdom{TId} \fpfn \pset{\textdom{InvName}}\\
-\textmon{TDis} \eqdef{}& \textdom{TId} \fpfn \finpset{\textdom{InvName}}
+\textdom{PId} \eqdef{}& \GName \\
+\textmon{NaTok} \eqdef{}& \finpset{\InvName} \times \pset{\InvName}
\end{align*}
-For every thread, there is a set of tokens designating which invariants are \emph{enabled} (closed).
+For every pool, there is a set of tokens designating which invariants are \emph{enabled} (closed).
This corresponds to the mask of ``normal'' invariants.
We re-use the structure given by namespaces for non-atomic invariants.
Furthermore, there is a \emph{finite} set of invariants that is \emph{disabled} (open).
-We assume a global instance $\Gttok$ of \textmon{TTok}, and an instance $\Gtdis$ of $\textmon{TDis}$.
-Then we can define some sugar for owning tokens:
+Owning tokens is defined as follows:
\begin{align*}
-\TTokE\tid\mask \eqdef{}& \ownGhost{\Gttok}{ \mapsingleton\tid\mask : \textmon{TTok} } \\
-\TTok\tid \eqdef{}& \TTokE\tid\top
+\NaTokE\pid\mask \eqdef{}& \ownGhost{\pid}{ (\emptyset, \mask) } \\
+\NaTok\pid \eqdef{}& \NaTokE\pid\top
\end{align*}
Next, we define non-atomic invariants.
To simplify this construction,we piggy-back into ``normal'' invariants.
\begin{align*}
- \NaInv\tid\namesp\prop \eqdef{}& \Exists \iname\in\namesp. \knowInv\namesp{\prop * \ownGhost\Gtdis{\set{\iname}} \lor \TTokE\tid{\set{\iname}}}
+ \NaInv\pid\namesp\prop \eqdef{}& \Exists \iname\in\namesp. \knowInv\namesp{\prop * \ownGhost\pid{(\set{\iname},\emptyset)} \lor \NaTokE\pid{\set{\iname}}}
\end{align*}
We easily obtain:
\begin{mathpar}
\axiom
- {\TRUE \vs[\bot] \Exists\tid. \TTok\tid}
+ {\TRUE \vs[\bot] \Exists\pid. \NaTok\pid}
\axiom
- {\TTokE\tid{\mask_1 \uplus \mask_2} \Lra \TTokE\tid{\mask_1} * \TTokE\tid{\mask_2}}
+ {\NaTokE\pid{\mask_1 \uplus \mask_2} \Lra \NaTokE\pid{\mask_1} * \NaTokE\pid{\mask_2}}
\axiom
- {\later\prop \vs[\namesp] \always\NaInv\tid\namesp\prop}
+ {\later\prop \vs[\namesp] \always\NaInv\pid\namesp\prop}
\axiom
- {\NaInv\tid\namesp\prop \proves \Acc[\namesp]{\TTokE\tid\namesp}{\later\prop}}
+ {\NaInv\pid\namesp\prop \proves \Acc[\namesp]{\NaTokE\pid\namesp}{\later\prop}}
\end{mathpar}
from which we can derive
\begin{mathpar}
\infer
{\namesp \subseteq \mask}
- {\NaInv\tid\namesp\prop \proves \Acc[\namesp]{\TTokE\tid\mask}{\later\prop * \TTokE\tid{\mask \setminus \namesp}}}
+ {\NaInv\pid\namesp\prop \proves \Acc[\namesp]{\NaTokE\pid\mask}{\later\prop * \NaTokE\pid{\mask \setminus \namesp}}}
\end{mathpar}
diff --git a/docs/iris.sty b/docs/iris.sty
index 5781d31e7..8578e2e6a 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -339,6 +339,9 @@
\newcommand{\physatomic}[1]{\textlog{atomic}($#1$)}
\newcommand{\infinite}{\textlog{infinite}}
+\newcommand\InvName{\textdom{InvName}}
+\newcommand\GName{\textdom{GName}}
+
\newcommand{\Prop}{\textlog{Prop}}
\newcommand{\Pred}{\textlog{Pred}}
@@ -427,13 +430,11 @@
\newcommand{\mapstoprop}{\mathrel{\kern-0.5ex\tikz[baseline=(m)]{\node at (0,0) (m){}; \draw[line cap=round] (0,0.16) -- (0,-0.004);}\kern-1.5ex\Ra}}
% Non-atomic invariants
-\newcommand*\Gttok{\gname_\textrm{TTok}}
-\newcommand*\Gtdis{\gname_\textrm{TDis}}
-\newcommand*\tid{t}
-\newcommand\NaInv[3]{\textlog{NAInv}^{#1.#2}(#3)}
+\newcommand*\pid{p}
+\newcommand\NaInv[3]{\textlog{NaInv}^{#1.#2}(#3)}
-\newcommand*\TTok[1]{{[}\textrm{T}:#1{]}}
-\newcommand*\TTokE[2]{{[}\textrm{T}:#1.#2{]}}
+\newcommand*\NaTok[1]{{[}\textrm{NaInv}:#1{]}}
+\newcommand*\NaTokE[2]{{[}\textrm{NaInv}:#1.#2{]}}
\endinput
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 997215f1b..152313f72 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -27,8 +27,8 @@ To instantiate the program logic, the user picks a family of locally contractive
From this, we construct the bifunctor defining the overall resources as follows:
\begin{align*}
- \mathcal G \eqdef{}& \nat \\
- \textdom{ResF}(\ofe^\op, \ofe) \eqdef{}& \prod_{i \in \mathcal I} \mathcal G \fpfn \iFunc_i(\ofe^\op, \ofe)
+ \GName \eqdef{}& \nat \\
+ \textdom{ResF}(\ofe^\op, \ofe) \eqdef{}& \prod_{i \in \mathcal I} \GName \fpfn \iFunc_i(\ofe^\op, \ofe)
\end{align*}
We will motivate both the use of a product and the finite partial function below.
$\textdom{ResF}(\ofe^\op, \ofe)$ is a CMRA by lifting the individual CMRAs pointwise, and it has a unit (using the empty finite partial functions).
@@ -112,10 +112,10 @@ To this end, we use tokens that manage which invariants are currently enabled.
We assume to have the following four CMRAs available:
\begin{align*}
- \mathcal I \eqdef{}& \nat \\
- \textmon{Inv} \eqdef{}& \authm(\mathcal I \fpfn \agm(\latert \iPreProp)) \\
- \textmon{En} \eqdef{}& \pset{\mathcal I} \\
- \textmon{Dis} \eqdef{}& \finpset{\mathcal I} \\
+ \InvName \eqdef{}& \nat \\
+ \textmon{Inv} \eqdef{}& \authm(\InvName \fpfn \agm(\latert \iPreProp)) \\
+ \textmon{En} \eqdef{}& \pset{\InvName} \\
+ \textmon{Dis} \eqdef{}& \finpset{\InvName} \\
\textmon{State} \eqdef{}& \authm(\maybe{\exm(\State)})
\end{align*}
The last two are the tokens used for managing invariants, $\textmon{Inv}$ is the monoid used to manage the invariants themselves.
@@ -126,7 +126,7 @@ We assume that at the beginning of the verification, instances named $\gname_{\t
\paragraph{World Satisfaction.}
We can now define the assertion $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:
\begin{align*}
- W \eqdef{}& \Exists I : \mathcal I \fpfn \Prop.
+ W \eqdef{}& \Exists I : \InvName \fpfn \Prop.
\begin{array}[t]{@{} l}
\ownGhost{\gname_{\textmon{Inv}}}{\authfull
\mapComp {\iname}
@@ -471,8 +471,8 @@ We use the notation $\namesp.\iname$ for the namespace $[\iname] \dplus \namesp$
The elements of a namespaces are \emph{structured invariant names} (think: Java fully qualified class name).
They, too, are lists of $\nat$, the same type as namespaces.
-In order to connect this up to the definitions of \Sref{sec:invariants}, we need a way to map structued invariant names to $\mathcal I$, the type of ``plain'' invariant names.
-Any injective mapping $\textlog{namesp\_inj}$ will do; and such a mapping has to exist because $\List(\nat)$ is countable and $\mathcal I$ is infinite.
+In order to connect this up to the definitions of \Sref{sec:invariants}, we need a way to map structued invariant names to $\InvName$, the type of ``plain'' invariant names.
+Any injective mapping $\textlog{namesp\_inj}$ will do; and such a mapping has to exist because $\List(\nat)$ is countable and $\InvName$ is infinite.
Whenever needed, we (usually implicitly) coerce $\namesp$ to its encoded suffix-closure, \ie to the set of encoded structured invariant names contained in the namespace: \[\namecl\namesp \eqdef \setComp{\iname}{\Exists \namesp'. \iname = \textlog{namesp\_inj}(\namesp' \dplus \namesp)}\]
We will overload the notation for invariant assertions for using namespaces instead of names:
--
GitLab