Commit 5d8b2eb6 authored by Ralf Jung's avatar Ralf Jung

docs: apply some feedback from Ales

parent df918d8b
......@@ -278,10 +278,10 @@ Furthermore, we derive some forms that directly involve view shifts and Hoare tr
\subsection{Global functor and ghost ownership}
Hereinafter we assume the global CMRA functor (served up as a parameter to Iris) is obtained from a family of functors $(F_i)_{i \in I}$ for some finite $I$ by picking
\[ F(\cofe) \eqdef \prod_{i \in I} \textlog{GhName} \fpfn F_i(\cofe) \]
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 F_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 $\ownGGhost{[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.
......
......@@ -58,6 +58,7 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
\clearpage
\section{Logic}
\label{sec:logic}
To instantiate Iris, you need to define the following parameters:
\begin{itemize}
......
......@@ -52,9 +52,11 @@ 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^\op, \cofe) \eqdef{}& \record{\wld: \mathbb{N} \fpfn \agm(\latert \cofe), \pres: \exm(\textdom{State}), \ghostRes: \iFunc(\cofe^\op, \cofe)}
\textdom{ResF}(\cofe^\op, \cofe) \eqdef{}& \record{\wld: \mathbb{N} \fpfn \agm(\latert \cofe), \pres: \maybe{\exm(\textdom{State})}, \ghostRes: \iFunc(\cofe^\op, \cofe)}
\end{align*}
Remember that $\iFunc$ is the user-chosen bifunctor from $\COFEs$ to $\CMRAs$.
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, if $F$ is locally contractive, then so is $\textdom{ResF}$.
......
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