From 87ae6771cf2ed5a9ad44f5594f67dfc8d5bd2886 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 6 Oct 2016 16:40:12 +0200
Subject: [PATCH] docs: define the program logic
---
docs/base-logic.tex | 2 +-
docs/derived.tex | 8 ++--
docs/iris.sty | 12 +++--
docs/program-logic.tex | 99 +++++++++++++++++++++++++-----------------
4 files changed, 73 insertions(+), 48 deletions(-)
diff --git a/docs/base-logic.tex b/docs/base-logic.tex
index af5689c6d..26bebe1de 100644
--- a/docs/base-logic.tex
+++ b/docs/base-logic.tex
@@ -372,7 +372,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
\end{mathpar}
-\paragraph{Laws for the update modality.}
+\paragraph{Laws for the resource update modality.}
\begin{mathpar}
\infer[upd-mono]
{\prop \proves \propB}
diff --git a/docs/derived.tex b/docs/derived.tex
index ef9c4d99f..744919b2c 100644
--- a/docs/derived.tex
+++ b/docs/derived.tex
@@ -46,8 +46,9 @@ We collect here some important and frequently used derived proof rules.
An assertion $\prop$ is \emph{persistent} if $\prop \proves \always\prop$.
\end{defn}
+\ralf{Needs update.}
Of course, $\always\prop$ is persistent for any $\prop$.
-Furthermore, by the proof rules given in \Sref{sec:proof-rules}, $t = t'$ as well as $\ownGGhost{\mcore\melt}$, $\mval(\melt)$ and $\knowInv\iname\prop$ are persistent.
+Furthermore, by the proof rules given in \Sref{sec:proof-rules}, $t = t'$ as well as $\ownGhost\gname{\mcore\melt}$, $\mval(\melt)$ and $\knowInv\iname\prop$ are persistent.
Persistence is preserved by conjunction, disjunction, separating conjunction as well as universal and existential quantification.
In our proofs, we will implicitly add and remove $\always$ from persistent assertions as necessary, and generally treat them like normal, non-linear assumptions.
@@ -98,7 +99,7 @@ The following rules can be derived for view shifts.
\begin{mathparpagebreakable}
\inferH{vs-update}
{\melt \mupd \meltsB}
- {\ownGGhost{\melt} \vs \exists \meltB \in \meltsB.\; \ownGGhost{\meltB}}
+ {\ownGhost\gname{\melt} \vs \exists \meltB \in \meltsB.\; \ownGhost\gname{\meltB}}
\and
\inferH{vs-trans}
{\prop \vs[\mask_1][\mask_2] \propB \and \propB \vs[\mask_2][\mask_3] \propC \and \mask_2 \subseteq \mask_1 \cup \mask_3}
@@ -240,10 +241,11 @@ We can derive some specialized forms of the lifting axioms for the operational s
\subsection{Global functor and ghost ownership}
+\ralf{Should be entirely redundant.}
Hereinafter we assume the global CMRA functor (served up as a parameter to Iris) is obtained from a family of functors $(\iFunc_i)_{i \in I}$ for some finite $I$ by picking
\[ \iFunc(\cofe) \eqdef \prod_{i \in I} \textlog{GhName} \fpfn \iFunc_i(\cofe) \]
We don't care so much about what concretely $\textlog{GhName}$ is, as long as it is countable and infinite.
-With $M_i \eqdef \iFunc_i(\iProp)$, we write $\ownGhost{\gname}{\melt : M_i}$ (or just $\ownGhost{\gname}{\melt}$ if $M_i$ is clear from the context) for $\ownGGhost{[i \mapsto [\gname \mapsto \melt]]}$.
+With $M_i \eqdef \iFunc_i(\iProp)$, we write $\ownGhost{\gname}{\melt : M_i}$ (or just $\ownGhost{\gname}{\melt}$ if $M_i$ is clear from the context) for $\ownM{[i \mapsto [\gname \mapsto \melt]]}$.
In other words, $\ownGhost{\gname}{\melt : M_i}$ asserts that in the current state of monoid $M_i$, the ``ghost location'' $\gname$ is allocated and we own piece $\melt$.
From~\ruleref{pvs-update}, \ruleref{vs-update} and the frame-preserving updates in~\Sref{sec:prodm} and~\Sref{sec:fpfnm}, we have the following derived rules.
diff --git a/docs/iris.sty b/docs/iris.sty
index ac183873e..460e4deaa 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -228,9 +228,8 @@
}
\newcommand*{\knowInv}[2]{\boxedassert{#2}[#1]}
\newcommand*{\ownGhost}[2]{\boxedassert[densely dashed]{#2}[#1]}
-\newcommand*{\ownGGhost}[1]{\boxedassert[densely dashed]{#1}}
-\newcommand{\ownM}[1]{\textlog{Own}(#1)}
-\newcommand{\ownPhys}[1]{\textlog{Phy}(#1)}
+\newcommand*{\ownM}[1]{\textlog{Own}(#1)}
+\newcommand*{\ownPhys}[1]{\textlog{Phy}(#1)}
%% View Shifts
\NewDocumentCommand \vsGen {O{} m O{}}%
@@ -249,6 +248,13 @@
{\vsGen[#1]{\Lleftarrow\!\!\!\Rrightarrow}[#2]}
\NewDocumentCommand \pvs {O{} O{}} {\mathord{\vsGen[#1]{{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}[#2]\kern0.2ex}}
+\newcommand\vsWand{\kern0.1ex\tikz[baseline=(base),line width=0.375pt]{%
+ \draw (0, 0) -- (0.4, 0); \draw (0, -0.075) -- (0.28, -0.075); \draw (0, 0.075) -- (0.28, 0.075);
+ \node at (0.4, -0.235) (ast) {$\smash{\scaleto{\ast}{1.2em}}$};
+ \node at (0.4, -0.095) (base) {};
+}{\vphantom{\Rrightarrow}}\kern-1.2ex}
+\NewDocumentCommand \vsW {O{} O{}} {\vsGen[#1]{\vsWand}[#2]}
+
% for now, the update modality looks like a pvs without masks.
\NewDocumentCommand \upd {} {\mathord{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 21ccdfd6d..8105f9bfc 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -1,3 +1,5 @@
+\let\bar\overline
+
\section{Language}
\label{sec:language}
@@ -6,21 +8,21 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions}
\item There exist functions $\ofval : \textdom{Val} \to \textdom{Expr}$ and $\toval : \textdom{Expr} \pfn \textdom{val}$ (notice the latter is partial), such that
\begin{mathpar} {\All \expr, \val. \toval(\expr) = \val \Ra \ofval(\val) = \expr} \and {\All\val. \toval(\ofval(\val)) = \val}
\end{mathpar}
-\item There exists a \emph{primitive reduction relation} \[(-,- \step -,-,-) \subseteq \textdom{Expr} \times \textdom{State} \times \textdom{Expr} \times \textdom{State} \times (\textdom{Expr} \uplus \set{\bot})\]
- We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, \bot$. \\
- A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f$ indicates that, when $\expr_1$ reduces to $\expr_2$, a \emph{new thread} $\expr_\f$ is forked off.
+\item There exists a \emph{primitive reduction relation} \[(-,- \step -,-,-) \subseteq \textdom{Expr} \times \textdom{State} \times \textdom{Expr} \times \textdom{State} \times (\cup_n \textdom{Expr}^n)\]
+ A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \overline\expr$ indicates that, when $\expr_1$ reduces to $\expr_2$, the new threads in the list $\overline\expr$ is forked off.
+ We will write $\expr_1, \state_1 \step \expr_2, \state_2$ for $\expr_1, \state_1 \step \expr_2, \state_2, ()$, \ie when no threads are forked off. \\
\item All values are stuck:
\[ \expr, \_ \step \_, \_, \_ \Ra \toval(\expr) = \bot \]
\end{itemize}
\begin{defn}
An expression $\expr$ and state $\state$ are \emph{reducible} (written $\red(\expr, \state)$) if
- \[ \Exists \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \]
+ \[ \Exists \expr_2, \state_2, \bar\expr. \expr,\state \step \expr_2,\state_2,\bar\expr \]
\end{defn}
\begin{defn}
An expression $\expr$ is said to be \emph{atomic} if it reduces in one step to a value:
- \[ \All\state_1, \expr_2, \state_2, \expr_\f. \expr, \state_1 \step \expr_2, \state_2, \expr_\f \Ra \Exists \val_2. \toval(\expr_2) = \val_2 \]
+ \[ \All\state_1, \expr_2, \state_2, \bar\expr. \expr, \state_1 \step \expr_2, \state_2, \bar\expr \Ra \Exists \val_2. \toval(\expr_2) = \val_2 \]
\end{defn}
\begin{defn}[Context]
@@ -29,9 +31,9 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions}
\item $\lctx$ does not turn non-values into values:\\
$\All\expr. \toval(\expr) = \bot \Ra \toval(\lctx(\expr)) = \bot $
\item One can perform reductions below $\lctx$:\\
- $\All \expr_1, \state_1, \expr_2, \state_2, \expr_\f. \expr_1, \state_1 \step \expr_2,\state_2,\expr_\f \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\expr_\f $
+ $\All \expr_1, \state_1, \expr_2, \state_2, \bar\expr. \expr_1, \state_1 \step \expr_2,\state_2,\bar\expr \Ra \lctx(\expr_1), \state_1 \step \lctx(\expr_2),\state_2,\bar\expr $
\item Reductions stay below $\lctx$ until there is a value in the hole:\\
- $\All \expr_1', \state_1, \expr_2, \state_2, \expr_\f. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\expr_\f \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\expr_\f $
+ $\All \expr_1', \state_1, \expr_2, \state_2, \bar\expr. \toval(\expr_1') = \bot \land \lctx(\expr_1'), \state_1 \step \expr_2,\state_2,\bar\expr \Ra \Exists\expr_2'. \expr_2 = \lctx(\expr_2') \land \expr_1', \state_1 \step \expr_2',\state_2,\bar\expr $
\end{enumerate}
\end{defn}
@@ -48,13 +50,9 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
\cfg{\tpool'}{\state'}}
\begin{mathpar}
\infer
- {\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f \and \expr_\f \neq \bot}
- {\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state_1} \step
- \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus [\expr_\f]}{\state_2}}
-\and\infer
- {\expr_1, \state_1 \step \expr_2, \state_2}
+ {\expr_1, \state_1 \step \expr_2, \state_2, \bar\expr}
{\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state_1} \step
- \cfg{\tpool \dplus [\expr_2] \dplus \tpool'}{\state_2}}
+ \cfg{\tpool \dplus [\expr_2] \dplus \tpool' \dplus \bar\expr}{\state_2}}
\end{mathpar}
\clearpage
@@ -62,6 +60,7 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
\label{sec:program-logic}
This section describes how to build a program logic for an arbitrary language (\cf \Sref{sec:language}) on top of the logic described in \Sref{sec:hogs}.
+So in the following, we assume that some language $\Lang$ was fixed.
\subsection{World Satisfaction, Invariants, View Shifts}
@@ -82,24 +81,56 @@ Finally, $\textmon{State}$ is used to provide the program with a view of the phy
Furthermore, we assume that instances named $\gname_{\textmon{State}}$, $\gname_{\textmon{Inv}}$, $\gname_{\textmon{En}}$ and $\gname_{\textmon{Dis}}$ of these CMRAs have been created.
(We will discuss later how this assumption is discharged.)
+\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 : \mathbb N \fpfn \Prop. \ownGhost{\gname_{\textmon{Inv}}}{\authfull \aginj(\latertinj(\wIso(I)))}
-%
-%(∃ I : gmap positive (iProp Σ),
-% own invariant_name (◠(invariant_unfold <$> I : gmap _ _)) ★
-% [★ map] i ↦ Q ∈ I, ▷ Q ★ ownD {[i]} ∨ ownE {[i]})
+ W \eqdef{}& \Exists I : \mathbb N \fpfn \Prop. \ownGhost{\gname_{\textmon{Inv}}}{\authfull \aginj(\latertinj(\wIso(I)))} * \Sep_{\iname \in \dom(I)} \left( \later I(\iname) * \ownGhost{\gname_{\textmon{Dis}}}{\set{\iname}} \lor \ownGhost{\gname_{\textmon{En}}}{\set{\iname}} \right)
+\end{align*}
+
+\paragraph{Invariants.}
+The following assertion states that an invariant with name $\iname$ exists and maintains assertion $\prop$:
+\[ \knowInv\iname\prop \eqdef \ownGhost{\gname_{\textmon{Inv}}}{\authfrag \aginj(\latertinj(\wIso(\prop)))} \]
+
+\paragraph{View Shifts.}
+Next, we define \emph{view updates}, which are essentially the same as the resource updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants:
+\[ \pvs[\mask_1][\mask_2] \prop \eqdef W * \ownGhost{\gname_{\textmon{En}}}{\mask_1} \wand W * \ownGhost{\gname_{\textmon{En}}}{\mask_2} * \prop \]
+
+We further define the notions of \emph{view shifts} and \emph{linear view shifts}:
+\begin{align*}
+ \prop \vs[\mask_1][\mask_2] \propB \eqdef{}& \always(\prop \Ra \pvs[\mask_1][\mask_2] \propB) \\
+ \prop \vsW[\mask_1][\mask_2] \propB \eqdef{}& \prop \wand \pvs[\mask_1][\mask_2] \propB
+\end{align*}
+
+\ralf{Show some proof rules.}
+
+\subsection{Hoare Triples}
+
+Finally, we can define the core piece of the program logic, the assertion that reasons about program behavior: Weakest precondition, from which Hoare triples will be derived.
+We assume that everything making up the definition of the language, \ie values, expressions, states, the conversion functions, reduction relation and all their properties, are suitably reflected into the logic (\ie they are part of the signature $\Sig$).
+
+\begin{align*}
+ \textdom{pre-wp}(\textdom{wp})(\mask, \expr, \pred) \eqdef{}&
+ (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \prop) \lor {}\\
+ &\Bigl(\toval(\expr) = \bot \land \All \state. \ownGhost{\gname_{\textmon{State}}}{\authfull \state} \vsW[\mask][\emptyset] {}\\
+ &\qquad \red(\expr, \state) * \later\All \expr', \state', \bar\expr. (\expr, \state \step \expr', \state', \bar\expr) \vsW[\emptyset][\mask] {}\\
+ &\qquad\qquad \ownGhost{\gname_{\textmon{State}}}{\authfull \state'} * \textdom{wp}(\mask, \expr', \pred) * \Sep_{\expr'' \in \bar\expr} \textdom{wp}(\mathbb N, \expr'', \Lam \any. \TRUE)\Bigr) \\
+% (* value case *)
+ \wpre\expr[\mask]{\Ret\val. \prop} \eqdef{}& (\MU \textdom{wp}. \textdom{pre-wp}(\textdom{wp}))(\mask, \expr, \Lam\val.\prop)
\end{align*}
+This ties the authoritative part of \textmon{State} to the actual physical state of the reduction witnessed by the weakest precondition.
+The fragment will then be available to the user of the logic, as their way of talking about the physical state:
+\[ \ownPhys\state \eqdef \ownGhost{\gname_{\textmon{State}}}{\authfrag \state} \]
+
+It turns out that weakest precondition is actually quite convenient to work with, in particular when perfoming these proofs on paper.
+Still, for a more traditional presentation, we can easily derive the notion of a Hoare triple:
+\[
+\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \wpre{\expr}[\mask]{\lambda\Ret\val.\propB})}
+\]
\subsection{Lost stuff}
\ralf{TODO: Right now, this is a dump of all the things that moved out of the base...}
-To instantiate Iris, you need to define the following parameters:
-\begin{itemize}
-\item A language $\Lang$, and
-\item a locally contractive bifunctor $\iFunc : \COFEs \to \CMRAs$ defining the ghost state, such that for all COFEs $\cofe$, the CMRA $\iFunc(A)$ has a unit. (By \lemref{lem:cmra-unit-total-core}, this means that the core of $\iFunc(\cofe)$ is a total function.)
-\end{itemize}
We will write $\pvs[\term] \prop$ for $\pvs[\term][\term] \prop$.
If we omit the mask, then it is $\top$ for weakest precondition $\wpre\expr{\Ret\var.\prop}$ and $\emptyset$ for primitive view shifts $\pvs \prop$.
@@ -138,7 +169,7 @@ We introduce additional metavariables ranging over terms and generally let the c
\infer
{\text{$\melt$ is a discrete COFE element}}
-{\timeless{\ownGGhost\melt}}
+{\timeless{\ownM\melt}}
\infer
{\text{$\melt$ is an element of a discrete CMRA}}
@@ -198,7 +229,7 @@ We introduce additional metavariables ranging over terms and generally let the c
\inferH{pvs-update}
{\melt \mupd \meltsB}
-{\ownGGhost\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownGGhost\meltB}
+{\ownM\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownM\meltB}
\end{mathpar}
\paragraph{Laws of weakest preconditions.}
@@ -256,7 +287,7 @@ The adequacy statement concerning functional correctness reads as follows:
\begin{align*}
&\All \mask, \expr, \val, \pred, \state, \melt, \state', \tpool'.
\\&(\All n. \melt \in \mval_n) \Ra
- \\&( \ownPhys\state * \ownGGhost\melt \proves \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra
+ \\&( \ownPhys\state * \ownM\melt \proves \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra
\\&\cfg{\state}{[\expr]} \step^\ast
\cfg{\state'}{[\val] \dplus \tpool'} \Ra
\\&\pred(\val)
@@ -267,7 +298,7 @@ Furthermore, the following adequacy statement shows that our weakest preconditio
\begin{align*}
&\All \mask, \expr, \state, \melt, \state', \tpool'.
\\&(\All n. \melt \in \mval_n) \Ra
- \\&( \ownPhys\state * \ownGGhost\melt \proves \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra
+ \\&( \ownPhys\state * \ownM\melt \proves \wpre{\expr}[\mask]{x.\; \pred(x)}) \Ra
\\&\cfg{\state}{[\expr]} \step^\ast
\cfg{\state'}{\tpool'} \Ra
\\&\All\expr'\in\tpool'. \toval(\expr') \neq \bot \lor \red(\expr', \state')
@@ -320,20 +351,6 @@ $\textdom{wp}$ is defined as the fixed-point of a contractive function.
\end{align*}
-\typedsection{Interpretation of program logic assertions}{\Sem{\vctx \proves \term : \Prop} : \Sem{\vctx} \nfn \iProp}
-
-$\knowInv\iname\prop$, $\ownGGhost\melt$ and $\ownPhys\state$ are just syntactic sugar for forms of $\ownM{-}$.
-\begin{align*}
- \knowInv{\iname}{\prop} &\eqdef \ownM{[\iname \mapsto \aginj(\latertinj(\wIso(\prop)))], \munit, \munit} \\
- \ownGGhost{\melt} &\eqdef \ownM{\munit, \munit, \melt} \\
- \ownPhys{\state} &\eqdef \ownM{\munit, \exinj(\state), \munit} \\
-~\\
- \Sem{\vctx \proves \pvs[\mask_1][\mask_2] \prop : \Prop}_\gamma &\eqdef
- \textdom{pvs}^{\Sem{\vctx \proves \mask_2 : \textlog{InvMask}}_\gamma}_{\Sem{\vctx \proves \mask_1 : \textlog{InvMask}}_\gamma}(\Sem{\vctx \proves \prop : \Prop}_\gamma) \\
- \Sem{\vctx \proves \wpre{\expr}[\mask]{\Ret\var.\prop} : \Prop}_\gamma &\eqdef
- \textdom{wp}_{\Sem{\vctx \proves \mask : \textlog{InvMask}}_\gamma}(\Sem{\vctx \proves \expr : \textlog{Expr}}_\gamma, \Lam\val. \Sem{\vctx \proves \prop : \Prop}_{\gamma[\var\mapsto\val]})
-\end{align*}
-
%%% Local Variables:
%%% mode: latex
--
GitLab