Commit d3137967 authored by Ralf Jung's avatar Ralf Jung
Browse files

describe how we obtian the dynamic modular higher-order ghost state

parent 7b92a6d7
...@@ -2,6 +2,7 @@ ...@@ -2,6 +2,7 @@
\label{sec:base-logic} \label{sec:base-logic}
The base logic is parameterized by an arbitrary CMRA $\monoid$ having a unit. The base logic is parameterized by an arbitrary CMRA $\monoid$ having a unit.
By \lemref{lem:cmra-unit-total-core}, this means that the core of $\monoid$ is a total function, so we will treat it as such in the following.
This defines the structure of resources that can be owned. This defines the structure of resources that can be owned.
As usual for higher-order logics, you can furthermore pick a \emph{signature} $\Sig = (\SigType, \SigFn, \SigAx)$ to add more types, symbols and axioms to the language. As usual for higher-order logics, you can furthermore pick a \emph{signature} $\Sig = (\SigType, \SigFn, \SigAx)$ to add more types, symbols and axioms to the language.
......
\section{Modular Dynamic Higher-Order Resources}
\label{sec:hogs}
The logic described in \Sref{sec:base-logic} works over an arbitrary CMRA $\monoid$ defining the structure of the resources.
It turns out that we can generalize this further and permit picking CMRAs ``$\iFunc(\Prop)$'' that depend on the structure of assertions themselves.
Of course, $\Prop$ is just the syntactic type of assertions; for this to make sense we have to look at the semantics.
To instantiate the logic, you pick a family of locally contractive bifunctors $(\iFunc_i : \COFEs \to \CMRAs)_{i \in \mathcal{I}}$.
From this, we construct the bifunctor defining the overall resources as follows:
\begin{align*}
\textdom{ResF}(\cofe^\op, \cofe) \eqdef{}& \prod_{i \in \mathcal I} \mathbb{N} \fpfn \iFunc_i(\cofe^\op, \cofe)
\end{align*}
$\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).
Furthermore, since the $\iFunc_i$ are locally contractive, so is $\textdom{ResF}$.
Now we can write down the recursive domain equation:
\[ \iPreProp \cong \UPred(\textdom{ResF}(\iPreProp, \iPreProp)) \]
$\iPreProp$ is a COFE defined as the fixed-point of a locally contractive bifunctor.
This fixed-point exists and is unique by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}.
We do not need to consider how the object is constructed.
We only need the isomorphism, given by
\begin{align*}
\Res &\eqdef \textdom{ResF}(\iPreProp, \iPreProp) \\
\iProp &\eqdef \UPred(\Res) \\
\wIso &: \iProp \nfn \iPreProp \\
\wIso^{-1} &: \iPreProp \nfn \iProp
\end{align*}
Notice that $\iProp$ is the semantic model of assertions for the logic described in \Sref{sec:base-logic} with $\Res$:
\[ \Sem{\Prop} \eqdef \iProp = \UPred(\Res) \]
We thus obtain all the rules of \Sref{sec:base-logic}, and furthermore, we can use the maps $\wIso$ and $\wIso^{-1}$ \emph{in the logic} to convert between logical assertions and the domain $\iPreProp$ which is used in the construction of $\Res$ -- so from elements of $\iPreProp$, we can construct elements of $\Sem{\textlog M}$, which are the elements that can be owned in our logic.
\ralf{TODO: Describe the pattern of only assuming some elements of the index family to indicate a particular functor.}
\ralf{TODO: Show the rules for ownership in this world.}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
%%% End:
...@@ -35,6 +35,8 @@ ...@@ -35,6 +35,8 @@
\endgroup\clearpage\begingroup \endgroup\clearpage\begingroup
\input{model} \input{model}
\endgroup\clearpage\begingroup \endgroup\clearpage\begingroup
\input{ghost-state}
\endgroup\clearpage\begingroup
\input{program-logic} \input{program-logic}
\endgroup\clearpage\begingroup \endgroup\clearpage\begingroup
\input{derived} \input{derived}
......
\section{Language} \section{Language}
\label{sec:language}
A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} (metavariable $\expr$), a set \textdom{Val} of \emph{values} (metavariable $\val$), and a set \textdom{State} of \emph{states} (metvariable $\state$) such that A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions} (metavariable $\expr$), a set \textdom{Val} of \emph{values} (metavariable $\val$), and a set \textdom{State} of \emph{states} (metvariable $\state$) such that
\begin{itemize} \begin{itemize}
...@@ -58,6 +59,7 @@ For any language $\Lang$, we define the corresponding thread-pool semantics. ...@@ -58,6 +59,7 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
\clearpage \clearpage
\section{Program Logic} \section{Program Logic}
\label{sec:program-logic}
\ralf{TODO: Right now, this is a dump of all the things that moved out of the base...} \ralf{TODO: Right now, this is a dump of all the things that moved out of the base...}
...@@ -243,32 +245,7 @@ Notice that this is stronger than saying that the thread pool can reduce; we act ...@@ -243,32 +245,7 @@ Notice that this is stronger than saying that the thread pool can reduce; we act
\subsection{Iris model} \subsection{Iris model}
\paragraph{Semantic domain of assertions.} \paragraph{Semantic domain of assertions.}
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: \maybe{\exm(\textdom{State})}, \ghostRes: \iFunc(\cofe^\op, \cofe)}
\end{align*}
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, since $\Sigma$ is locally contractive, so is $\textdom{ResF}$.
Now we can write down the recursive domain equation:
\[ \iPreProp \cong \UPred(\textdom{ResF}(\iPreProp, \iPreProp)) \]
$\iPreProp$ is a COFE defined as the fixed-point of a locally contractive bifunctor.
This fixed-point exists and is unique by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}.
We do not need to consider how the object is constructed.
We only need the isomorphism, given by
\begin{align*}
\Res &\eqdef \textdom{ResF}(\iPreProp, \iPreProp) \\
\iProp &\eqdef \UPred(\Res) \\
\wIso &: \iProp \nfn \iPreProp \\
\wIso^{-1} &: \iPreProp \nfn \iProp
\end{align*}
We then pick $\iProp$ as the interpretation of $\Prop$:
\[ \Sem{\Prop} \eqdef \iProp \]
\paragraph{Interpretation of assertions.} \paragraph{Interpretation of assertions.}
......
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