From 5d8b2eb6ce7c84cc745a13ba6f7b2012025b6279 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 27 Jul 2016 17:55:11 +0200
Subject: [PATCH] docs: apply some feedback from Ales
---
docs/derived.tex | 6 +++---
docs/logic.tex | 1 +
docs/model.tex | 6 ++++--
3 files changed, 8 insertions(+), 5 deletions(-)
diff --git a/docs/derived.tex b/docs/derived.tex
index 8fa3c08cd..89d0f082e 100644
--- a/docs/derived.tex
+++ b/docs/derived.tex
@@ -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.
diff --git a/docs/logic.tex b/docs/logic.tex
index 5d62e467e..d36424c5c 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -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}
diff --git a/docs/model.tex b/docs/model.tex
index f6ce77818..6f5f76555 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -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}$.
--
GitLab