\documentclass[11pt,twoside]{article}
\usepackage{macros-course-lectures}

\renewcommand{\thepage}{\arabic{page}}

%\makeslides

\renewcommand{\thefootnote}{}

\begin{document}

\onlystudents

\lecture{notes10}{Composing and Decomposing Computational
Processes}{October 12, 2000}

\section{Externally-visible behavior}

\subsection{Dynamic Set}

\begin{tabbing}
XXX\=XXX\= \kill
$Q$: 
\> $\ms{fun}$, a function from $S$ to $\{0, 1\}$. \\
\> $\ms{req}$, either $\ms{add}(v)$, $\ms{delete}(v)$, $\ms{lookup}(v)$,
or $\ms{null}$, which represents no active request \\
\> $\ms{resp}$, either $\ms{OK}$, a Boolean $b$, or $\ms{null}$, which
indicates no ready response. \\
$Q_0$: 
\> $\ms{fun}$: As before, the function that maps everything to $0$,
representing the empty set. \\
\> $\ms{req}$: $\ms{null}$ \\
\> $\ms{resp}$: $\ms{null}$ \\
$\delta$: 
\> Input steps: \\
\> $\ms{request}(\ms{add}(v))$: \\
\> Can occur anytime \\
\> Effect: if $\ms{req} = \ms{null}$ then $\ms{req} := \ms{add}(v)$ \\
\> And similarly for the other two kinds of inputs. \\
\\
\> Internal steps: \\
\> $\ms{perform}(\ms{add}(v))$: \\
\> Can occur if: $\ms{req} = \ms{add}(v)$ and $\ms{resp} = \ms{null}$ \\
\> Effect is to set $\ms{fun}(v)$ to $1$ and $\ms{resp}$ to $\ms{OK}$ \\
\\
\> $\ms{perform}(\ms{delete}(v))$ \\
\> Can occur if: $\ms{req} = \ms{delete}(v)$ and $\ms{resp} = \ms{null}$\\
\> Effect: $\ms{fun}(v) := 0$; $\ms{resp} := \ms{OK}$ \\
\\
\> $\ms{perform}(\ms{lookup}(v))$: \\
\> Can occur if: $\ms{req} = \ms{lookup}(v)$ and $\ms{resp} = \ms{null}$\\
\> Effect: $\ms{resp} := \ms{fun}(v)$ \\
\\
\> Output steps: \\
\> $\ms{respond}(r)$: \\
\> Can occur if: $\ms{resp} = r$ \\
\> Effect:  $\ms{req} := \ms{null}$, $\ms{resp} := \ms{null}$
\end{tabbing}

\subsection{Caching}

