Forked from
Iris / Iris
4487 commits behind the upstream repository.
constructions.tex 16.65 KiB
\section{OFE and COFE Constructions}
\subsection{Trivial Pointwise Lifting}
The (C)OFE structure on many types can be easily obtained by pointwise lifting of the structure of the components.
This is what we do for option $\maybe\cofe$, product $(M_i)_{i \in I}$ (with $I$ some finite index set), sum $\cofe + \cofe'$ and finite partial functions $K \fpfn \monoid$ (with $K$ infinite countable).
\subsection{Next (Type-Level Later)}
Given a OFE $\cofe$, we define $\latert\cofe$ as follows (using a datatype-like notation to define the type):
\begin{align*}
\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 $\OFEs$ to $\OFEs$.
\subsection{Uniform Predicates}
Given a camera $\monoid$, we define the COFE $\UPred(\monoid)$ of \emph{uniform predicates} over $\monoid$ as follows:
\begin{align*}
\monoid \monnra \SProp \eqdef{}& \setComp{\pred: \monoid \nfn \SProp}
{\All n, \melt, \meltB. \melt \mincl[n] \meltB \Ra \pred(\melt) \nincl{n} \pred(\meltB)} \\
\UPred(\monoid) \eqdef{}& \faktor{\monoid \monnra \SProp}{\equiv} \\
\pred \equiv \predB \eqdef{}& \All m, \melt. m \in \mval(\melt) \Ra (m \in \pred(\melt) \iff m \in \predB(\melt)) \\
\pred \nequiv{n} \predB \eqdef{}& \All m \le n, \melt. m \in \mval(\melt) \Ra (m \in \pred(\melt) \iff m \in \predB(\melt))
\end{align*}
You can think of uniform predicates as monotone, step-indexed predicates over a camera that ``ignore'' invalid elements (as defined by the quotient).
$\UPred(-)$ is a locally non-expansive functor from $\CMRAs$ to $\COFEs$.
It is worth noting that the above quotient admits canonical
representatives. More precisely, one can show that every
equivalence class contains exactly one element $P_0$ such that:
\begin{align*}
\All n, \melt. (\mval(\melt) \nincl{n} P_0(\melt)) \Ra n \in P_0(\melt) \tagH{UPred-canonical}
\end{align*}
Intuitively, this says that $P_0$ trivially holds whenever the resource is invalid.
Starting from any element $P$, one can find this canonical
representative by choosing $P_0(\melt) := \setComp{n}{n \in \mval(\melt) \Ra n \in P(\melt)}$.
Hence, as an alternative definition of $\UPred$, we could use the set
of canonical representatives. This alternative definition would
save us from using a quotient. However, the definitions of the various
connectives would get more complicated, because we have to make sure
they all verify \ruleref{UPred-canonical}, which sometimes requires some adjustments. We
would moreover need to prove one more property for every logical
connective.
\clearpage
\section{RA and Camera Constructions}
\subsection{Product}
\label{sec:prodm}
Given a family $(M_i)_{i \in I}$ of cameras ($I$ finite), we construct a camera for the product $\prod_{i \in I} M_i$ by lifting everything pointwise.
Frame-preserving updates on the $M_i$ lift to the product:
\begin{mathpar}
\inferH{prod-update}
{\melt \mupd_{M_i} \meltsB}
{\mapinsert i \melt f \mupd \setComp{ \mapinsert i \meltB f}{\meltB \in \meltsB}}
\end{mathpar}
\subsection{Sum}
\label{sec:summ}
The \emph{sum camera} $\monoid_1 \csumm \monoid_2$ for any cameras $\monoid_1$ and $\monoid_2$ is defined as (again, we use a datatype-like notation):
\begin{align*}
\monoid_1 \csumm \monoid_2 \eqdef{}& \cinl(\melt_1:\monoid_1) \mid \cinr(\melt_2:\monoid_2) \mid \mundef \\
\mval(\mundef) \eqdef{}& \emptyset \\
\mval(\cinl(\melt)) \eqdef{}& \mval_1(\melt) \\
\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*}
Above, $\mval_1$ refers to the validity of $\monoid_1$.
The validity, composition and core for $\cinr$ are defined symmetrically.
The remaining cases of the composition and core are all $\mundef$.
Notice that we added the artificial ``invalid'' (or ``undefined'') element $\mundef$ to this camera just in order to make certain compositions of elements (in this case, $\cinl$ and $\cinr$) invalid.
The step-indexed equivalence is inductively defined as follows:
\begin{mathpar}
\infer{x \nequiv{n} y}{\cinl(x) \nequiv{n} \cinl(y)}
\infer{x \nequiv{n} y}{\cinr(x) \nequiv{n} \cinr(y)}
\axiom{\mundef \nequiv{n} \mundef}
\end{mathpar}
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 \in M, n. n \notin \mval(\melt \mtimes \melt_\f) \and \mvalFull(\meltB)}
{\cinl(\melt) \mupd \cinr(\meltB)}
\end{mathpar}
Crucially, the second rule allows us to \emph{swap} the ``side'' of the sum that the camera is on if $\mval$ has \emph{no possible frame}.
\subsection{Option}
The definition of the camera/RA axioms already lifted the composition operation on $\monoid$ to one on $\maybe\monoid$.
We can easily extend this to a full camera by defining a suitable core, namely
\begin{align*}
\mcore{\mnocore} \eqdef{}& \mnocore & \\
\mcore{\maybe\melt} \eqdef{}& \mcore\melt & \text{If $\maybe\melt \neq \mnocore$}
\end{align*}
Notice that this core is total, as the result always lies in $\maybe\monoid$ (rather than in $\maybe{\mathord{\maybe\monoid}}$).
\subsection{Finite Partial Functions}
\label{sec:fpfnm}
Given some infinite countable $K$ and some camera $\monoid$, the set of finite partial functions $K \fpfn \monoid$ is equipped with a camera structure by lifting everything pointwise.
We obtain the following frame-preserving updates:
\begin{mathpar}
\inferH{fpfn-alloc-strong}
{\text{$G$ infinite} \and \mvalFull(\melt)}
{\emptyset \mupd \setComp{\mapsingleton \gname \melt}{\gname \in G}}
\inferH{fpfn-alloc}
{\mvalFull(\melt)}
{\emptyset \mupd \setComp{\mapsingleton \gname \melt}{\gname \in K}}
\inferH{fpfn-update}
{\melt \mupd_\monoid \meltsB}
{\mapinsert i \melt f] \mupd \setComp{ \mapinsert i \meltB f}{\meltB \in \meltsB}}
\end{mathpar}
Above, $\mvalFull$ refers to the (full) validity of $\monoid$.
$K \fpfn (-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$.
\subsection{Agreement}
Given some OFE $\cofe$, we define the camera $\agm(\cofe)$ as follows:
\begin{align*}
\agm(\cofe) \eqdef{}& \setComp{\melt \in \finpset\cofe}{\melt \neq \emptyset} /\ {\sim} \\[-0.2em]
\melt \nequiv{n} \meltB \eqdef{}& (\All x \in \melt. \Exists y \in \meltB. x \nequiv{n} y) \land (\All y \in \meltB. \Exists x \in \melt. x \nequiv{n} y) \\
\textnormal{where }& \melt \sim \meltB \eqdef{} \All n. \melt \nequiv{n} \meltB \\
~\\
% \All n \in {\melt.V}.\, \melt.x \nequiv{n} \meltB.x \\
\mval(\melt) \eqdef{}& \setComp{n}{ \All x, y \in \melt. x \nequiv{n} y } \\
\mcore\melt \eqdef{}& \melt \\
\melt \mtimes \meltB \eqdef{}& \melt \cup \meltB
\end{align*}
%Note that the carrier $\agm(\cofe)$ is a \emph{record} consisting of the two fields $c$ and $V$.
$\agm(-)$ is a locally non-expansive functor from $\OFEs$ to $\CMRAs$.
We define a non-expansive injection $\aginj$ into $\agm(\cofe)$ as follows:
\[ \aginj(x) \eqdef \set{x} \]
There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can show the following:
\begin{mathpar}
\axiomH{ag-val}{\mvalFull(\aginj(x))}
\axiomH{ag-dup}{\aginj(x) = \aginj(x)\mtimes\aginj(x)}
\axiomH{ag-agree}{n \in \mval(\aginj(x) \mtimes \aginj(y)) \Ra x \nequiv{n} y}
\end{mathpar}
\subsection{Exclusive Camera}
Given an OFE $\cofe$, we define a camera $\exm(\cofe)$ such that at most one $x \in \cofe$ can be owned:
\begin{align*}
\exm(\cofe) \eqdef{}& \exinj(\cofe) \mid \mundef \\
\mval(\melt) \eqdef{}& \setComp{n}{\melt \notnequiv{n} \mundef}
\end{align*}
All cases of composition go to $\mundef$.
\begin{align*}
\mcore{\exinj(x)} \eqdef{}& \mnocore &
\mcore{\mundef} \eqdef{}& \mundef
\end{align*}
Remember that $\mnocore$ is the ``dummy'' element in $\maybe\monoid$ indicating (in this case) that $\exinj(x)$ has no core.
The step-indexed equivalence is inductively defined as follows:
\begin{mathpar}
\infer{x \nequiv{n} y}{\exinj(x) \nequiv{n} \exinj(y)}
\axiom{\mundef \nequiv{n} \mundef}
\end{mathpar}
$\exm(-)$ is a locally non-expansive functor from $\OFEs$ to $\CMRAs$.
We obtain the following frame-preserving update:
\begin{mathpar}
\inferH{ex-update}{}
{\exinj(x) \mupd \exinj(y)}
\end{mathpar}
\subsection{Fractions}
We define an RA structure on the rational numbers in $(0, 1]$ as follows:
\begin{align*}
\fracm \eqdef{}& \fracinj(\mathbb{Q} \cap (0, 1]) \mid \mundef \\
\mvalFull(\melt) \eqdef{}& \melt \neq \mundef \\
\fracinj(q_1) \mtimes \fracinj(q_2) \eqdef{}& \fracinj(q_1 + q_2) \quad \text{if $q_1 + q_2 \leq 1$} \\
\mcore{\fracinj(x)} \eqdef{}& \bot \\
\mcore{\mundef} \eqdef{}& \mundef
\end{align*}
All remaining cases of composition go to $\mundef$.
Frequently, we will write just $x$ instead of $\fracinj(x)$.
The most important property of this RA is that $1$ has no frame.
This is useful in combination with \ruleref{sum-swap}, and also when used with pairs:
\begin{mathpar}
\inferH{pair-frac-change}{}
{(1, a) \mupd (1, b)}
\end{mathpar}
%TODO: These need syncing with Coq
% \subsection{Finite Powerset Monoid}
% Given an infinite set $X$, we define a monoid $\textmon{PowFin}$ with carrier $\mathcal{P}^{\textrm{fin}}(X)$ as follows:
% \[
% \melt \cdot \meltB \;\eqdef\; \melt \cup \meltB \quad \mbox{if } \melt \cap \meltB = \emptyset
% \]
% We obtain:
% \begin{mathpar}
% \inferH{PowFinUpd}{}
% {\emptyset \mupd \{ \{x\} \mid x \in X \}}
% \end{mathpar}
% \begin{proof}[Proof of \ruleref{PowFinUpd}]
% Assume some frame $\melt_\f \sep \emptyset$. Since $\melt_\f$ is finite and $X$ is infinite, there exists an $x \notin \melt_\f$.
% Pick that for the result.
% \end{proof}
% The powerset monoids is cancellative.
% \begin{proof}[Proof of cancellativity]
% Let $\melt_\f \mtimes \melt = \melt_\f \mtimes \meltB \neq \mzero$.
% So we have $\melt_\f \sep \melt$ and $\melt_\f \sep \meltB$, and we have to show $\melt = \meltB$.
% Assume $x \in \melt$. Hence $x \in \melt_\f \mtimes \melt$ and thus $x \in \melt_\f \mtimes \meltB$.
% By disjointness, $x \notin \melt_\f$ and hence $x \in meltB$.
% The other direction works the same way.
% \end{proof}
\subsection{Authoritative}
\label{sec:auth-camera}
Given a camera $M$, we construct $\authm(M)$ modeling someone owning an \emph{authoritative} element $\melt$ of $M$, and others potentially owning fragments $\meltB \mincl \melt$ of $\melt$.
We assume that $M$ has a unit $\munit$, and hence its core is total.
(If $M$ is an exclusive monoid, the construction is very similar to a half-ownership monoid with two asymmetric halves.)
\begin{align*}
\authm(M) \eqdef{}& \maybe{\exm(M)} \times M \\
\mval( (x, \meltB ) ) \eqdef{}& \setComp{ n }{ n \in \mval(\meltB) \land (x = \mnocore \lor \Exists \melt. x = \exinj(\melt) \land \meltB \mincl_n \melt) } \\
(x_1, \meltB_1) \mtimes (x_2, \meltB_2) \eqdef{}& (x_1 \mtimes x_2, \meltB_2 \mtimes \meltB_2) \\
\mcore{(x, \meltB)} \eqdef{}& (\mnocore, \mcore\meltB) \\
(x_1, \meltB_1) \nequiv{n} (x_2, \meltB_2) \eqdef{}& x_1 \nequiv{n} x_2 \land \meltB_1 \nequiv{n} \meltB_2
\end{align*}
Note that $(\mnocore, \munit)$ is the unit and asserts no ownership whatsoever, but $(\exinj(\munit), \munit)$ asserts that the authoritative element is $\munit$.
Let $\melt, \meltB \in M$.
We write $\authfull \melt$ for full ownership $(\exinj(\melt), \munit)$ and $\authfrag \meltB$ for fragmental ownership $(\mnocore, \meltB)$ and $\authfull \melt , \authfrag \meltB$ for combined ownership $(\exinj(\melt), \meltB)$.
The frame-preserving update involves the notion of a \emph{local update}:
\newcommand\lupd{\stackrel{\mathrm l}{\mupd}}
\begin{defn}
It is possible to do a \emph{local update} from $\melt_1$ and $\meltB_1$ to $\melt_2$ and $\meltB_2$, written $(\melt_1, \meltB_1) \lupd (\melt_2, \meltB_2)$, if
\[ \All n, \maybe{\melt_\f}. n \in \mval(\melt_1) \land \melt_1 \nequiv{n} \meltB_1 \mtimes \maybe{\melt_\f} \Ra n \in \mval(\melt_2) \land \melt_2 \nequiv{n} \meltB_2 \mtimes \maybe{\melt_\f} \]
\end{defn}
In other words, the idea is that for every possible frame $\maybe{\melt_\f}$ completing $\meltB_1$ to $\melt_1$, the same frame also completes $\meltB_2$ to $\melt_2$.
We then obtain
\begin{mathpar}
\inferH{auth-update}
{(\melt_1, \meltB_1) \lupd (\melt_2, \meltB_2)}
{\authfull \melt_1 , \authfrag \meltB_1 \mupd \authfull \melt_2 , \authfrag \meltB_2}
\end{mathpar}
\subsection{STS with Tokens}
\label{sec:sts-camera}
Given a state-transition system~(STS, \ie a directed graph) $(\STSS, {\stsstep} \subseteq \STSS \times \STSS)$, a set of tokens $\STST$, and a labeling $\STSL: \STSS \ra \wp(\STST)$ of \emph{protocol-owned} tokens for each state, we construct an RA modeling an authoritative current state and permitting transitions given a \emph{bound} on the current state and a set of \emph{locally-owned} tokens.
The construction follows the idea of STSs as described in CaReSL \cite{caresl}.
We first lift the transition relation to $\STSS \times \wp(\STST)$ (implementing a \emph{law of token conservation}) and define a stepping relation for the \emph{frame} of a given token set:
\begin{align*}
(s, T) \stsstep (s', T') \eqdef{}& s \stsstep s' \land \STSL(s) \uplus T = \STSL(s') \uplus T' \\
s \stsfstep{T} s' \eqdef{}& \Exists T_1, T_2. T_1 \disj \STSL(s) \cup T \land (s, T_1) \stsstep (s', T_2)
\end{align*}
We further define \emph{closed} sets of states (given a particular set of tokens) as well as the \emph{closure} of a set:
\begin{align*}
\STSclsd(S, T) \eqdef{}& \All s \in S. \STSL(s) \disj T \land \left(\All s'. s \stsfstep{T} s' \Ra s' \in S\right) \\
\upclose(S, T) \eqdef{}& \setComp{ s' \in \STSS}{\Exists s \in S. s \stsftrans{T} s' }
\end{align*}
The STS RA is defined as follows
\begin{align*}
\monoid \eqdef{}& \STSauth(s:\STSS, T:\wp(\STST) \mid \STSL(s) \disj T) \mid{}\\& \STSfrag(S: \wp(\STSS), T: \wp(\STST) \mid \STSclsd(S, T) \land S \neq \emptyset) \mid \mundef \\
\mvalFull(\melt) \eqdef{}& \melt \neq \mundef \\
\STSfrag(S_1, T_1) \mtimes \STSfrag(S_2, T_2) \eqdef{}& \STSfrag(S_1 \cap S_2, T_1 \cup T_2) \qquad\qquad\qquad \text{if $T_1 \disj T_2$ and $S_1 \cap S_2 \neq \emptyset$} \\
\STSfrag(S, T) \mtimes \STSauth(s, T') \eqdef{}& \STSauth(s, T') \mtimes \STSfrag(S, T) \eqdef \STSauth(s, T \cup T') \qquad \text{if $T \disj T'$ and $s \in S$} \\
\mcore{\STSfrag(S, T)} \eqdef{}& \STSfrag(\upclose(S, \emptyset), \emptyset) \\
\mcore{\STSauth(s, T)} \eqdef{}& \STSfrag(\upclose(\set{s}, \emptyset), \emptyset)
\end{align*}
The remaining cases are all $\mundef$.
We will need the following frame-preserving update:
\begin{mathpar}
\inferH{sts-step}{(s, T) \ststrans (s', T')}
{\STSauth(s, T) \mupd \STSauth(s', T')}
\inferH{sts-weaken}
{\STSclsd(S_2, T_2) \and S_1 \subseteq S_2 \and T_2 \subseteq T_1}
{\STSfrag(S_1, T_1) \mupd \STSfrag(S_2, T_2)}
\end{mathpar}
\paragraph{The core is not a homomorphism.}
The core of the STS construction is only satisfying the RA axioms because we are \emph{not} demanding the core to be a homomorphism---all we demand is for the core to be monotone with respect the \ruleref{ra-incl}.
In other words, the following does \emph{not} hold for the STS core as defined above:
\[ \mcore\melt \mtimes \mcore\meltB = \mcore{\melt\mtimes\meltB} \]
To see why, consider the following STS:
\newcommand\st{\textlog{s}}
\newcommand\tok{\textmon{t}}
\begin{center}
\begin{tikzpicture}[sts]
\node at (0,0) (s1) {$\st_1$};
\node at (3,0) (s2) {$\st_2$};
\node at (9,0) (s3) {$\st_3$};
\node at (6,0) (s4) {$\st_4$\\$[\tok_1, \tok_2]$};
\path[sts_arrows] (s2) edge (s4);
\path[sts_arrows] (s3) edge (s4);
\end{tikzpicture}
\end{center}
Now consider the following two elements of the STS RA:
\[ \melt \eqdef \STSfrag(\set{\st_1,\st_2}, \set{\tok_1}) \qquad\qquad
\meltB \eqdef \STSfrag(\set{\st_1,\st_3}, \set{\tok_2}) \]
We have:
\begin{mathpar}
{\melt\mtimes\meltB = \STSfrag(\set{\st_1}, \set{\tok_1, \tok_2})}
{\mcore\melt = \STSfrag(\set{\st_1, \st_2, \st_4}, \emptyset)}
{\mcore\meltB = \STSfrag(\set{\st_1, \st_3, \st_4}, \emptyset)}
{\mcore\melt \mtimes \mcore\meltB = \STSfrag(\set{\st_1, \st_4}, \emptyset) \neq
\mcore{\melt \mtimes \meltB} = \STSfrag(\set{\st_1}, \emptyset)}
\end{mathpar}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
%%% End: