From 06aedc30ccc821226e3a01f95444e4e702f04e5c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 25 Jul 2016 20:48:47 +0200
Subject: [PATCH] docs: update CMRA constructions for partial core
---
CHANGELOG.md | 2 ++
docs/algebra.tex | 9 +++--
docs/constructions.tex | 79 ++++++++++++++++++------------------------
docs/iris.sty | 1 +
docs/logic.tex | 23 +++++-------
5 files changed, 48 insertions(+), 66 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index be6bccf5e..3853fde16 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -12,6 +12,8 @@ This version accompanies the final ICFP paper.
carry a proof of closedness. Substitution, closedness and value-ness proofs
are performed by computation after reflecting into a term langauge that knows
about values and closed expressions.
+* [program_logic/language] The language does not define its own "atomic"
+ predicate. Instead, atomicity is defined as reducing in one step to a value.
## Iris 2.0-rc1
diff --git a/docs/algebra.tex b/docs/algebra.tex
index 2bbc6a487..c22f0baa7 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -61,7 +61,6 @@ The function space $(-) \nfn (-)$ is a locally non-expansive bifunctor.
Note that the composition of non-expansive (bi)functors is non-expansive, and the composition of a non-expansive and a contractive (bi)functor is contractive.
\subsection{RA}
-\newcommand\dummymelt\bot
\begin{defn}
A \emph{resource algebra} (RA) is a tuple \\
@@ -75,7 +74,7 @@ Note that the composition of non-expansive (bi)functors is non-expansive, and th
\All \melt, \meltB.& \mcore\melt \in \monoid \land \melt \mincl \meltB \Ra \mcore\meltB \in \monoid \land \mcore\melt \mincl \mcore\meltB \tagH{ra-core-mono} \\
\All \melt, \meltB.& (\melt \mtimes \meltB) \in \mval \Ra \melt \in \mval \tagH{ra-valid-op} \\
\text{where}\qquad %\qquad\\
- \maybe\monoid \eqdef{}& \monoid \uplus \set{\dummymelt} \qquad\qquad\qquad \melt^? \mtimes \dummymelt \eqdef \dummymelt \mtimes \melt^? \eqdef \melt^? \\
+ \maybe\monoid \eqdef{}& \monoid \uplus \set{\mnocore} \qquad\qquad\qquad \melt^? \mtimes \mnocore \eqdef \mnocore \mtimes \melt^? \eqdef \melt^? \\
\melt \mincl \meltB \eqdef{}& \Exists \meltC \in \monoid. \meltB = \melt \mtimes \meltC \tagH{ra-incl}
\end{align*}
\end{defn}
@@ -90,7 +89,7 @@ This take on partiality is necessary when defining the structure of \emph{higher
for an arbitrary number of units, via a function $\mcore{{-}}$ assigning to an element $\melt$ its \emph{(duplicable) core} $\mcore\melt$, as demanded by \ruleref{ra-core-id}.
We further demand that $\mcore{{-}}$ is idempotent (\ruleref{ra-core-idem}) and monotone (\ruleref{ra-core-mono}) with respect to the \emph{extension order}, defined similarly to that for PCMs (\ruleref{ra-incl}).
- Notice that the domain of the core is $\maybe\monoid$, a set that adds a dummy element $\dummymelt$ to $\monoid$.
+ Notice that the domain of the core is $\maybe\monoid$, a set that adds a dummy element $\mnocore$ to $\monoid$.
% (This corresponds to the option type.)
Thus, the core can be \emph{partial}: not all elements need to have a unit.
We use the metavariable $\maybe\melt$ to indicate elements of $\maybe\monoid$.
@@ -108,7 +107,7 @@ Notice also that the core of an RA is a strict generalization of the unit that a
We further define $\melt \mupd \meltB \eqdef \melt \mupd \set\meltB$.
\end{defn}
The assertion $\melt \mupd \meltsB$ says that every element $\maybe{\melt_\f}$ compatible with $\melt$ (we also call such elements \emph{frames}), must also be compatible with some $\meltB \in \meltsB$.
-Notice that $\maybe{\melt_\f}$ could be $\dummymelt$, so the frame-preserving update can also be applied to elements that have \emph{no} frame.
+Notice that $\maybe{\melt_\f}$ could be $\mnocore$, so the frame-preserving update can also be applied to elements that have \emph{no} frame.
Intuitively, this means that whatever assumptions the rest of the program is making about the state of $\gname$, if these assumptions are compatible with $\melt$, then updating to $\meltB$ will not invalidate any of these assumptions.
Since Iris ensures that the global ghost state is valid, this means that we can soundly update the ghost state from $\melt$ to a non-deterministically picked $\meltB \in \meltsB$.
@@ -173,7 +172,7 @@ This operation is needed to prove that $\later$ commutes with separating conjunc
\end{enumerate}
\end{defn}
-\begin{lem}
+\begin{lem}\label{lem:cmra-unit-total-core}
If $\monoid$ has a unit $\munit$, then the core $\mcore{{-}}$ is total, \ie $\All\melt. \mcore\melt \in \monoid$.
\end{lem}
diff --git a/docs/constructions.tex b/docs/constructions.tex
index 03e331a13..cf4114d7b 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -59,6 +59,35 @@ Frame-preserving updates on the $M_i$ lift to the product:
{f[i \mapsto \melt] \mupd \setComp{ f[i \mapsto \meltB]}{\meltB \in \meltsB}}
\end{mathpar}
+\subsection{Sum}
+\label{sec:summ}
+
+The \emph{sum CMRA} $\monoid_1 \csumm \monoid_2$ for any CMRAs $\monoid_1$ and $\monoid_2$ is defined as:
+\begin{align*}
+ \monoid_1 \csumm \monoid_2 \eqdef{}& \cinl(\melt_1:\monoid_1) \mid \cinr(\melt_2:\monoid_2) \mid \bot \\
+ \mval_n \eqdef{}& \setComp{\cinl(\melt_1)\!}{\!\melt_1 \in \mval'_n}
+ \cup \setComp{\cinr(\melt_2)\!}{\!\melt_2 \in \mval''_n} \\
+ \cinl(\melt_1) \mtimes \cinl(\meltB_1) \eqdef{}& \cinl(\melt_1 \mtimes \meltB_1) \\
+% \munit \mtimes \ospending \eqdef{}& \ospending \mtimes \munit \eqdef \ospending \\
+% \munit \mtimes \osshot(\melt) \eqdef{}& \osshot(\melt) \mtimes \munit \eqdef \osshot(\melt) \\
+ \mcore{\cinl(\melt_1)} \eqdef{}& \begin{cases}\mnocore & \text{if $\mcore{\melt_1} = \mnocore$} \\ \cinl({\mcore{\melt_1}}) & \text{otherwise} \end{cases}
+\end{align*}
+The composition and core for $\cinr$ are defined symmetrically.
+The remaining cases of the composition and core are all $\bot$.
+Above, $\mval'$ refers to the validity of $\monoid_1$, and $\mval''$ to the validity of $\monoid_2$.
+
+We obtain the following frame-preserving updates, as well as their symmetric counterparts:
+\begin{mathpar}
+ \inferH{sum-update}
+ {\melt \mupd_{M_1} \meltsB}
+ {\cinl(\melt) \mupd \setComp{ \cinl(\meltB)}{\meltB \in \meltsB}}
+
+ \inferH{sum-swap}
+ {\All \melt_\f, n. \melt \mtimes \melt_\f \notin \mval'_n \and \meltB \in \mval''}
+ {\cinl(\melt) \mupd \cinr(\meltB)}
+\end{mathpar}
+Crucially, the second rule allows us to \emph{swap} the ``side'' of the sum that the CMRA is on if $\mval$ has \emph{no possible frame}.
+
\subsection{Finite partial function}
\label{sec:fpfnm}
@@ -118,59 +147,17 @@ There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can
\axiomH{ag-agree}{\aginj(x) \mtimes \aginj(y) \in \mval_n \Ra x \nequiv{n} y}
\end{mathpar}
-\subsection{One-shot}
-
-The purpose of the one-shot CMRA is to lazily initialize the state of a ghost location.
-Given some CMRA $\monoid$, we define $\oneshotm(\monoid)$ as follows:
-\begin{align*}
- \oneshotm(\monoid) \eqdef{}& \ospending + \osshot(\monoid) + \munit + \bot \\
- \mval_n \eqdef{}& \set{\ospending, \munit} \cup \setComp{\osshot(\melt)}{\melt \in \mval_n}
-\\%\end{align*}
-%\begin{align*}
- \osshot(\melt) \mtimes \osshot(\meltB) \eqdef{}& \osshot(\melt \mtimes \meltB) \\
- \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 \\
- \mcore{\munit} \eqdef{}& \munit & \mcore{\bot} \eqdef{}& \bot
-\end{align*}
-The step-indexed equivalence is inductively defined as follows:
-\begin{mathpar}
- \axiom{\ospending \nequiv{n} \ospending}
-
- \infer{\melt \nequiv{n} \meltB}{\osshot(\melt) \nequiv{n} \osshot(\meltB)}
-
- \axiom{\munit \nequiv{n} \munit}
-
- \axiom{\bot \nequiv{n} \bot}
-\end{mathpar}
-$\oneshotm(-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$.
-
-We obtain the following frame-preserving updates:
-\begin{mathpar}
- \inferH{oneshot-shoot}
- {\melt \in \mval}
- {\ospending \mupd \osshot(\melt)}
-
- \inferH{oneshot-update}
- {\melt \mupd \meltsB}
- {\osshot(\melt) \mupd \setComp{\osshot(\meltB)}{\meltB \in \meltsB}}
-\end{mathpar}
\subsection{Exclusive CMRA}
Given a cofe $\cofe$, we define a CMRA $\exm(\cofe)$ such that at most one $x \in \cofe$ can be owned:
\begin{align*}
- \exm(\cofe) \eqdef{}& \exinj(\cofe) + \munit + \bot \\
- \mval_n \eqdef{}& \setComp{\melt\in\exm(\cofe)}{\melt \neq \bot} \\
- \munit \mtimes \exinj(x) \eqdef{}& \exinj(x) \mtimes \munit \eqdef \exinj(x)
+ \exm(\cofe) \eqdef{}& \exinj(\cofe) + \bot \\
+ \mval_n \eqdef{}& \setComp{\melt\in\exm(\cofe)}{\melt \neq \bot}
\end{align*}
-The remaining cases of composition go to $\bot$.
+All cases of composition go to $\bot$.
\begin{align*}
- \mcore{\exinj(x)} \eqdef{}& \munit & \mcore{\munit} \eqdef{}& \munit &
+ \mcore{\exinj(x)} \eqdef{}& \mnocore &
\mcore{\bot} \eqdef{}& \bot
\end{align*}
The step-indexed equivalence is inductively defined as follows:
diff --git a/docs/iris.sty b/docs/iris.sty
index fba354f5a..c95c30e23 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -147,6 +147,7 @@
\newcommand{\munit}{\varepsilon}
\newcommand{\mcore}[1]{{\mid}#1{\mid}} % using "|" here makes LaTeX diverge. WTF.
+\newcommand{\mnocore}\top
\newcommand{\mtimes}{\mathbin{\cdot}}
\newcommand{\mupd}{\rightsquigarrow}
diff --git a/docs/logic.tex b/docs/logic.tex
index 24a8ca03a..94b627f16 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -10,18 +10,6 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions}
A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f$ indicates that, when $\expr_1$ reduces to $\expr$, a \emph{new thread} $\expr_\f$ is forked off.
\item All values are stuck:
\[ \expr, \_ \step \_, \_, \_ \Ra \toval(\expr) = \bot \]
-\item There is a predicate defining \emph{atomic} expressions satisfying
-\let\oldcr\cr
-\begin{mathpar}
- {\All\expr. \atomic(\expr) \Ra \toval(\expr) = \bot} \and
- {{
- \begin{inbox}
-\All\expr_1, \state_1, \expr_2, \state_2, \expr_\f. \atomic(\expr_1) \land \expr_1, \state_1 \step \expr_2, \state_2, \expr_\f \Ra {}\\\qquad\qquad\qquad\quad~~ \Exists \val_2. \toval(\expr_2) = \val_2
- \end{inbox}
-}}
-\end{mathpar}
-In other words, atomic expression \emph{reduce in one step to a value}.
-It does not matter whether they fork off an arbitrary expression.
\end{itemize}
\begin{defn}
@@ -29,6 +17,11 @@ It does not matter whether they fork off an arbitrary expression.
\[ \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]
@@ -68,8 +61,8 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
To instantiate Iris, you need to define the following parameters:
\begin{itemize}
-\item A language $\Lang$
-\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
+\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
@@ -141,7 +134,7 @@ 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.}
+%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:
--
GitLab