Weak caching:
\begin{tabbing}
XXX\=XXX\= \kill
$Q$: 
\> $\ms{mem}$, $\ms{cache}$, same types as before \\
\> $\ms{req}$, a mapping from $I$ (locations) to the set of values $\{ \ms{read}(a), \ms{write}(a,v), \ms{null} \}$ \\
\> $\ms{resp}$, a mapping from $I$ to the set of values $V$ (the value set) $\cup \{ \ms{OK} \ms{null} \}$ \\
$Q_0$: 
$\ms{mem}$ everywhere $v_0$, $\ms{cache}$ everywhere $\ms{null}$,
bookkeeping components all $\ms{null}$ \\
$L$: 
\> Input: \\ 
\> \> $\ms{request}(\ms{read}(a),i)$, $a \in A$, $i \in I$ \\
\> \> $\ms{request}(\ms{write}(a,v),i)$, $a \in A$, $v \in V$, $i \in I$ \\
\> Internal: \\
\> \> $\ms{perform}(\ms{read}(a),i)$, $a \in A$, $i \in I$ \\
\> \> $\ms{perform}(\ms{write}(a,v),i)$, $a \in A$, $v \in V$, $i \in I$ \\
\> \> $\ms{copy}(a,i)$, $a \in A$, $i \in I$ \\
\> \> $\ms{drop}(a,i)$, $a \in A$, $i \in I$ \\
\> Output: \\
\> \> $\ms{respond}(v,i)$, $v \in V$, $i \in I$ \\
\> \> $\ms{respond}(\ms{OK},i)$, $i \in I$ \\
$\delta$: 
\> $\ms{request}(\ms{read}(a),i)$ \\
\> Can occur:  anytime \\
\> Effect: if $\ms{req}(i) = \ms{null}$ then $\ms{req}(i) := \ms{read}(a)$ \\
\\
\> $\ms{request}(\ms{write}(a,v),i)$ \\
\> Can occur:  anytime \\
\> Effect: if $\ms{req}(i) = \ms{null}$ then $\ms{req}(i) := \ms{write}(a,v)$ \\
\\
\> $\ms{perform}(\ms{read}(a),i)$, $a \in A$, $i \in I$ \\
\> Can occur: $\ms{req}(i) = \ms{read}(a)$, $\ms{cache}(a,i) \neq \ms{null}$,
and $\ms{resp}(i) = \ms{null}$ \\
\> Effect: $\ms{resp}(i) := \ms{cache}(a,i)$ \\
\\
\> $\ms{perform}(\ms{write}(a,v),i)$ \\
\> Can occur: $\ms{req}(i) = \ms{write}(a,v)$ and $\ms{resp}(i) = \ms{null}$ \\
\> Effect: $\ms{mem}(a) := v$; $\ms{resp}(i) := \ms{OK}$ \\
\\
\> $\ms{copy}(a,i)$ \\
\> Can occur: anytime \\
\> Effect: $\ms{cache}(a,i) := \ms{mem}(a)$ \\
\\
\> $\ms{drop}(a,i)$ \\
\> Can occur:  anytime \\
\> Effect: $\ms{cache}(a,i) := \ms{null}$ \\
\\
\> $\ms{respond}(r,i)$ \\
\> Can occur: $\ms{resp}(i) = r$ \\
\> Effect: $\ms{req}(i) := \ms{null}$; $\ms{resp}(i) := \ms{null}$ \\
\\
Strong caching, same except for: \\
\> $\ms{perform}(\ms{write}(a,v),i)$ \\
\> Can occur: $\ms{req}(i) = \ms{write}(a,v)$ and $\ms{resp}(i) = \ms{null}$ \\
\> Effect: $\ms{mem}(a) := v$; for all $i$, $\ms{cache}(a,i) := \ms{null}$;
$\ms{resp}(i) := \ms{OK}$ 
\end{tabbing}

\newpage
\section{Implementation}

\subsection{Dynamic set}

\begin{tabbing}
XXX\=XXX\= \kill
$Q$: 
\> $\ms{dynamic-set}$, a subset of $S$ \\
\> $\ms{req}$, $\ms{resp}$, as before \\
$Q_0$: 
\> $\ms{dynamic-set}$: $\emptyset$ \\
\> $\ms{req}$, $\ms{resp}$: $\ms{null}$ \\
$L$: 
\> As before. \\
$\delta$: 
\> Inputs, outputs:  As before. \\
\> Internal steps: \\
\> $\ms{perform}(\ms{add}(v))$: \\
\> Can occur if: $\ms{req} = \ms{add}(v)$ and $\ms{resp} = \ms{null}$ \\
\> Effect: $\ms{dynamic-set} := \ms{dynamic-set} \cup \{ v \}$; $\ms{resp} := \ms{OK}$ \\
\\
\> $\ms{perform}(\ms{delete}(v))$ \\
\> Can occur if: $\ms{req} = \ms{delete}(v)$ and $\ms{resp} = \ms{null}$\\
\> Effect: $\ms{dynamic-set} := \ms{dynamic-set} - \{ v \}$; $\ms{resp} := \ms{OK}$ \\
\\
\> $\ms{perform}(\ms{lookup}(v))$: \\
\> Can occur if: $\ms{req} = \ms{lookup}(v)$ and $\ms{resp} = \ms{null}$\\
\> Effect: if $v \in \ms{dynamic-set}$ then $\ms{resp} := 1$ else
$\ms{resp} := 0$ 
\end{tabbing}

