Commit 0621aa23 authored by Ralf Jung's avatar Ralf Jung

start updating the appendix to iris 3.0

parent 2e98600d
\section{Language}
\section{Base Logic}
\label{sec:base-logic}
A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} (metavariable $\expr$), a set \textdom{Val} of \emph{values} (metavariable $\val$), and a set \textdom{State} of \emph{states} (metvariable $\state$) such that
\begin{itemize}
\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 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 \]
\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 \]
\end{defn}
\begin{defn}[Context]
A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied:
\begin{enumerate}[itemsep=0pt]
\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 $
\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 $
\end{enumerate}
\end{defn}
\subsection{Concurrent language}
The base logic is parameterized by an arbitrary CMRA $\monoid$ having a unit.
This defines the structure of resources that can be owned.
For any language $\Lang$, we define the corresponding thread-pool semantics.
\paragraph{Machine syntax}
\[
\tpool \in \textdom{ThreadPool} \eqdef \bigcup_n \textdom{Expr}^n
\]
\judgment[Machine reduction]{\cfg{\tpool}{\state} \step
\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}
{\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state_1} \step
\cfg{\tpool \dplus [\expr_2] \dplus \tpool'}{\state_2}}
\end{mathpar}
\clearpage
\section{Logic}
\label{sec:logic}
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 $A$, the CMRA $\iFunc(A)$ has a unit. (By \lemref{lem:cmra-unit-total-core}, this means that the core of $\iFunc(A)$ is a total function.)
\end{itemize}
\noindent
As usual for higher-order logics, you can furthermore pick a \emph{signature} $\Sig = (\SigType, \SigFn, \SigAx)$ to add more types, symbols and axioms to the language.
You have to make sure that $\SigType$ includes the base types:
\[
\SigType \supseteq \{ \textlog{Val}, \textlog{Expr}, \textlog{State}, \textlog{M}, \textlog{InvName}, \textlog{InvMask}, \Prop \}
\SigType \supseteq \{ \textlog{M}, \Prop \}
\]
Elements of $\SigType$ are ranged over by $\sigtype$.
......@@ -88,7 +25,8 @@ Elements of $\SigAx$ are ranged over by $\sigax$.
\subsection{Grammar}\label{sec:grammar}
\paragraph{Syntax.}
Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\textdom{Var}$ of variables (ranged over by metavariables $x$, $y$, $z$):
Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\textdom{Var}$ of variables (ranged over by metavariables $x$, $y$, $z$).
Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$.
\begin{align*}
\type \bnfdef{}&
......@@ -105,7 +43,7 @@ Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\t
\pi_i\; \term \mid
\Lam \var:\type.\term \mid
\term(\term) \mid
\munit \mid
\melt \mid
\mcore\term \mid
\term \mtimes \term \mid
\\&
......@@ -122,47 +60,15 @@ Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\t
\Exists \var:\type. \prop \mid
\All \var:\type. \prop \mid
\\&
\knowInv{\term}{\prop} \mid
\ownGGhost{\term} \mid \mval(\term) \mid
\ownPhys{\term} \mid
\always\prop \mid
{\later\prop} \mid
\pvs[\term][\term] \prop\mid
\wpre{\term}[\term]{\Ret\var.\term}
\upd \prop\mid
\end{align*}
Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality.
Note that $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
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$.
%FIXME $\top$ is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.
Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them.
This is a \emph{meta-level} assertion about propositions, defined as follows:
Note that the modalities $\upd$, $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
\[ \vctx \proves \timeless{\prop} \eqdef \vctx\mid\later\prop \proves \prop \lor \later\FALSE \]
\paragraph{Metavariable conventions.}
We introduce additional metavariables ranging over terms and generally let the choice of metavariable indicate the term's type:
\[
\begin{array}{r|l}
\text{metavariable} & \text{type} \\\hline
\term, \termB & \text{arbitrary} \\
\val, \valB & \textlog{Val} \\
\expr & \textlog{Expr} \\
\state & \textlog{State} \\
\end{array}
\qquad\qquad
\begin{array}{r|l}
\text{metavariable} & \text{type} \\\hline
\iname & \textlog{InvName} \\
\mask & \textlog{InvMask} \\
\melt, \meltB & \textlog{M} \\
\prop, \propB, \propC & \Prop \\
\pred, \predB, \predC & \type\to\Prop \text{ (when $\type$ is clear from context)} \\
\end{array}
\]
\paragraph{Variable conventions.}
We assume that, if a term occurs multiple times in a rule, its free variables are exactly those binders which are available at every occurrence.
......@@ -259,22 +165,12 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
\and
\infer{\vctx, x:\type \proves \wtt{\prop}{\Prop}}
{\vctx \proves \wtt{\All x:\type. \prop}{\Prop}}
\and
\infer{
\vctx \proves \wtt{\prop}{\Prop} \and
\vctx \proves \wtt{\iname}{\textlog{InvName}}
}{
\vctx \proves \wtt{\knowInv{\iname}{\prop}}{\Prop}
}
\and
\infer{\vctx \proves \wtt{\melt}{\textlog{M}}}
{\vctx \proves \wtt{\ownGGhost{\melt}}{\Prop}}
\and
\infer{\vctx \proves \wtt{\melt}{\type} \and \text{$\type$ is a CMRA}}
{\vctx \proves \wtt{\mval(\melt)}{\Prop}}
\and
\infer{\vctx \proves \wtt{\state}{\textlog{State}}}
{\vctx \proves \wtt{\ownPhys{\state}}{\Prop}}
\and
\infer{\vctx \proves \wtt{\prop}{\Prop}}
{\vctx \proves \wtt{\always\prop}{\Prop}}
......@@ -283,19 +179,9 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
{\vctx \proves \wtt{\later\prop}{\Prop}}
\and
\infer{
\vctx \proves \wtt{\prop}{\Prop} \and
\vctx \proves \wtt{\mask}{\textlog{InvMask}} \and
\vctx \proves \wtt{\mask'}{\textlog{InvMask}}
}{
\vctx \proves \wtt{\pvs[\mask][\mask'] \prop}{\Prop}
}
\and
\infer{
\vctx \proves \wtt{\expr}{\textlog{Expr}} \and
\vctx,\var:\textlog{Val} \proves \wtt{\term}{\Prop} \and
\vctx \proves \wtt{\mask}{\textlog{InvMask}}
\vctx \proves \wtt{\prop}{\Prop}
}{
\vctx \proves \wtt{\wpre{\expr}[\mask]{\Ret\var.\term}}{\Prop}
\vctx \proves \wtt{\upd \prop}{\Prop}
}
\end{mathparpagebreakable}
......@@ -454,40 +340,6 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
\end{mathpar}
A type $\type$ being \emph{inhabited} means that $ \proves \wtt{\term}{\type}$ is derivable for some $\term$.
\begin{mathpar}
\infer
{\text{$\term$ or $\term'$ is a discrete COFE element}}
{\timeless{\term =_\type \term'}}
\infer
{\text{$\melt$ is a discrete COFE element}}
{\timeless{\ownGGhost\melt}}
\infer
{\text{$\melt$ is an element of a discrete CMRA}}
{\timeless{\mval(\melt)}}
\infer{}
{\timeless{\ownPhys\state}}
\infer
{\vctx \proves \timeless{\propB}}
{\vctx \proves \timeless{\prop \Ra \propB}}
\infer
{\vctx \proves \timeless{\propB}}
{\vctx \proves \timeless{\prop \wand \propB}}
\infer
{\vctx,\var:\type \proves \timeless{\prop}}
{\vctx \proves \timeless{\All\var:\type.\prop}}
\infer
{\vctx,\var:\type \proves \timeless{\prop}}
{\vctx \proves \timeless{\Exists\var:\type.\prop}}
\end{mathpar}
\paragraph{Laws for the always modality.}
\begin{mathpar}
\infer[$\always$I]
......@@ -512,149 +364,31 @@ A type $\type$ being \emph{inhabited} means that $ \proves \wtt{\term}{\type}$ i
\and
{ \term =_\type \term' \proves \always \term =_\type \term'}
\and
{ \knowInv\iname\prop \proves \always \knowInv\iname\prop}
\and
{ \ownGGhost{\mcore\melt} \proves \always \ownGGhost{\mcore\melt}}
\and
{ \mval(\melt) \proves \always \mval(\melt)}
\end{mathpar}
\paragraph{Laws of primitive view shifts.}
\paragraph{Laws for the update modality.}
\begin{mathpar}
\infer[pvs-intro]
{}{\prop \proves \pvs[\mask] \prop}
\infer[pvs-mono]
{\prop \proves \propB}
{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1][\mask_2] \propB}
\infer[pvs-timeless]
{\timeless\prop}
{\later\prop \proves \pvs[\mask] \prop}
\infer[pvs-trans]
{\mask_2 \subseteq \mask_1 \cup \mask_3}
{\pvs[\mask_1][\mask_2] \pvs[\mask_2][\mask_3] \prop \proves \pvs[\mask_1][\mask_3] \prop}
\infer[pvs-mask-frame]
{}{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1 \uplus \mask_\f][\mask_2 \uplus \mask_\f] \prop}
\infer[pvs-frame]
{}{\propB * \pvs[\mask_1][\mask_2]\prop \proves \pvs[\mask_1][\mask_2] \propB * \prop}
\infer[upd-intro]
{}{\prop \proves \upd \prop}
\inferH{pvs-allocI}
{\text{$\mask$ is infinite}}
{\later\prop \proves \pvs[\mask] \Exists \iname \in \mask. \knowInv\iname\prop}
\infer[upd-trans]
{}
{\upd \upd \prop \proves \upd \prop}
\inferH{pvs-openI}
{}{\knowInv\iname\prop \proves \pvs[\set\iname][\emptyset] \later\prop}
\infer[upd-frame]
{}{\propB * \upd\prop \proves \upd (\propB * \prop)}
\inferH{pvs-closeI}
{}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE}
\inferH{pvs-update}
\inferH{upd-update}
{\melt \mupd \meltsB}
{\ownGGhost\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownGGhost\meltB}
{\ownGGhost\melt \proves \upd \Exists\meltB\in\meltsB. \ownGGhost\meltB}
\end{mathpar}
\paragraph{Laws of weakest preconditions.}
\begin{mathpar}
\infer[wp-value]
{}{\prop[\val/\var] \proves \wpre{\val}[\mask]{\Ret\var.\prop}}
\infer[wp-mono]
{\mask_1 \subseteq \mask_2 \and \var:\textlog{val}\mid\prop \proves \propB}
{\wpre\expr[\mask_1]{\Ret\var.\prop} \proves \wpre\expr[\mask_2]{\Ret\var.\propB}}
\infer[pvs-wp]
{}{\pvs[\mask] \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}
\infer[wp-pvs]
{}{\wpre\expr[\mask]{\Ret\var.\pvs[\mask] \prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}
\infer[wp-atomic]
{\mask_2 \subseteq \mask_1 \and \physatomic{\expr}}
{\pvs[\mask_1][\mask_2] \wpre\expr[\mask_2]{\Ret\var. \pvs[\mask_2][\mask_1]\prop}
\proves \wpre\expr[\mask_1]{\Ret\var.\prop}}
\infer[wp-frame]
{}{\propB * \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\propB*\prop}}
\infer[wp-frame-step]
{\toval(\expr) = \bot \and \mask_2 \subseteq \mask_1}
{\wpre\expr[\mask]{\Ret\var.\prop} * \pvs[\mask_1][\mask_2]\later\pvs[\mask_2][\mask_1]\propB \proves \wpre\expr[\mask \uplus \mask_1]{\Ret\var.\propB*\prop}}
\infer[wp-bind]
{\text{$\lctx$ is a context}}
{\wpre\expr[\mask]{\Ret\var. \wpre{\lctx(\ofval(\var))}[\mask]{\Ret\varB.\prop}} \proves \wpre{\lctx(\expr)}[\mask]{\Ret\varB.\prop}}
\end{mathpar}
\paragraph{Lifting of operational semantics.}~
\begin{mathpar}
\infer[wp-lift-step]
{\mask_2 \subseteq \mask_1 \and
\toval(\expr_1) = \bot}
{ {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below...
~~\pvs[\mask_1][\mask_2] \Exists \state_1. \red(\expr_1,\state_1) \land \later\ownPhys{\state_1} * {}\\\qquad\qquad\qquad \later\All \expr_2, \state_2, \expr_\f. \left( (\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f) \land \ownPhys{\state_2} \right) \wand \pvs[\mask_2][\mask_1] \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} {}\\\proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}
\end{inbox}} }
\\\\
\infer[wp-lift-pure-step]
{\toval(\expr_1) = \bot \and
\All \state_1. \red(\expr_1, \state_1) \and
\All \state_1, \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \state_1 = \state_2 }
{\later\All \state, \expr_2, \expr_\f. (\expr_1,\state \step \expr_2, \state,\expr_\f) \Ra \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
\end{mathpar}
Notice that primitive view shifts cover everything to their right, \ie $\pvs \prop * \propB \eqdef \pvs (\prop * \propB)$.
Here we define $\wpre{\expr_\f}[\mask]{\Ret\var.\prop} \eqdef \TRUE$ if $\expr_\f = \bot$ (remember that our stepping relation can, but does not have to, define a forked-off expression).
\subsection{Adequacy}
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
\\&\cfg{\state}{[\expr]} \step^\ast
\cfg{\state'}{[\val] \dplus \tpool'} \Ra
\\&\pred(\val)
\end{align*}
where $\pred$ is a \emph{meta-level} predicate over values, \ie it can mention neither resources nor invariants.
Furthermore, the following adequacy statement shows that our weakest preconditions imply that the execution never gets \emph{stuck}: Every expression in the thread pool either is a value, or can reduce further.
\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
\\&\cfg{\state}{[\expr]} \step^\ast
\cfg{\state'}{\tpool'} \Ra
\\&\All\expr'\in\tpool'. \toval(\expr') \neq \bot \lor \red(\expr', \state')
\end{align*}
Notice that this is stronger than saying that the thread pool can reduce; we actually assert that \emph{every} non-finished thread can take a step.
% RJ: If we want this section back, we should port it to primitive view shifts and prove it in Coq.
% \subsection{Unsound rules}
% Some rule suggestions (or rather, wishes) keep coming up, which are unsound. We collect them here.
% \begin{mathpar}
% \infer
% {P \vs Q}
% {\later P \vs \later Q}
% \and
% \infer
% {\later(P \vs Q)}
% {\later P \vs \later Q}
% \end{mathpar}
% Of course, the second rule implies the first, so let's focus on that.
% Since implications work under $\later$, from $\later P$ we can get $\later \pvs{Q}$.
% If we now try to prove $\pvs{\later Q}$, we will be unable to establish world satisfaction in the new world:
% We have no choice but to use $\later \pvs{Q}$ at one step index below what we are operating on (because we have it under a $\later$).
% We can easily get world satisfaction for that lower step-index (by downwards-closedness of step-indexed predicates).
% We can, however, not make much use of the world satisfaction that we get out, becaase it is one step-index too low.
\subsection{Soundness}
The soundness statement of the logic
%%% Local Variables:
......
......@@ -249,6 +249,9 @@
{\vsGen[#1]{\Lleftarrow\!\!\!\Rrightarrow}[#2]}
\NewDocumentCommand \pvs {O{} O{}} {\mathord{\vsGen[#1]{{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}[#2]\kern0.2ex}}
% for now, the update modality looks like a pvs without masks.
\NewDocumentCommand \upd {} {\mathord{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}
%% Hoare Triples
\newcommand*{\hoaresizebox}[1]{%
......
......@@ -31,10 +31,12 @@
\endgroup\clearpage\begingroup
\input{constructions}
\endgroup\clearpage\begingroup
\input{logic}
\input{base-logic}
\endgroup\clearpage\begingroup
\input{model}
\endgroup\clearpage\begingroup
\input{program-logic}
\endgroup\clearpage\begingroup
\input{derived}
\endgroup\clearpage\begingroup
\printbibliography
......
\section{Language}
A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} (metavariable $\expr$), a set \textdom{Val} of \emph{values} (metavariable $\val$), and a set \textdom{State} of \emph{states} (metvariable $\state$) such that
\begin{itemize}
\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 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 \]
\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 \]
\end{defn}
\begin{defn}[Context]
A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied:
\begin{enumerate}[itemsep=0pt]
\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 $
\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 $
\end{enumerate}
\end{defn}
\subsection{Concurrent language}
For any language $\Lang$, we define the corresponding thread-pool semantics.
\paragraph{Machine syntax}
\[
\tpool \in \textdom{ThreadPool} \eqdef \bigcup_n \textdom{Expr}^n
\]
\judgment[Machine reduction]{\cfg{\tpool}{\state} \step
\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}
{\cfg{\tpool \dplus [\expr_1] \dplus \tpool'}{\state_1} \step
\cfg{\tpool \dplus [\expr_2] \dplus \tpool'}{\state_2}}
\end{mathpar}
\clearpage
\section{Program Logic}
\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$.
%FIXME $\top$ is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.
Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them.
This is a \emph{meta-level} assertion about propositions, defined as follows:
\[ \vctx \proves \timeless{\prop} \eqdef \vctx\mid\later\prop \proves \prop \lor \later\FALSE \]
\paragraph{Metavariable conventions.}
We introduce additional metavariables ranging over terms and generally let the choice of metavariable indicate the term's type:
\[
\begin{array}{r|l}
\text{metavariable} & \text{type} \\\hline
\term, \termB & \text{arbitrary} \\
\val, \valB & \textlog{Val} \\
\expr & \textlog{Expr} \\
\state & \textlog{State} \\
\end{array}
\qquad\qquad
\begin{array}{r|l}
\text{metavariable} & \text{type} \\\hline
\iname & \textlog{InvName} \\
\mask & \textlog{InvMask} \\
\melt, \meltB & \textlog{M} \\
\prop, \propB, \propC & \Prop \\
\pred, \predB, \predC & \type\to\Prop \text{ (when $\type$ is clear from context)} \\
\end{array}
\]
\begin{mathpar}
\infer
{\text{$\term$ or $\term'$ is a discrete COFE element}}
{\timeless{\term =_\type \term'}}
\infer
{\text{$\melt$ is a discrete COFE element}}
{\timeless{\ownGGhost\melt}}
\infer
{\text{$\melt$ is an element of a discrete CMRA}}
{\timeless{\mval(\melt)}}
\infer{}
{\timeless{\ownPhys\state}}
\infer
{\vctx \proves \timeless{\propB}}
{\vctx \proves \timeless{\prop \Ra \propB}}
\infer
{\vctx \proves \timeless{\propB}}
{\vctx \proves \timeless{\prop \wand \propB}}
\infer
{\vctx,\var:\type \proves \timeless{\prop}}
{\vctx \proves \timeless{\All\var:\type.\prop}}
\infer
{\vctx,\var:\type \proves \timeless{\prop}}
{\vctx \proves \timeless{\Exists\var:\type.\prop}}
\end{mathpar}
\begin{mathpar}
\infer[pvs-intro]
{}{\prop \proves \pvs[\mask] \prop}
\infer[pvs-mono]
{\prop \proves \propB}
{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1][\mask_2] \propB}
\infer[pvs-timeless]
{\timeless\prop}
{\later\prop \proves \pvs[\mask] \prop}
\infer[pvs-trans]
{\mask_2 \subseteq \mask_1 \cup \mask_3}
{\pvs[\mask_1][\mask_2] \pvs[\mask_2][\mask_3] \prop \proves \pvs[\mask_1][\mask_3] \prop}
\infer[pvs-mask-frame]
{}{\pvs[\mask_1][\mask_2] \prop \proves \pvs[\mask_1 \uplus \mask_\f][\mask_2 \uplus \mask_\f] \prop}
\infer[pvs-frame]
{}{\propB * \pvs[\mask_1][\mask_2]\prop \proves \pvs[\mask_1][\mask_2] \propB * \prop}
\inferH{pvs-allocI}
{\text{$\mask$ is infinite}}
{\later\prop \proves \pvs[\mask] \Exists \iname \in \mask. \knowInv\iname\prop}
\inferH{pvs-openI}
{}{\knowInv\iname\prop \proves \pvs[\set\iname][\emptyset] \later\prop}
\inferH{pvs-closeI}
{}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE}
\inferH{pvs-update}
{\melt \mupd \meltsB}
{\ownGGhost\melt \proves \pvs[\mask] \Exists\meltB\in\meltsB. \ownGGhost\meltB}
\end{mathpar}
\paragraph{Laws of weakest preconditions.}
\begin{mathpar}
\infer[wp-value]
{}{\prop[\val/\var] \proves \wpre{\val}[\mask]{\Ret\var.\prop}}
\infer[wp-mono]
{\mask_1 \subseteq \mask_2 \and \var:\textlog{val}\mid\prop \proves \propB}
{\wpre\expr[\mask_1]{\Ret\var.\prop} \proves \wpre\expr[\mask_2]{\Ret\var.\propB}}
\infer[pvs-wp]
{}{\pvs[\mask] \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}
\infer[wp-pvs]
{}{\wpre\expr[\mask]{\Ret\var.\pvs[\mask] \prop} \proves \wpre\expr[\mask]{\Ret\var.\prop}}
\infer[wp-atomic]
{\mask_2 \subseteq \mask_1 \and \physatomic{\expr}}
{\pvs[\mask_1][\mask_2] \wpre\expr[\mask_2]{\Ret\var. \pvs[\mask_2][\mask_1]\prop}
\proves \wpre\expr[\mask_1]{\Ret\var.\prop}}
\infer[wp-frame]
{}{\propB * \wpre\expr[\mask]{\Ret\var.\prop} \proves \wpre\expr[\mask]{\Ret\var.\propB*\prop}}
\infer[wp-frame-step]
{\toval(\expr) = \bot \and \mask_2 \subseteq \mask_1}
{\wpre\expr[\mask]{\Ret\var.\prop} * \pvs[\mask_1][\mask_2]\later\pvs[\mask_2][\mask_1]\propB \proves \wpre\expr[\mask \uplus \mask_1]{\Ret\var.\propB*\prop}}
\infer[wp-bind]
{\text{$\lctx$ is a context}}
{\wpre\expr[\mask]{\Ret\var. \wpre{\lctx(\ofval(\var))}[\mask]{\Ret\varB.\prop}} \proves \wpre{\lctx(\expr)}[\mask]{\Ret\varB.\prop}}
\end{mathpar}
\paragraph{Lifting of operational semantics.}~
\begin{mathpar}
\infer[wp-lift-step]
{\mask_2 \subseteq \mask_1 \and
\toval(\expr_1) = \bot}
{ {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below...
~~\pvs[\mask_1][\mask_2] \Exists \state_1. \red(\expr_1,\state_1) \land \later\ownPhys{\state_1} * {}\\\qquad\qquad\qquad \later\All \expr_2, \state_2, \expr_\f. \left( (\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f) \land \ownPhys{\state_2} \right) \wand \pvs[\mask_2][\mask_1] \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} {}\\\proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}
\end{inbox}} }
\\\\
\infer[wp-lift-pure-step]
{\toval(\expr_1) = \bot \and
\All \state_1. \red(\expr_1, \state_1) \and
\All \state_1, \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \state_1 = \state_2 }
{\later\All \state, \expr_2, \expr_\f. (\expr_1,\state \step \expr_2, \state,\expr_\f) \Ra \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
\end{mathpar}
Notice that primitive view shifts cover everything to their right, \ie $\pvs \prop * \propB \eqdef \pvs (\prop * \propB)$.
Here we define $\wpre{\expr_\f}[\mask]{\Ret\var.\prop} \eqdef \TRUE$ if $\expr_\f = \bot$ (remember that our stepping relation can, but does not have to, define a forked-off expression).
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
\\&\cfg{\state}{[\expr]} \step^\ast
\cfg{\state'}{[\val] \dplus \tpool'} \Ra
\\&\pred(\val)
\end{align*}
where $\pred$ is a \emph{meta-level} predicate over values, \ie it can mention neither resources nor invariants.
Furthermore, the following adequacy statement shows that our weakest preconditions imply that the execution never gets \emph{stuck}: Every expression in the thread pool either is a value, or can reduce further.
\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
\\&\cfg{\state}{[\expr]} \step^\ast
\cfg{\state'}{\tpool'} \Ra
\\&\All\expr'\in\tpool'. \toval(\expr') \neq \bot \lor \red(\expr', \state')
\end{align*}
Notice that this is stronger than saying that the thread pool can reduce; we actually assert that \emph{every} non-finished thread can take a step.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
%%% End:
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment