From d48b2c6a758183bc49554ce0629e5367e7badfb6 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 11 Dec 2017 11:30:26 +0100 Subject: [PATCH] cancellable invariants --- docs/constructions.tex | 2 +- docs/derived.tex | 38 ++++++++++++++++++++++++++++++++++---- docs/iris.sty | 5 +++++ 3 files changed, 40 insertions(+), 5 deletions(-) diff --git a/docs/constructions.tex b/docs/constructions.tex index 5a1373f4..8987f873 100644 --- a/docs/constructions.tex +++ b/docs/constructions.tex @@ -202,7 +202,7 @@ We define an RA structure on the rational numbers in $(0, 1]$ as follows: \begin{align*} \fracm \eqdef{}& \fracinj(\mathbb{Q} \cap (0, 1]) \mid \mundef \\ \mvalFull(\melt) \eqdef{}& \melt \neq \mundef \\ - \fracinj(x) \mtimes \fracinj(y) \eqdef{}& \fracinj(x + y) \quad \text{if $x + y \leq 1$} \\ + \fracinj(q_1) \mtimes \fracinj(q_2) \eqdef{}& \fracinj(q_1 + q_2) \quad \text{if $q_1 + q_2 \leq 1$} \\ \mcore{\fracinj(x)} \eqdef{}& \bot \\ \mcore{\mundef} \eqdef{}& \mundef \end{align*} diff --git a/docs/derived.tex b/docs/derived.tex index 938de82b..948c5333 100644 --- a/docs/derived.tex +++ b/docs/derived.tex @@ -1,5 +1,35 @@ \section{Derived Constructions} +\subsection{Cancellable Invariants} + +Iris invariants as described in \Sref{sec:invariants} are persistent---once established, they hold forever. +However, based on them, it is possible to \emph{encode} a form of invariants that can be cancelled'' again. + +First, we need some ghost state: +\begin{align*} + \textmon{CInvTok} \eqdef{}& \fracm +\end{align*} + +Now we define: +\begin{align*} + \CInvTok{\gname}{q} \eqdef{}& \ownGhost\gname{q} \\ + \CInv{\gname}{\namesp}{\prop} \eqdef{}& \knowInv\namesp{\prop \lor \ownGhost\gname{1}} +\end{align*} + +It is then straight-forward to prove: +\begin{mathpar} + \inferH{CInv-new}{} + {\later\prop \vs[\bot] \Exists \gname. \CInvTok\gname{1} * \always\CInv\gname\namesp\prop} + + \inferH{CInv-acc}{} + {\CInv\gname\namesp\prop \proves \Acc[\namesp][\emptyset]{\CInvTok\gname{q}}{\later\prop}} + + \inferH{CInv-cancel}{} + {\CInv\gname\namesp\prop \proves \CInvTok\gname{1} \vs[\namesp] \later\prop} +\end{mathpar} + +Cancellable invariants are useful, for example, when reasoning about data structures that will be deallocated: Every reference to the data structure comes with a fraction of the token, and when all fractions have been gathered, \ruleref{CInv-cancel} is used to cancel the invariant, after which the data structure can be deallocated. + \subsection{Non-atomic (Thread-Local'') Invariants} Sometimes it is necessary to maintain invariants that we need to open non-atomically. @@ -40,16 +70,16 @@ To simplify this construction,we piggy-back into normal'' invariants. We easily obtain: \begin{mathpar} - \axiom + \axiomH{NAInv-new-pool} {\TRUE \vs[\bot] \Exists\pid. \NaTok\pid} - \axiom + \axiomH{NAInv-tok-split} {\NaTokE\pid{\mask_1 \uplus \mask_2} \Lra \NaTokE\pid{\mask_1} * \NaTokE\pid{\mask_2}} - \axiom + \axiomH{NAInv-new-inv} {\later\prop \vs[\namesp] \always\NaInv\pid\namesp\prop} - \axiom + \axiomH{NAInv-acc} {\NaInv\pid\namesp\prop \proves \Acc[\namesp]{\NaTokE\pid\namesp}{\later\prop}} \end{mathpar} from which we can derive diff --git a/docs/iris.sty b/docs/iris.sty index c0006138..aec6f526 100644 --- a/docs/iris.sty +++ b/docs/iris.sty @@ -409,6 +409,7 @@ % Fraction \newcommand{\fracm}{\ensuremath{\textmon{Frac}}} +\newcommand{\fracinj}{\textlog{frac}} % Exclusive \newcommand{\exm}{\ensuremath{\textmon{Ex}}} @@ -452,6 +453,10 @@ %% 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}} +%% Cancellable invariants +\newcommand\CInv[3]{\textlog{CInv}^{#1,#2}(#3)} +\newcommand*\CInvTok[2]{{[}\textrm{CInv}:#1{]}_{#2}} + %% Non-atomic invariants \newcommand*\pid{p} \newcommand\NaInv[3]{\textlog{NaInv}^{#1.#2}(#3)} -- GitLab