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

docs: STS construction; explain why the RA core is not a homomorphism

parent 476bad44
...@@ -42,7 +42,7 @@ Now we can rewrite $\UPred(\monoid)$ as monotone step-indexed predicates over $\ ...@@ -42,7 +42,7 @@ Now we can rewrite $\UPred(\monoid)$ as monotone step-indexed predicates over $\
The reason we chose the first definition is that it is easier to work with in Coq. The reason we chose the first definition is that it is easier to work with in Coq.
\clearpage \clearpage
\section{CMRA constructions} \section{RA and CMRA constructions}
\subsection{Product} \subsection{Product}
\label{sec:prodm} \label{sec:prodm}
...@@ -378,54 +378,79 @@ We obtain the following frame-preserving update: ...@@ -378,54 +378,79 @@ We obtain the following frame-preserving update:
% } % }
% \end{mathpar} % \end{mathpar}
% \subsection{STS with tokens monoid} \subsection{STS with tokens}
% \label{sec:stsmon} \label{sec:stsmon}
% Given a state-transition system~(STS) $(\STSS, \ra)$, a set of tokens $\STSS$, and a labeling $\STSL: \STSS \ra \mathcal{P}(\STST)$ of \emph{protocol-owned} tokens for each state, we construct a monoid modeling an authoritative current state and permitting transitions given a \emph{bound} on the current state and a set of \emph{locally-owned} tokens. 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 a monoid 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}. The construction follows the idea of STSs as described in CaReSL \cite{caresl}.
% We first lift the transition relation to $\STSS \times \mathcal{P}(\STST)$ (implementing a \emph{law of token conservation}) and define upwards closure: 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*} \begin{align*}
% (s, T) \ra (s', T') \eqdef&\, s \ra s' \land \STSL(s) \uplus T = \STSL(s') \uplus T' \\ (s, T) \stsstep (s', T') \eqdef{}& s \stsstep s' \land \STSL(s) \uplus T = \STSL(s') \uplus T' \\
% \textsf{frame}(s, T) \eqdef&\, (s, \STST \setminus (\STSL(s) \uplus T)) \\ s \stsfstep{T} s' \eqdef{}& \Exists T_1, T_2. T_1 \sep \STSL(s) \cup T \l+and (s, T_1) \stsstep (s', T_2)
% \upclose(S, T) \eqdef&\, \setComp{ s' \in \STSS}{\exists s \in S.\; \textsf{frame}(s, T) \ststrans \textsf{frame}(s', T) } \end{align*}
% \end{align*}
% \noindent We further define \emph{closed} sets of states (given a particular set of tokens) as well as the \emph{closure} of a set:
% We have \begin{align*}
% \begin{quote} \STSclsd(S, T) \eqdef{}& \All s \in S. \STSL(s) \sep T \land \All s'. s \stsfstep{T} s' \Ra s' \in S \\
% If $(s, T) \ra (s', T')$\\ \upclose(S, T) \eqdef{}& \setComp{ s' \in \STSS}{\Exists s \in S. s \stsftrans{T} s' }
% and $T_\f \sep (T \uplus \STSL(s))$,\\ \end{align*}
% then $\textsf{frame}(s, T_\f) \ra \textsf{frame}(s', T_\f)$.
% \end{quote}
% \begin{proof}
% This follows directly by framing the tokens in $\STST \setminus (T_\f \uplus T \uplus \STSL(s))$ around the given transition, which yields $(s, \STST \setminus (T_\f \uplus \STSL{T}(s))) \ra (s', T' \uplus (\STST \setminus (T_\f \uplus T \uplus \STSL{T}(s))))$.
% This is exactly what we have to show, since we know $\STSL(s) \uplus T = \STSL(s') \uplus T'$.
% \end{proof}
% Let $\STSMon{\STSS}$ be the monoid with carrier The STS RA is defined as follows
% \[ \begin{align*}
% \setComp{ (s, S, T) \in \exm{\STSS} \times \mathcal{P}(\STSS) \times \mathcal{P}(\STST) }{ \begin{aligned} &(s = \munit \lor s \in S) \land \upclose(S, T) = S \land{} \\& S \neq \emptyset \land \All s \in S. \STSL(s) \sep T \end{aligned} } \monoid \eqdef{}& \setComp{\STSauth((s, T) \in \STSS \times \wp(\STST))}{\STSL(s) \sep T} +{}\\& \setComp{\STSfrag((S, T) \in \wp(\STSS) \times \wp(\STST))}{\STSclsd(S, T) \land S \neq \emptyset} + \bot \\
% \] \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 \sep T_2$ and $S_1 \cap S_2 \neq \emptyset$} \\
% and multiplication \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 \sep T'$ and $s \in S$} \\
% \[ \mcore{\STSfrag(S, T)} \eqdef{}& \STSfrag(\upclose(S, \emptyset), \emptyset) \\
% (s, S, T) \mtimes (s', S', T') \eqdef (s'' \eqdef s \mtimes_{\exm{\STSS}} s', S'' \eqdef S \cap S', T'' \eqdef T \cup T') \quad \text{if }\begin{aligned}[t] &(s = \munit \lor s' = \munit) \land T \sep T' \land{} \\& S'' \neq \emptyset \land (s'' \neq \munit \Ra s'' \in S'') \end{aligned} \mcore{\STSauth(s, T)} \eqdef{}& \STSfrag(\upclose(\set{s}, \emptyset), \emptyset)
% \] \end{align*}
The remaining cases are all $\bot$.
% Some sugar makes it more convenient to assert being at least in a certain state and owning some tokens: $(s, T) : \STSMon{\STSS} \eqdef (\munit, \upclose(\{s\}, T), T) : \STSMon{\STSS}$, and We will need the following frame-preserving update:
% $s : \STSMon{\STSS} \eqdef (s, \emptyset) : \STSMon{\STSS}$. \begin{mathpar}
\inferH{sts-step}{(s, T) \ststrans (s', T')}
{\STSauth(s, T) \mupd \STSauth(s', T')}
% We will need the following frame-preserving update. \inferH{sts-weaken}
% \begin{mathpar} {\STSclsd(S_2, T_2) \and S_1 \subseteq S_2 \and T_2 \subseteq T_1}
% \inferH{StsStep}{(s, T) \ststrans (s', T')} {\STSfrag(S_1, T_1) \mupd \STSfrag(S_2, T_2)}
% {(s, S, T) \mupd (s', \upclose(\{s'\}, T'), T')} \end{mathpar}
% \end{mathpar}
% \begin{proof}[Proof of \ruleref{StsStep}] \paragraph{The core is not a homomorphism.}
% Assume some upwards-closed $S_\f, T_\f$ (the frame cannot be authoritative) s.t.\ $s \in S_\f$ and $T_\f \sep (T \uplus \STSL(s))$. We have to show that this frame combines with our final monoid element, which is the case if $s' \in S_\f$ and $T_\f \sep T'$. 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}.
% By upward-closedness, it suffices to show $\textsf{frame}(s, T_\f) \ststrans \textsf{frame}(s', T_\f)$.
% This follows by induction on the path $(s, T) \ststrans (s', T')$, and using the lemma proven above for each step. In other words, the following does \emph{not} hold for the STS core as defined above:
% \end{proof} \[ \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: %%% Local Variables:
%%% mode: latex %%% mode: latex
......
...@@ -353,10 +353,16 @@ ...@@ -353,10 +353,16 @@
% STSs % STSs
\newcommand{\STSCtx}{\textlog{StsCtx}} \newcommand{\STSCtx}{\textlog{StsCtx}}
\newcommand{\STSSt}{\textlog{StsSt}} \newcommand{\STSSt}{\textlog{StsSt}}
\newcommand{\STSclsd}{\textlog{closed}}
\newcommand{\STSauth}{\textlog{auth}}
\newcommand{\STSfrag}{\textlog{frag}}
\newcommand{\STSS}{\mathcal{S}} % states \newcommand{\STSS}{\mathcal{S}} % states
\newcommand{\STST}{\mathcal{T}} % tokens \newcommand{\STST}{\mathcal{T}} % tokens
\newcommand{\STSL}{\mathcal{L}} % labels \newcommand{\STSL}{\mathcal{L}} % labels
\newcommand{\stsstep}{\ra}
\newcommand{\ststrans}{\ra^{*}}% the relation relevant to the STS rules \newcommand{\ststrans}{\ra^{*}}% the relation relevant to the STS rules
\newcommand{\stsfstep}[1]{\xrightarrow{#1}}
\newcommand{\stsftrans}[1]{\stsfstep{#1}^{*}}
\tikzstyle{sts} = [->,every node/.style={rectangle, rounded corners, draw, minimum size=1.2cm, align=center}] \tikzstyle{sts} = [->,every node/.style={rectangle, rounded corners, draw, minimum size=1.2cm, align=center}]
......
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