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

docs: fix some comments raised by Lars

parent 0aaa35e7
......@@ -5,11 +5,14 @@
Given a COFE $\cofe$, we define $\latert\cofe$ as follows:
\begin{align*}
\latert\cofe \eqdef{}& \latertinj(\cofe) \\
\latert\cofe \eqdef{}& \latertinj(x:\cofe) \\
\latertinj(x) \nequiv{n} \latertinj(y) \eqdef{}& n = 0 \lor x \nequiv{n-1} y
\end{align*}
Note that in the definition of the carrier $\latert\cofe$, $\latertinj$ is a constructor (like the constructors in Coq), \ie this is short for $\setComp{\latertinj(x)}{x \in \cofe}$.
$\latert(-)$ is a locally \emph{contractive} functor from $\COFEs$ to $\COFEs$.
\subsection{Uniform Predicates}
Given a CMRA $\monoid$, we define the COFE $\UPred(\monoid)$ of \emph{uniform predicates} over $\monoid$ as follows:
......@@ -25,13 +28,13 @@ where $\mProp$ is the set of meta-level propositions, \eg Coq's \texttt{Prop}.
$\UPred(-)$ is a locally non-expansive functor from $\CMRAs$ to $\COFEs$.
One way to understand this definition is to re-write it a little.
We start by defining the COFE of \emph{step-indexed propositions}: For every step-index, we proposition either holds or does not hold.
We start by defining the COFE of \emph{step-indexed propositions}: For every step-index, the proposition either holds or does not hold.
\begin{align*}
\SProp \eqdef{}& \psetdown{\mathbb{N}} \\
\eqdef{}& \setComp{X \in \pset{\mathbb{N}}}{ \All n, m. n \geq m \Ra n \in X \Ra m \in X } \\
X \nequiv{n} Y \eqdef{}& \All m \leq n. m \in X \Lra m \in Y
\end{align*}
Notice that with this notion of $\SProp$ is already hidden in the validity predicate $\mval_n$ of a CMRA:
Notice that this notion of $\SProp$ is already hidden in the validity predicate $\mval_n$ of a CMRA:
We could equivalently require every CMRA to define $\mval_{-}(-) : \monoid \nfn \SProp$, replacing \ruleref{cmra-valid-ne} and \ruleref{cmra-valid-mono}.
Now we can rewrite $\UPred(\monoid)$ as monotone step-indexed predicates over $\monoid$, where the definition of a ``monotone'' function here is a little funny.
......@@ -75,6 +78,8 @@ We obtain the following frame-preserving updates:
{\melt \mupd \meltsB}
{f[i \mapsto \melt] \mupd \setComp{ f[i \mapsto \meltB]}{\meltB \in \meltsB}}
\end{mathpar}
Remember that $\mval$ is the set of elements of a CMRA that are valid at \emph{all} step-indices.
$K \fpfn (-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$.
\subsection{Agreement}
......@@ -87,10 +92,12 @@ Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows:
& \text{quotiented by} \\
\melt \equiv \meltB \eqdef{}& \melt.\aginjV = \meltB.\aginjV \land \All n. n \in \melt.\aginjV \Ra \melt.\aginjc(n) \nequiv{n} \meltB.\aginjc(n) \\
\melt \nequiv{n} \meltB \eqdef{}& (\All m \leq n. m \in \melt.\aginjV \Lra m \in \meltB.\aginjV) \land (\All m \leq n. m \in \melt.\aginjV \Ra \melt.\aginjc(m) \nequiv{m} \meltB.\aginjc(m)) \\
\mval_n \eqdef{}& \setComp{\melt \in \monoid}{ n \in \melt.\aginjV \land \All m \leq n. \melt.\aginjc(n) \nequiv{m} \melt.\aginjc(m) } \\
\mval_n \eqdef{}& \setComp{\melt \in \agm(\cofe)}{ n \in \melt.\aginjV \land \All m \leq n. \melt.\aginjc(n) \nequiv{m} \melt.\aginjc(m) } \\
\mcore\melt \eqdef{}& \melt \\
\melt \mtimes \meltB \eqdef{}& (\melt.\aginjc, \setComp{n}{n \in \melt.\aginjV \land n \in \meltB.\aginjV \land \melt \nequiv{n} \meltB })
\end{align*}
Note that the carrier $\agm(\cofe)$ is a \emph{record} consisting of the two fields $\aginjc$ and $\aginjV$.
$\agm(-)$ is a locally non-expansive functor from $\COFEs$ to $\CMRAs$.
You can think of the $\aginjc$ as a \emph{chain} of elements of $\cofe$ that has to converge only for $n \in \aginjV$ steps.
......@@ -124,6 +131,7 @@ Given some CMRA $\monoid$, we define $\oneshotm(\monoid)$ as follows:
\munit \mtimes \ospending \eqdef{}& \ospending \mtimes \munit \eqdef \ospending \\
\munit \mtimes \osshot(\melt) \eqdef{}& \osshot(\melt) \mtimes \munit \eqdef \osshot(\melt)
\end{align*}%
Notice that $\oneshotm(\monoid)$ is a disjoint sum with the four constructors (injections) $\ospending$, $\osshot$, $\munit$ and $\bot$.
The remaining cases of composition go to $\bot$.
\begin{align*}
\mcore{\ospending} \eqdef{}& \munit & \mcore{\osshot(\melt)} \eqdef{}& \mcore\melt \\
......
......@@ -112,6 +112,8 @@
%% Some commonly used identifiers
\newcommand{\op}{\textrm{op}}
\newcommand{\SProp}{\textdom{SProp}}
\newcommand{\UPred}{\textdom{UPred}}
\newcommand{\mProp}{\textdom{Prop}} % meta-level prop
......
......@@ -141,9 +141,10 @@ Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable
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$.
\ralf{$\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} assertions about propositions, defined as follows:
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 \]
......@@ -631,7 +632,7 @@ Furthermore, the following adequacy statement shows that our weakest preconditio
\\&( \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')
\\&\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.
......
......@@ -53,19 +53,19 @@ For every definition, we have to show all the side-conditions: The maps have to
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:
\begin{align*}
\textdom{ResF}(\cofe) \eqdef{}& \record{\wld: \agm(\latert \cofe), \pres: \exm(\textdom{State}), \ghostRes: F(\cofe)}
\textdom{ResF}(\cofe^\op, \cofe) \eqdef{}& \record{\wld: \agm(\latert \cofe), \pres: \exm(\textdom{State}), \ghostRes: \iFunc(\cofe^\op, \cofe)}
\end{align*}
where $F$ is the user-chosen bifunctor from $\COFEs$ to $\CMRAs$.
$\textdom{ResF}(\cofe)$ is a CMRA by lifting the individual CMRAs pointwise.
Furthermore, if $F$ is locally contractive, then so is $\textdom{ResF}(-)$.
Remember that $\iFunc$ is the user-chosen bifunctor from $\COFEs$ to $\CMRAs$.
$\textdom{ResF}(\cofe^\op, \cofe)$ is a CMRA by lifting the individual CMRAs pointwise.
Furthermore, if $F$ is locally contractive, then so is $\textdom{ResF}$.
Now we can write down the recursive domain equation:
\[ \iPreProp \cong \UPred(\textdom{ResF}(\iPreProp)) \]
\[ \iPreProp \cong \UPred(\textdom{ResF}(\iPreProp, \iPreProp)) \]
$\iPreProp$ is a COFE, which exists 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
\begin{align*}
\Res &\eqdef \textdom{ResF}(\iPreProp) \\
\Res &\eqdef \textdom{ResF}(\iPreProp, \iPreProp) \\
\iProp &\eqdef \UPred(\Res) \\
\wIso &: \iProp \nfn \iPreProp \\
\wIso^{-1} &: \iPreProp \nfn \iProp
......@@ -77,7 +77,7 @@ We then pick $\iProp$ as the interpretation of $\Prop$:
\paragraph{Interpretation of assertions.}
$\iProp$ is a $\UPred$, and hence the definitions from \Sref{sec:upred-logic} apply.
We only have to define the missing connectives, the most interesting bits being primitive view shifts and weakest preconditions.
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
......@@ -87,7 +87,7 @@ We only have to define the missing connectives, the most interesting bits being
\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. \rs.\wld(\iname) \nequiv{n+1} \aginj(\latertinj(\wIso(\prop))) \Ra n \in \prop(\rss(\iname))
\All\iname \in \mask, \prop. (\rs.\wld)(\iname) \nequiv{n+1} \aginj(\latertinj(\wIso(\prop))) \Ra n \in \prop(\rss(\iname))
\end{inbox}\\
\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))}
\end{align*}
......@@ -106,9 +106,9 @@ $\textdom{wp}$ is defined as the fixed-point of a contractive function.
\begin{align*}
\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 \prop(\rs') \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs' \mtimes \rs_\f}) \land {}\\
&(\All\val. \toval(\expr) = \val \Ra \Exists \rsB. m+1 \in \pred(\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}{\rs' \mtimes \rs_\f} \land m \in \textdom{wp}(\mask, \expr_2, \pred)(\rsB_1) \land {}&\\
&\qquad \Exists \rsB_1, \rsB_2. m \in \wsat\state{\mask \cup \mask_\f}{\rsB \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)
......@@ -117,10 +117,12 @@ $\textdom{wp}$ is defined as the fixed-point of a contractive function.
\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*}
\Sem{\vctx \proves \knowInv{\iname}{\prop} : \Prop}_\gamma &\eqdef \ownM{[\iname \mapsto \aginj(\latertinj(\wIso(\prop)))], \munit, \munit} \\
\Sem{\vctx \proves \ownGGhost{\melt} : \Prop}_\gamma &\eqdef \ownM{\munit, \munit, \melt} \\
\Sem{\vctx \proves \ownPhys{\state} : \Prop}_\gamma &\eqdef \ownM{\munit, \exinj(\state), \munit} \\
\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
......@@ -149,9 +151,7 @@ The remaining domains are interpreted as follows:
\Sem{\type \to \type'} &\eqdef& \Sem{\type} \nfn \Sem{\type} \\
\end{array}
\]
The balance of our signature $\Sig$ is interpreted as follows.
For each base type $\type$ not covered by the preceding table, we pick an object $X_\type$ in $\cal U$ and define
For the remaining base types $\type$ defined by the signature $\Sig$, we pick an object $X_\type$ in $\cal U$ and define
\[
\Sem{\type} \eqdef X_\type
\]
......
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