MessagesAndRefinement chapter: refinement

frap_book.tex

@@ -4055,6 +4055,7 @@ Here's the intuitive explanation of each syntax construction.
 \newcommand{\readl}[2]{?#1(#2)}
 \newcommand{\writel}[2]{!#1(#2)}
 \newcommand{\lts}[3]{#1 \stackrel{#2}{\longrightarrow} #3}
+\newcommand{\ltsS}[3]{#1 \stackrel{#2}{\longrightarrow}^* #3}
 
 \medskip
 
@@ -4107,6 +4108,76 @@ The labelled transition system approach may seem a bit unwieldy for just explain
 Where it really pays off is in supporting a modular, algebraic reasoning style about processes, which we turn to next.
 
 
+\section{Refinement Between Processes}
+
+What sorts of correctness theorems should we prove about processes?
+The classic choice is to show that a more complex \emph{implementation} process is a \emph{safe substitute} for a simpler \emph{specification} process.
+We will say that the implementation $p$ \emph{refines}\index{refinement} the specification $p'$.
+Intuitively, such a claim means that any trace of labels that $p$ could generate may also be generated by $p'$, so that $p$ has \emph{no more behaviors} than $p'$ has, though it may have fewer behaviors.
+Crucially, in building traces of process executions, we ignore silent labels, only collecting the send and receive labels.
+
+This condition is called \emph{trace inclusion}\index{trace inclusion}, and, though it is intuitive, it is not strong enough to support all of the composition properties that we will want.
+Instead, we formalize refinement via \emph{simulation}.
+
+\begin{definition}
+  Binary relation $R$ between processes is a \emph{simulation} when these two conditions hold.
+  \begin{itemize}
+  \item \textbf{Silent steps match up}: when $p_1 \; R \; p_2$ and $\lts{p_1}{}{p'_1}$, there always exists $p'_2$ such that $\ltsS{p_2}{}{p'_2}$ and $p'_1 \; R \; p'_2$.
+  \item \textbf{Communication steps match up}: when $p_1 \; R \; p_2$ and $\lts{p_1}{l}{p'_1}$ for $l \neq \silent$, there always exist $p''_2$ and $p'_2$ such that $\ltsS{p_2}{}{p''_2}$, $\lts{p''_2}{l}{p'_2}$, and $p'_1 \; R \; p'_2$.
+  \end{itemize}
+\end{definition}
+
+Intuitively, $R$ is a simulation when, starting in a pair of related processes, any step on the left can be matched by a step on the right, taking us back into $R$.
+The conditions are naturally illustrated with commuting diagrams\index{commuting diagram}.
+
+\[
+\begin{tikzcd}
+p_1 \arrow{r}{R} \arrow{d}{\forall \longrightarrow} & p_2 \arrow{d}{\exists \longrightarrow^*} \\
+p'_1 & p'_2 \arrow{l}{R^{-1}}
+\end{tikzcd}
+\quad \begin{tikzcd}
+p_1 \arrow{r}{R} \arrow{d}{\forall \stackrel{l}{\longrightarrow}} & p_2 \arrow{d}{\exists \longrightarrow^* \stackrel{l}{\longrightarrow}} \\
+p'_1 & p'_2 \arrow{l}{R^{-1}}
+\end{tikzcd}
+\]
+
+\newcommand{\refines}[2]{#1 \leq #2}
+
+\invariants
+This notion of simulation has quite a lot in common with our well-worn concept of invariants of transition systems.
+Simulation can be seen as a kind of natural generalization of invariants, which are predicates over single states, into relations that apply to states of two different transition systems that need to evolve in (approximate) lock-step.
+
+We define \emph{refinement} $\refines{p_1}{p_2}$ to indicate that there exists a simulation $R$ such that $p_1 \; R \; p_2$.
+Luckily, this somewhat involved definition is easily related back to our intuitions.
+
+\begin{theorem}
+  If $\refines{p_1}{p_2}$, then every trace generated by $p_1$ is also generated by $p_2$.
+\end{theorem}
+\begin{proof}
+  By induction on any trace generated by $p_1$.
+\end{proof}
+
+Refinement is also a preorder\index{preorder}.
+
+\begin{theorem}[Reflexivity]
+  For all $p$, $\refines{p}{p}$.
+\end{theorem}
+\begin{proof}
+  Choose equality as the simulation relation.
+\end{proof}
+
+\begin{theorem}[Transitivity]
+  If $\refines{p_1}{p_2}$ and $\refines{p_2}{p_3}$, then $\refines{p_1}{p_3}$.
+\end{theorem}
+\begin{proof}
+  The two premises respectively imply the existence of simulations $R_1$ and $R_2$.
+  Set the new simulation relation as $R_1 \circ R_2$, defined to contain a pair $(p, q)$ iff there exists $r$ with $p \; R_1 \; r$ and $r \; R_2 \; q$.
+\end{proof}
+
+The accompanying Coq code includes several examples of verifying moderately complex processes, by manual tailoring of simulation relations.
+We leave those details to the code, turning now instead to further algebraic properties that allow us to \emph{compose} laborious manual proofs about components, in a black-box way.
+
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \appendix