Commit 1a18f2ff authored by Ralf Jung's avatar Ralf Jung

docs: update model

parent 9df1dae0
......@@ -60,7 +60,7 @@ Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$.
\Exists \var:\type. \prop \mid
\All \var:\type. \prop \mid
\ownGGhost{\term} \mid \mval(\term) \mid
\ownM{\term} \mid \mval(\term) \mid
\always\prop \mid
{\later\prop} \mid
\upd \prop\mid
......@@ -167,7 +167,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
{\vctx \proves \wtt{\All x:\type. \prop}{\Prop}}
\infer{\vctx \proves \wtt{\melt}{\textlog{M}}}
{\vctx \proves \wtt{\ownGGhost{\melt}}{\Prop}}
{\vctx \proves \wtt{\ownM{\melt}}{\Prop}}
\infer{\vctx \proves \wtt{\melt}{\type} \and \text{$\type$ is a CMRA}}
{\vctx \proves \wtt{\mval(\melt)}{\Prop}}
......@@ -345,10 +345,10 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
\paragraph{Laws for ghosts and validity.}
\ownGGhost{\melt} * \ownGGhost{\meltB} &\provesIff& \ownGGhost{\melt \mtimes \meltB} \\
\ownGGhost\melt &\proves& \always{\ownGGhost{\mcore\melt}} \\
\TRUE &\proves& \ownGGhost{\munit} \\
\later\ownGGhost\melt &\proves& \Exists\meltB. \ownGGhost\meltB \land \later(\melt = \meltB)
\ownM{\melt} * \ownM{\meltB} &\provesIff& \ownM{\melt \mtimes \meltB} \\
\ownM\melt &\proves& \always{\ownM{\mcore\melt}} \\
\TRUE &\proves& \ownM{\munit} \\
\later\ownM\melt &\proves& \Exists\meltB. \ownM\meltB \land \later(\melt = \meltB)
......@@ -360,7 +360,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
{\mval(\melt) \proves \FALSE}
\ownGGhost{\melt} &\proves& \mval(\melt) \\
\ownM{\melt} &\proves& \mval(\melt) \\
\mval(\melt \mtimes \meltB) &\proves& \mval(\melt) \\
\mval(\melt) &\proves& \always\mval(\melt)
......@@ -385,7 +385,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
{\melt \mupd \meltsB}
{\ownGGhost\melt \proves \upd \Exists\meltB\in\meltsB. \ownGGhost\meltB}
{\ownM\melt \proves \upd \Exists\meltB\in\meltsB. \ownM\meltB}
This diff is collapsed.
......@@ -240,6 +240,91 @@ Furthermore, the following adequacy statement shows that our weakest preconditio
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.
\subsection{Iris model}
\paragraph{Semantic domain of assertions.}
The first complicated task in building a model of full Iris is defining the semantic model of $\Prop$.
We start by defining the functor that assembles the CMRAs we need to the global resource CMRA:
\textdom{ResF}(\cofe^\op, \cofe) \eqdef{}& \record{\wld: \mathbb{N} \fpfn \agm(\latert \cofe), \pres: \maybe{\exm(\textdom{State})}, \ghostRes: \iFunc(\cofe^\op, \cofe)}
Above, $\maybe\monoid$ is the monoid obtained by adding a unit to $\monoid$.
(It's not a coincidence that we used the same notation for the range of the core; it's the same type either way: $\monoid + 1$.)
Remember that $\iFunc$ is the user-chosen bifunctor from $\COFEs$ to $\CMRAs$ (see~\Sref{sec:logic}).
$\textdom{ResF}(\cofe^\op, \cofe)$ is a CMRA by lifting the individual CMRAs pointwise.
Furthermore, since $\Sigma$ is locally contractive, so is $\textdom{ResF}$.
Now we can write down the recursive domain equation:
\[ \iPreProp \cong \UPred(\textdom{ResF}(\iPreProp, \iPreProp)) \]
$\iPreProp$ is a COFE defined as the fixed-point of a locally contractive bifunctor.
This fixed-point exists and is unique by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}.
We do not need to consider how the object is constructed.
We only need the isomorphism, given by
\Res &\eqdef \textdom{ResF}(\iPreProp, \iPreProp) \\
\iProp &\eqdef \UPred(\Res) \\
\wIso &: \iProp \nfn \iPreProp \\
\wIso^{-1} &: \iPreProp \nfn \iProp
We then pick $\iProp$ as the interpretation of $\Prop$:
\[ \Sem{\Prop} \eqdef \iProp \]
\paragraph{Interpretation of assertions.}
$\iProp$ is a $\UPred$, and hence the definitions from \Sref{sec:upred-logic} apply.
We only have to define the interpretation of the missing connectives, the most interesting bits being primitive view shifts and weakest preconditions.
\typedsection{World satisfaction}{\wsat{-}{-}{-} :
\Delta\textdom{State} \times
\Delta\pset{\mathbb{N}} \times
\textdom{Res} \nfn \SProp }
\wsatpre(n, \mask, \state, \rss, \rs) & \eqdef \begin{inbox}[t]
\rs \in \mval_{n+1} \land \rs.\pres = \exinj(\sigma) \land
\dom(\rss) \subseteq \mask \cap \dom( \rs.\wld) \land {}\\
\All\iname \in \mask, \prop \in \iProp. (\rs.\wld)(\iname) \nequiv{n+1} \aginj(\latertinj(\wIso(\prop))) \Ra n \in \prop(\rss(\iname))
\wsat{\state}{\mask}{\rs} &\eqdef \set{0}\cup\setComp{n+1}{\Exists \rss : \mathbb{N} \fpfn \textdom{Res}. \wsatpre(n, \mask, \state, \rss, \rs \mtimes \prod_\iname \rss(\iname))}
\typedsection{Primitive view-shift}{\mathit{pvs}_{-}^{-}(-) : \Delta(\pset{\mathbb{N}}) \times \Delta(\pset{\mathbb{N}}) \times \iProp \nfn \iProp}
\mathit{pvs}_{\mask_1}^{\mask_2}(\prop) &= \Lam \rs. \setComp{n}{\begin{aligned}
\All \rs_\f, k, \mask_\f, \state.& 0 < k \leq n \land (\mask_1 \cup \mask_2) \disj \mask_\f \land k \in \wsat\state{\mask_1 \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\&
\Exists \rsB. k \in \prop(\rsB) \land k \in \wsat\state{\mask_2 \cup \mask_\f}{\rsB \mtimes \rs_\f}
\typedsection{Weakest precondition}{\mathit{wp}_{-}(-, -) : \Delta(\pset{\mathbb{N}}) \times \Delta(\textdom{Exp}) \times (\Delta(\textdom{Val}) \nfn \iProp) \nfn \iProp}
$\textdom{wp}$ is defined as the fixed-point of a contractive function.
\textdom{pre-wp}(\textdom{wp})(\mask, \expr, \pred) &\eqdef \Lam\rs. \setComp{n}{\begin{aligned}
\All &\rs_\f, m, \mask_\f, \state. 0 \leq m < n \land \mask \disj \mask_\f \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\
&(\All\val. \toval(\expr) = \val \Ra \Exists \rsB. m+1 \in \pred(\val)(\rsB) \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rsB \mtimes \rs_\f}) \land {}\\
&(\toval(\expr) = \bot \land 0 < m \Ra \red(\expr, \state) \land \All \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \Ra {}\\
&\qquad \Exists \rsB_1, \rsB_2. m \in \wsat\state{\mask \cup \mask_\f}{\rsB_1 \mtimes \rsB_2 \mtimes \rs_\f} \land m \in \textdom{wp}(\mask, \expr_2, \pred)(\rsB_1) \land {}&\\
&\qquad\qquad (\expr_\f = \bot \lor m \in \textdom{wp}(\top, \expr_\f, \Lam\any.\Lam\any.\mathbb{N})(\rsB_2))
\end{aligned}} \\
\textdom{wp}_\mask(\expr, \pred) &\eqdef \mathit{fix}(\textdom{pre-wp})(\mask, \expr, \pred)
\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{-}$.
\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]})
%%% Local Variables:
%%% mode: latex
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