\subsection{Caching example}

Centralized memory machine:
\begin{tabbing}
XXX\=XXX\= \kill
$Q$: $\ms{mem}$, $\ms{req}$, $\ms{resp}$, same types as for $\ms{SC}$ \\
$Q_0$:  As for $\ms{SC}$. \\
$L$: 
\> Input, Output:  As for $\ms{SC}$. \\
\> Internal: \\
\> \> $\ms{perform}(\ms{read}(a),i)$, $a \in A$, $i \in I$ \\
\> \> $\ms{perform}(\ms{write}(a,v),i)$, $a \in A$, $v \in V$, $i \in I$ \\
Transitions: \\
\> Input, Output:  As for $\ms{SC}$. \\
\> Internal: \\
\> $\ms{perform}(\ms{read}(a),i)$ \\
\> Can occur: $\ms{req}(i) = \ms{read}(a)$ and $\ms{resp}(i) = \ms{null}$ \\
\> Effect: $\ms{resp}(i) := \ms{mem}(a)$ \\
\\
\> $\ms{perform}(\ms{write}(a,v),i)$ \\
\> Can occur: $\ms{req}(i) = \ms{write}(a,v)$ and $\ms{resp}(i) = \ms{null}$ \\
\> Effect: $\ms{mem}(a) := v$; $\ms{resp}(i) := \ms{OK}$ 
\end{tabbing}

\newpage
\section{Abstraction relations and the Abstraction Theorem}

\begin{definition}
Suppose $A$ and $B$ are labeled state machines with the same input
and output labels. \\
Then a relation $R$ from states of $A$ to states of $B$ is called an {\em
abstraction relation\/} from $A$ to $B$ provided that the following
conditions hold: 
\begin{enumerate}
\item (Start condition) \\
If $q_A$ is a start state of $A$, then there exists
a start state $q_B$ of $B$ such that $(q_A,q_B) \in R$. 
\item (Step condition) \\
If $q_A$ and $q_B$ are reachable states of $A$ and $B$, respectively,
$(q_A,q_B) \in R$, and $(q_A,\ell,q'_A)$ is a step of $A$, 
then there is a sequence of ($0$ or more) steps of $B$ that: \\
-- Starts with $q_B$, \\
-- Ends with some state $q'_B$ such that $(q'_A,q'_B) \in R$, and \\
-- Has the same trace as the step of $A$ (that is, it looks the same
externally). 
\end{enumerate}
\end{definition}

\section{Composition}

Environment automaton, for $\ms{Split-SC}$
\begin{tabbing}
XXX\=XXX\= \kill
$Q$: $\ms{locks}$, a mapping from $A$ to subsets of $I$ \\
$Q_0$:  for all $a$, $\ms{locks}(a) = \emptyset$ \\
$L$: Reverse of $\ms{Split-SC}$: \\
\> Input: \\
\> \> $\ms{respond}(v,i)$, $v \in V$, $i \in I$ \\
\> \> $\ms{respond}(\ms{OK},i)$, $i \in I$ \\
\> Output: \\
\> \> $\ms{request}(\ms{read}(a),i)$, $a \in A$, $i \in I$ \\
\> \> $\ms{request}(\ms{write}(a,v),i)$, $a \in A$, $v \in V$, $i \in I$ \\  
\\
Transitions: \\
\> $\ms{respond}(*,i)$ \\
\> Can occur: anytime \\
\> Effect: for all $a$, $\ms{locks}(a) := \ms{locks}(a) - \{ i \}$ \\
\\
\> $\ms{request}(\ms{read}(a),i)$ \\
\> Can occur: $\ms{locks}(a) = \emptyset$ \\
\> Effect: $\ms{locks}(a) := \{ i \}$ \\
\\
\> $\ms{request}(\ms{write}(a,v),i)$ \\
\> Can occur: $\ms{locks}(a) = \emptyset$ \\
\> Effect: $\ms{locks}(a) := \{ i \}$ 
\end{tabbing}
\end{document}



