docs: finalize non-atomic invariants

docs/derived.tex

 \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}
 
 

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
 

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: