Commit 0dd40006 authored by Ralf Jung's avatar Ralf Jung

update documentation for the new OFE story

parent 965852ff
Pipeline #3211 passed with stage
in 10 minutes and 40 seconds
\section{Algebraic Structures}
\subsection{COFE}
\subsection{OFE}
The model of Iris lives in the category of \emph{Complete Ordered Families of Equivalences} (COFEs).
The model of Iris lives in the category of \emph{Ordered Families of Equivalences} (OFEs).
This definition varies slightly from the original one in~\cite{catlogic}.
\begin{defn}[Chain]
Given some set $\cofe$ and an indexed family $({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \nat}$ of equivalence relations, a \emph{chain} is a function $c : \nat \to \cofe$ such that $\All n, m. n \leq m \Ra c (m) \nequiv{n} c (n)$.
\end{defn}
\begin{defn}
A \emph{complete ordered family of equivalences} (COFE) is a tuple $(\cofe, ({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \nat}, \lim : \chain(\cofe) \to \cofe)$ satisfying
An \emph{ordered family of equivalences} (OFE) is a tuple $(\ofe, ({\nequiv{n}} \subseteq \ofe \times \ofe)_{n \in \nat})$ satisfying
\begin{align*}
\All n. (\nequiv{n}) ~& \text{is an equivalence relation} \tagH{cofe-equiv} \\
\All n, m.& n \geq m \Ra (\nequiv{n}) \subseteq (\nequiv{m}) \tagH{cofe-mono} \\
\All x, y.& x = y \Lra (\All n. x \nequiv{n} y) \tagH{cofe-limit} \\
\All n, c.& \lim(c) \nequiv{n} c(n) \tagH{cofe-compl}
\All n. (\nequiv{n}) ~& \text{is an equivalence relation} \tagH{ofe-equiv} \\
\All n, m.& n \geq m \Ra (\nequiv{n}) \subseteq (\nequiv{m}) \tagH{ofe-mono} \\
\All x, y.& x = y \Lra (\All n. x \nequiv{n} y) \tagH{ofe-limit}
\end{align*}
\end{defn}
The key intuition behind COFEs is that elements $x$ and $y$ are $n$-equivalent, notation $x \nequiv{n} y$, if they are \emph{equivalent for $n$ steps of computation}, \ie if they cannot be distinguished by a program running for no more than $n$ steps.
In other words, as $n$ increases, $\nequiv{n}$ becomes more and more refined (\ruleref{cofe-mono})---and in the limit, it agrees with plain equality (\ruleref{cofe-limit}).
In order to solve the recursive domain equation in \Sref{sec:model} it is also essential that COFEs are \emph{complete}, \ie that any chain has a limit (\ruleref{cofe-compl}).
The key intuition behind OFEs is that elements $x$ and $y$ are $n$-equivalent, notation $x \nequiv{n} y$, if they are \emph{equivalent for $n$ steps of computation}, \ie if they cannot be distinguished by a program running for no more than $n$ steps.
In other words, as $n$ increases, $\nequiv{n}$ becomes more and more refined (\ruleref{ofe-mono})---and in the limit, it agrees with plain equality (\ruleref{ofe-limit}).
\begin{defn}
An element $x \in \cofe$ of a COFE is called \emph{discrete} if
\[ \All y \in \cofe. x \nequiv{0} y \Ra x = y\]
A COFE $A$ is called \emph{discrete} if all its elements are discrete.
For a set $X$, we write $\Delta X$ for the discrete COFE with $x \nequiv{n} x' \eqdef x = x'$
An element $x \in \ofe$ of an OFE is called \emph{discrete} if
\[ \All y \in \ofe. x \nequiv{0} y \Ra x = y\]
An OFE $A$ is called \emph{discrete} if all its elements are discrete.
For a set $X$, we write $\Delta X$ for the discrete OFE with $x \nequiv{n} x' \eqdef x = x'$
\end{defn}
\begin{defn}
A function $f : \cofe \to \cofeB$ between two COFEs is \emph{non-expansive} (written $f : \cofe \nfn \cofeB$) if
\[\All n, x \in \cofe, y \in \cofe. x \nequiv{n} y \Ra f(x) \nequiv{n} f(y) \]
A function $f : \ofe \to \ofeB$ between two OFEs is \emph{non-expansive} (written $f : \ofe \nfn \ofeB$) if
\[\All n, x \in \ofe, y \in \ofe. x \nequiv{n} y \Ra f(x) \nequiv{n} f(y) \]
It is \emph{contractive} if
\[ \All n, x \in \cofe, y \in \cofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(y) \]
\[ \All n, x \in \ofe, y \in \ofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(y) \]
\end{defn}
Intuitively, applying a non-expansive function to some data will not suddenly introduce differences between seemingly equal data.
Elements that cannot be distinguished by programs within $n$ steps remain indistinguishable after applying $f$.
The reason that contractive functions are interesting is that for every contractive $f : \cofe \to \cofe$ with $\cofe$ inhabited, there exists a \emph{unique} fixed-point $\fix(f)$ such that $\fix(f) = f(\fix(f))$.
\begin{defn}
The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows.
The category $\OFEs$ consists of OFEs as objects, and non-expansive functions as arrows.
\end{defn}
Note that $\COFEs$ is cartesian closed. In particular:
Note that $\OFEs$ is cartesian closed. In particular:
\begin{defn}
Given two COFEs $\cofe$ and $\cofeB$, the set of non-expansive functions $\set{f : \cofe \nfn \cofeB}$ is itself a COFE with
Given two OFEs $\ofe$ and $\ofeB$, the set of non-expansive functions $\set{f : \ofe \nfn \ofeB}$ is itself an OFE with
\begin{align*}
f \nequiv{n} g \eqdef{}& \All x \in \cofe. f(x) \nequiv{n} g(x)
f \nequiv{n} g \eqdef{}& \All x \in \ofe. f(x) \nequiv{n} g(x)
\end{align*}
\end{defn}
\begin{defn}
A (bi)functor $F : \COFEs \to \COFEs$ is called \emph{locally non-expansive} if its action $F_1$ on arrows is itself a non-expansive map.
A (bi)functor $F : \OFEs \to \OFEs$ is called \emph{locally non-expansive} if its action $F_1$ on arrows is itself a non-expansive map.
Similarly, $F$ is called \emph{locally contractive} if $F_1$ is a contractive map.
\end{defn}
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.
The reason contractive (bi)functors are interesting is that by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}, they have a unique\footnote{Uniqueness is not proven in Coq.} fixed-point.
\subsection{COFE}
COFEs are \emph{complete OFEs}, which means that we can take limits of arbitrary chains.
\begin{defn}[Chain]
Given some set $\cofe$ and an indexed family $({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \nat}$ of equivalence relations, a \emph{chain} is a function $c : \nat \to \cofe$ such that $\All n, m. n \leq m \Ra c (m) \nequiv{n} c (n)$.
\end{defn}
\begin{defn}
A \emph{complete ordered family of equivalences} (COFE) is a tuple $(\cofe : \OFEs, \lim : \chain(\cofe) \to \cofe)$ satisfying
\begin{align*}
\All n, c.& \lim(c) \nequiv{n} c(n) \tagH{cofe-compl}
\end{align*}
\end{defn}
\begin{defn}
The category $\COFEs$ consists of COFEs as objects, and non-expansive functions as arrows.
\end{defn}
The function space $\ofe \nfn \cofeB$ is a COFE if $\cofeB$ is a COFE (\ie the domain $\ofe$ can actually be just an OFE).
Completeness is necessary to take fixed-points.
For once, every \emph{contractive function} $f : \ofe \to \cofeB$ where $\cofeB$ is a COFE and inhabited has a \emph{unique} fixed-point $\fix(f)$ such that $\fix(f) = f(\fix(f))$.
Furthermore, by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}, every contractive (bi)functor from $\COFEs$ to $\COFEs$ has a unique\footnote{Uniqueness is not proven in Coq.} fixed-point.
\subsection{RA}
......@@ -115,7 +132,7 @@ Since Iris ensures that the global ghost state is valid, this means that we can
\subsection{CMRA}
\begin{defn}
A \emph{CMRA} is a tuple $(\monoid : \COFEs, (\mval_n \subseteq \monoid)_{n \in \nat},\\ \mcore{{-}}: \monoid \nfn \maybe\monoid, (\mtimes) : \monoid \times \monoid \nfn \monoid)$ satisfying:
A \emph{CMRA} is a tuple $(\monoid : \OFEs, (\mval_n \subseteq \monoid)_{n \in \nat},\\ \mcore{{-}}: \monoid \nfn \maybe\monoid, (\mtimes) : \monoid \times \monoid \nfn \monoid)$ satisfying:
\begin{align*}
\All n, \melt, \meltB.& \melt \nequiv{n} \meltB \land \melt\in\mval_n \Ra \meltB\in\mval_n \tagH{cmra-valid-ne} \\
\All n, m.& n \geq m \Ra \mval_n \subseteq \mval_m \tagH{cmra-valid-mono} \\
......@@ -133,7 +150,7 @@ Since Iris ensures that the global ghost state is valid, this means that we can
\end{align*}
\end{defn}
This is a natural generalization of RAs over COFEs.
This is a natural generalization of RAs over OFEs.
All operations have to be non-expansive, and the validity predicate $\mval$ can now also depend on the step-index.
We define the plain $\mval$ as the ``limit'' of the $\mval_n$:
\[ \mval \eqdef \bigcap_{n \in \nat} \mval_n \]
......@@ -209,7 +226,7 @@ Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE struct
\begin{defn}
The category $\CMRAs$ consists of CMRAs as objects, and monotone functions as arrows.
\end{defn}
Note that every object/arrow in $\CMRAs$ is also an object/arrow of $\COFEs$.
Note that every object/arrow in $\CMRAs$ is also an object/arrow of $\OFEs$.
The notion of a locally non-expansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.
%TODO: Discuss how we probably have a commuting square of functors between Set, RA, CMRA, COFE.
......
\section{COFE constructions}
\section{OFE and COFE constructions}
\subsection{Trivial pointwise lifting}
The COFE structure on many types can be easily obtained by pointwise lifting of the structure of the components.
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 COFE $\cofe$, we define $\latert\cofe$ as follows (using a datatype-like notation to define the type):
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 $\COFEs$ to $\COFEs$.
$\latert(-)$ is a locally \emph{contractive} functor from $\OFEs$ to $\OFEs$.
\subsection{Uniform Predicates}
......@@ -117,7 +117,7 @@ Notice that this core is total, as the result always lies in $\maybe\monoid$ (ra
\subsection{Finite partial function}
\label{sec:fpfnm}
Given some infinite countable $K$ and some CMRA $\monoid$, the set of finite partial functions $K \fpfn \monoid$ is equipped with a COFE and CMRA structure by lifting everything pointwise.
Given some infinite countable $K$ and some CMRA $\monoid$, the set of finite partial functions $K \fpfn \monoid$ is equipped with a CMRA structure by lifting everything pointwise.
We obtain the following frame-preserving updates:
\begin{mathpar}
......@@ -139,7 +139,7 @@ $K \fpfn (-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$.
\subsection{Agreement}
Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows:
Given some OFE $\cofe$, we define the CMRA $\agm(\cofe)$ as follows:
\begin{align*}
\agm(\cofe) \eqdef{}& \set{(c, V) \in (\nat \to \cofe) \times \SProp}/\ {\sim} \\[-0.2em]
\textnormal{where }& \melt \sim \meltB \eqdef{} \melt.V = \meltB.V \land
......@@ -152,7 +152,7 @@ Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows:
\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 $\COFEs$ to $\CMRAs$.
$\agm(-)$ is a locally non-expansive functor from $\OFEs$ to $\CMRAs$.
You can think of the $c$ as a \emph{chain} of elements of $\cofe$ that has to converge only for $n \in V$ steps.
The reason we store a chain, rather than a single element, is that $\agm(\cofe)$ needs to be a COFE itself, so we need to be able to give a limit for every chain of $\agm(\cofe)$.
......@@ -175,7 +175,7 @@ There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can
\subsection{Exclusive CMRA}
Given a COFE $\cofe$, we define a CMRA $\exm(\cofe)$ such that at most one $x \in \cofe$ can be owned:
Given an OFE $\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) \mid \mundef \\
\mval_n \eqdef{}& \setComp{\melt\in\exm(\cofe)}{\melt \neq \mundef}
......@@ -193,7 +193,7 @@ The step-indexed equivalence is inductively defined as follows:
\axiom{\mundef \nequiv{n} \mundef}
\end{mathpar}
$\exm(-)$ is a locally non-expansive functor from $\COFEs$ to $\CMRAs$.
$\exm(-)$ is a locally non-expansive functor from $\OFEs$ to $\CMRAs$.
We obtain the following frame-preserving update:
\begin{mathpar}
......
......@@ -51,7 +51,7 @@ Persistence is preserved by conjunction, disjunction, separating conjunction as
One of the troubles of working in a step-indexed logic is the ``later'' modality $\later$.
It turns out that we can somewhat mitigate this trouble by working below the following \emph{except-0} modality:
\[ \diamond \prop \eqdef \later\FALSE \lor \Prop \]
\[ \diamond \prop \eqdef \later\FALSE \lor \prop \]
This modality is useful because there is a class of assertions which we call \emph{timeless} assertions, for which we have
\[ \timeless{\prop} \eqdef \later\prop \proves \diamond\prop \]
......@@ -122,11 +122,11 @@ The following rules identify the class of timeless assertions:
\axiom{\timeless{\FALSE}}
\infer
{\text{$\term$ or $\term'$ is a discrete COFE element}}
{\text{$\term$ or $\term'$ is a discrete OFE element}}
{\timeless{\term =_\type \term'}}
\infer
{\text{$\melt$ is a discrete COFE element}}
{\text{$\melt$ is a discrete OFE element}}
{\timeless{\ownM\melt}}
\infer
......
......@@ -146,8 +146,11 @@
% List
\newcommand{\List}{\ensuremath{\textdom{List}}}
\newcommand{\cofe}{T}
\newcommand{\cofeB}{U}
\newcommand{\ofe}{T}
\newcommand{\ofeB}{U}
\newcommand{\cofe}{\ofe}
\newcommand{\cofeB}{\ofeB}
\newcommand{\OFEs}{\mathcal{OFE}} % category of OFEs
\newcommand{\COFEs}{\mathcal{COFE}} % category of COFEs
\newcommand{\iFunc}{\Sigma}
\newcommand{\fix}{\textdom{fix}}
......
......@@ -18,7 +18,7 @@ The semantic domains are interpreted as follows:
\Sem{\type \to \type'} &\eqdef& \Sem{\type} \nfn \Sem{\type} \\
\end{array}
\]
For the remaining base types $\type$ defined by the signature $\Sig$, we pick an object $X_\type$ in $\COFEs$ and define
For the remaining base types $\type$ defined by the signature $\Sig$, we pick an object $X_\type$ in $\OFEs$ and define
\[
\Sem{\type} \eqdef X_\type
\]
......
......@@ -22,16 +22,16 @@ The purpose of this section is to describe how we solve these issues.
\paragraph{Picking the resources.}
The key ingredient that we will employ on top of the base logic is to give some more fixed structure to the resources.
To instantiate the program logic, the user picks a family of locally contractive bifunctors $(\iFunc_i : \COFEs \to \CMRAs)_{i \in \mathcal{I}}$.
To instantiate the program logic, the user picks a family of locally contractive bifunctors $(\iFunc_i : \OFEs \to \CMRAs)_{i \in \mathcal{I}}$.
(This is in contrast to the base logic, where the user picks a single, fixed CMRA that has a unit.)
From this, we construct the bifunctor defining the overall resources as follows:
\begin{align*}
\mathcal G \eqdef{}& \nat \\
\textdom{ResF}(\cofe^\op, \cofe) \eqdef{}& \prod_{i \in \mathcal I} \mathcal G \fpfn \iFunc_i(\cofe^\op, \cofe)
\textdom{ResF}(\ofe^\op, \ofe) \eqdef{}& \prod_{i \in \mathcal I} \mathcal G \fpfn \iFunc_i(\ofe^\op, \ofe)
\end{align*}
We will motivate both the use of a product and the finite partial function below.
$\textdom{ResF}(\cofe^\op, \cofe)$ is a CMRA by lifting the individual CMRAs pointwise, and it has a unit (using the empty finite partial functions).
$\textdom{ResF}(\ofe^\op, \ofe)$ is a CMRA by lifting the individual CMRAs pointwise, and it has a unit (using the empty finite partial functions).
Furthermore, since the $\iFunc_i$ are locally contractive, so is $\textdom{ResF}$.
Now we can write down the recursive domain equation:
......@@ -93,7 +93,7 @@ We can show the following properties for this form of ownership:
{\ownGhost\gname{\melt : M_i} \Ra \mval_{M_i}(\melt)}
\inferH{res-timeless}
{\text{$\melt$ is a discrete COFE element}}
{\text{$\melt$ is a discrete OFE element}}
{\timeless{\ownGhost\gname{\melt : M_i}}}
\end{mathparpagebreakable}
......@@ -121,8 +121,7 @@ We assume to have the following four CMRAs available:
The last two are the tokens used for managing invariants, $\textmon{Inv}$ is the monoid used to manage the invariants themselves.
Finally, $\textmon{State}$ is used to provide the program with a view of the physical state of the machine.
Furthermore, we assume that instances named $\gname_{\textmon{State}}$, $\gname_{\textmon{Inv}}$, $\gname_{\textmon{En}}$ and $\gname_{\textmon{Dis}}$ of these CMRAs have been created.
(We will discuss later how this assumption is discharged.)
We assume that at the beginning of the verification, instances named $\gname_{\textmon{State}}$, $\gname_{\textmon{Inv}}$, $\gname_{\textmon{En}}$ and $\gname_{\textmon{Dis}}$ of these CMRAs have been created, such that these names are globally known.
\paragraph{World Satisfaction.}
We can now define the assertion $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:
......@@ -187,7 +186,7 @@ Fancy updates satisfy the following basic proof rules:
% \inferH{fup-closeI}
% {}{\knowInv\iname\prop \land \later\prop \proves \pvs[\emptyset][\set\iname] \TRUE}
\end{mathparpagebreakable}
(There are no rules related to invariants here. Those rules will be discussed later, in \Sref{sec:invariants}.)
(There are no rules related to invariants here. Those rules will be discussed later, in \Sref{sec:namespaces}.)
We can further define the notions of \emph{view shifts} and \emph{linear view shifts}:
\begin{align*}
......
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