diff --git a/docs/derived.tex b/docs/derived.tex index 2802c54173432c05c8e9e58424a1fee08b5938eb..7be98440a50215057f190bceed0305ecee22ed5b 100644 --- a/docs/derived.tex +++ b/docs/derived.tex @@ -1,4 +1,65 @@ -%\section{Derived constructions} +\section{Derived constructions} + +\subsection{Non-atomic 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. + +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}} +\end{align*} +For every thread, 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: +\begin{align*} +\TTokE\tid\mask \eqdef{}& \ownGhost{\Gttok}{ \mapsingleton\tid\mask : \textmon{TTok} } \\ +\TTok\tid \eqdef{}& \TTokE\tid\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}}} +\end{align*} + + +We easily obtain: +\begin{mathpar} + \axiom + {\TRUE \vs[\bot] \Exists\tid. \TTok\tid} + + \axiom + {\TTokE\tid{\mask_1 \uplus \mask_2} \Lra \TTokE\tid{\mask_1} * \TTokE\tid{\mask_2}} + + \axiom + {\later\prop \vs[\namesp] \always\NaInv\tid\namesp\prop} + + \axiom + {\NaInv\tid\namesp\prop \proves \Acc[\namesp]{\TTokE\tid\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}}} +\end{mathpar} + % TODO: These need syncing with Coq % \subsection{STSs with interpretation}\label{sec:stsinterp} diff --git a/docs/iris.sty b/docs/iris.sty index 136cc677a69699e009957d1125da0616681685dd..5781d31e72cd3b31cbeabaed4205690f7fc3741a 100644 --- a/docs/iris.sty +++ b/docs/iris.sty @@ -426,5 +426,14 @@ %% Stored Propositions \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*\TTok[1]{{[}\textrm{T}:#1{]}} +\newcommand*\TTokE[2]{{[}\textrm{T}:#1.#2{]}} + \endinput