diff --git a/docs/derived.tex b/docs/derived.tex index 7be98440a50215057f190bceed0305ecee22ed5b..55cea67985a0a76b63de6dac57461b2101a8f978 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 5781d31e72cd3b31cbeabaed4205690f7fc3741a..8578e2e6ac649222d599263dea0952726b8b93a1 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 997215f1b968dea78740b6d981524769997b9ded..152313f72e686a12cc5bc962d916f56c88e51b94 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: