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

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

%\makeslides

\renewcommand{\thefootnote}{}

\begin{document}

\mainlylecture

\lecture{notes8}{%
Computational Processes}{March 6, 2001}


\reading{These notes.  Rosen Section 2.2, 3.5 (skim)}


\section{Overview}

\footnote{\copyright~2000 by Nancy A. Lynch.  All rights reserved.}%

\begin{breakperiods}

Our next topic will introduce some of the basic math ideas behind {\em
  computational processes}.  I'm using the term in a very general
way, to denote any kind of system that begins in a special ``starting
state'', and progresses from state to state in discrete steps,
according to specified rules.  These include:
\begin{description}
\item[Sequential algorithms,] \ie\ abstract versions of
  sequential programs.  \Eg, programs that sort data, or compute a
  numerical solution to a complicated equation.
\item[Distributed algorithms,] \ie\ abstract versions of distributed
  programs.  For example,  programs that implement an application like
  a multi-branch banking system or an airline reservation system. 
\item[(Abstract descriptions of) complicated computer systems:]
  Operating systems, computer architectures, or communication systems. 
\item[Games,] defined by rules that constrain the moves. 
\end{description}
Many computational processes are {\em nondeterministic\/}, which just
means that the next state isn't always determined by the previous
state.  There might be explicit choice points, like the next move in
a game.  Or just different possible orders in which things might
happen, \eg, different orders in which two messages might arrive at a
destination.

The idea of a computational process is very general.
But it turns out that some simple math can go a long way in helping
us to understand and reason about them. 


We will introduce a basic math model for a computational process,
called a {\em state machine}.  We give basic definitions that will
let us talk about how such a process behaves.

We'll look at some informal examples, of several kinds, based on
sequential and parallel algorithms, system descriptions, and games.
We'll try to understand informally how these processes behave.  Also,
since they are based on a real math model, we will try to {\em
  prove\/} some things about how they behave.  After this high level
outline, we'll get more systematic about how you do proofs about
computational processes.

The most important idea for analyzing state machines is that of an
``invariant'', which describes a property that is always true of the
state of a process, no matter how it behaves.  You will see how
invariants can be used to prove basic correctness properties for
algorithms.  We'll give systematic method for proving invariants,
based on ordinary math induction.  Then we'll look briefly at other
kinds of properties one might want to prove about processes, \eg, that
they terminate, or that they finish within some fixed amount of time.
The focus here will be on providing the basic math definitions and a
little basic theory, and showing you some examples of how these can be
used.

One can move beyond this, looking at some ways to impose some
structure on processes, specifically, to:
\begin{itemize}
\item
Combine small processes to build bigger processes.

For instance, to build a distributed banking system out of pieces that
run on different machines.  Or, to build a powerful application out
of a bunch of simpler services.

\item
Consider systems at different levels of abstraction. 
\end{itemize}

These ideas will be useful to you when you work on (or take courses
on) computer systems.  \eg, 6.170 SWE includes a lot of
object-oriented programming.  State machines can be used to describe
objects, how some objects can be viewed at different levels of
abstraction, and how objects can be combined.
\end{breakperiods}

\section{Die Hard}

\begin{breakperiods}
  In Die Hard 3, Bruce Willis and Samuel Jackson are faced with a
  test.  They need exactly $4$ gallons of water to disarm a bomb.
  They have a reservoir and two empty jars, one that holds $3$ gallons
  and one that holds $5$ gallons.  Their only options are to fill a
  jar to the top, empty a jar completely, or pour water from one jar
  to the other until one is empty or the other is full.  Following
  their script carefully, they succeed!  Here's how:

\begin{center}
\begin{tabular}{lcc}
action & large bucket & small bucket \\
\hline fill big bucket & 5 & 0\\
pour big into little & 2 & 3\\
 empty little & 2 & 0\\
 pour big into little & 0 & 2\\
 fill big & 5 &2\\
 pour big into little & 4 & 3\\
\end{tabular}
\end{center}

However, according to rumor, there will be a sequel, Die Once and For
All.  In this film, Bruce and Samuel will face a more devious villian.
This time they will have a $3$-gallon jar and a $9$-gallon jar.  The
water-pouring rules are the same.  They must produce $4$ gallons in 30
seconds or the bomb will go off.

A little experimentation suggests that the task is impossible.  But
we'll all rest a little easier if we can prove mathematically that
there can be no more Die Hard movies.  How might such a proof be
constructed?  Insight can be gained by stating more precisely what we
want to prove: namely, that it is impossible, by any sequence of
moves, to get exactly 4 gallons of water into the large jug.  A
sequence of moves is constructed one move at a time.  This makes it
natural to consider a proof by induction on the length of the
sequence.

This is a general approach to this for handling processes. We want to
show that some condition always holds during the evolution of some
process.  We do so by induction on the number of steps or
operations in the evolution.  In this case, we can let $n$ be the
number of times water is poured.

All will be well if we can prove that neither jug contains $4$ gallons
after $n$ steps for all $n \geq 0$.  This statement contains a natural
number variable $n$, and so can serve as an induction hypothesis.
Let's try lunging into a proof:

\begin{theorem}
Bruce dies.
\end{theorem}

Let's try to prove this claim by induction.  Let $P(n)$ be the
predicate that neither jug contains 4 gallons of water after $n$
steps.  In the base case, $P(0)$ holds because both jugs are initially
empty.  In the inductive step, we assume that neither jug has 4
gallons after $n$ steps and try to prove that neither jug has 4
gallons after $n+1$ steps.

Now we are stuck; the proof cannot be completed.  The fact that
neither jug contains 4 gallons of water after $n$ steps is not
sufficient to prove that neither jug can contain 4 gallons after
$n+1$ steps.  For example, after $n$ steps each jug might hold 2
gallons of water.  Pouring all water in the 3-gallon jug into the
9-gallon jug would produce 4 gallons after $n+1$ steps.

What to do?  We can strengthen the induction hypothesis.  A
``stronger'' induction hypothesis is one that implies the old
hypothesis.

Some more experimentation suggests letting $P(n)$ be the predicate
that after $n$ steps, the number of gallons of water in each jug is a
multiple of 3.  This is a stronger predicate; if the number of gallons
of water in each jug is a multiple of 3, then neither jug contains 4
gallons of water.

This induction hypothesis does lead to a correct proof of the theorem.
In order to make this proof complete, we'll introduce some formal
machinery---a new mathematical data structure called a \emph{state
  machine}, which will be useful for this and other problems.


\section{State machines}

\subsection{Basic definitions}

Mathematically speaking, a state machine is just a binary relation on
states, where the pairs in the relation correspond to the allowed
steps of the machine.  In addition, a state machine has some states
that are designated as start states---the ones in which it is allowed
to begin executing.

\begin{definition} A \emph{state machine} is described by three elements:
\begin{itemize}
\item $Q$, the set of \emph{states} (which must be nonempty) 
\item $Q_0 \subseteq Q$, the set of \emph{start states} (also nonempty)
\item $\delta \subseteq Q \times Q$, the set of \emph{allowed
    transitions} between states. 
\end{itemize}
\end{definition}


Although this is really nothing more than a digraph with start states
(start nodes), we use different notation. 
Instead of $(A,R)$ as we used for relations, or $G=(V,E)$ as we used
for graphs, we use the three-tuple $(Q,Q_0,\delta)$. 
This simply reflects the different customs of different areas of cs
and math. 

We often write $q \rightarrow q'$ for the statement that $(q,q') \in
\delta$.

This is similar to the definition of a finite-state machine that you
might have seen in a hardware class (you will see this if you take
6.045).  But these need not be finite-state.  Also, we haven't given
them (yet) any notion of input and output.


\subsection{Examples}

Here are some simple examples of state machines.

\begin{example}
A bounded counter, which counts from $0$ to $100$ 
\begin{itemize}
\item 
$Q = \{ 0, 1, 2, \ldots, 99, \ms{overflow} \} 
$
(note the special value for overflow).

\item $Q_0 = \{ 0 \}$ 
\item $\delta = \{ (0,1), (1,2), (2,3), \ldots,
  (99,\ms{overflow}),(\ms{overflow},\ms{overflow}) \}$.  
Note the self-loop (transition to itself) for the overflow state.
\end{itemize}
It is easy to draw this state machine as digraph. 
\end{example}



\begin{example}
  An unbounded counter is similar, but has an infinite state set,
  yielding an infinite digraph.  This is harder to draw.
\end{example}

\begin{example}
Die Hard can be formalized as a state machine as well.
\begin{itemize}
\item 
  $Q = \{ (b,l) \mid  0 \leq b \leq 5, 0 \leq l \leq 3 \}$ Note that
  $(b,l)$ are not necessarily integers so we could allow the state set
  to range over reals).

\item $Q_0 = \{ (0,0) \}$, both start empty. 

\item $\delta$ has several kinds of steps: 
\begin{enumerate}

\item  Fill the little jar: $(b,l) \rightarrow (b,3)$ 

\item  Fill the big jar: $(b,l) \rightarrow (5,l)$ 

\item  Empty the little jar: $(b,l) \rightarrow (b,0)$ 

\item  Empty the big jar: $(b,l) \rightarrow (0,l)$ 

\item  Pour from the little jar into the big jar: $(b,l) \rightarrow
(\min{(b+l,5)},\max{(0,b+l-5)})$ 

\item Pour from big jar into little jar: $(b,l) \rightarrow 
(\max{(b+l-3,0)},\min{(b+l,3)})$ 
\end{enumerate}
\end{itemize}
\end{example}

Note the way we define the transition relation: we are listing a set
of states to which state $(b,l)$ can transition.  Implicitly, we are
saying this is the comprehensive list of transitions for every $(b,l)$
in the state set.

Let's discuss the reason for these expressions.  For example, look at
step five.  The amount of water that winds up in the big jar is all the
water than was there ($b$) plus as much of the water in the little jar
as will fit in the big jar.  That's $\min(b+l,5)$.  We can see this
using cases: if $b+l \leq 5$, we get $b+l$, otherwise it tops out at
$5$. The second term represents what's left over.  The amount in the
little jar is calculated similarly.


This state machine is an example of a {\em nondeterministic\/} state
machine.  There is more than one possible transition out of certain
states.


\begin{definition}
  A state machine $(Q,Q_0,\delta)$ is {\em deterministic\/} if $|Q_0|
  = 1$ and for every $q \in Q$, $\exists$ at most one $q'$ such that
  $q \rightarrow q'$.  Otherwise, it is {\em nondeterministic\/}.
\end{definition}

According to this definition, the Die Hard state machine is
nondeterministic.  In fact, it has as many as $6$ different
transitions out of some states (but not from all: for some values of
$(b,l)$, such as $(0,2)$, some of the transitions listed in the
definition become duplicates).  On the other hand, the counter
machines are deterministic.

\subsection{Executions of state machines}

We can model the possible behaviors of a computational process by
\emph{executions} of the state machine that's used to model it. 

\begin{definition}
An \emph{execution} is a (possibly infinite) sequence $q_0,
q_1, \ldots$ such that $q_0 \in Q_0$, and 
$\forall i \geq 0 (q_i,q_{i+1}) \in \delta$. 
\end{definition}
In other words, an execution is as a path in the digraph that begins
with a start state.  It is a sequence of states that can arise as the
process described by the state machine evolves.  

One thing we often want to understand about the behavior of a
computational process is what kinds of states can be reached in its
executions. 

\begin{definition}
  A state is {\em reachable\/} if it's the final state in some
  finite-length execution.
\end{definition}

\begin{example}
In Die Hard 3, we can reach state (4,0), by the execution: 

\begin{center}
\begin{tabular}{lc}
action & state\\
\hline (start state)& (0,0)\\
 fill the big jar & (5,0), \\
pour the big into the little & (2,3), \\
empty the little & (2,0), \\
pour the big into the little & (0,2), \\
fill the big jar, &(5,2)  \\
put the big into the little & (4,3), \\
empty the little & (4,0) \\
\end{tabular}
\end{center}
So, state (4,0) is reachable. 
\end{example}

Now back to Die Once and For All.  The same problem, but with 9 and 3
gallon jars instead of 5 and 3.  The states are similar to before.
The start state is the same.  The transition relation is different:
\begin{enumerate}
\item Fill the little jar: $(b,l) \rightarrow (b,3)$ 
\item Fill big jar: $(b,l) \rightarrow (9,l)$ 
\item Empty little jar: $(b,l) \rightarrow (b,0)$ 
\item Empty big jar: $(b,l) \rightarrow (0,l)$ 
\item Pour from little jar into big jar: $(b,l) \rightarrow
(\min{(b+l,9)},\max{(0,b+l-9)})$. 
\item Pour from big jar into little jar: $(b,l) \rightarrow 
(\max{(b+l-3,0)},\min{(b+l,3)})$. 
\end{enumerate}

Now reaching $(4,0)$ is impossible.  More formally, we can prove no
reachable state has 4 in the larger jar.  To do so we strengthen the
inductive hypothesis, and define:
\begin{quote}
$P(n)$: At the end of any $n$-step execution, the contents of
each jar are integer multiples of 3 gallons. 
\end{quote}
\end{breakperiods}

\structuredproof{
Prove: $\forall n \geq 0 (P(n))$ \\
1. (Base) $P(0)$ 
\> \> \> \> \> \reason{Start state is $(0,0)$, $0$ is a multiple of $3$.} \\
2. (Inductive step) $\forall n \geq 0 (P(n) \Rightarrow P(n+1))$ \noreason \\
\> 1. Fix $n \geq 0$. \\
\> 2. Assume $P(n)$, that is, after $n$ steps, both jars have
multiples of $3$. \noreason \\
\> 3. $P(n+1)$, that is, after $n+1$ steps, both jars have multiples
of $3$. \noreason \\
            \reason{???} \\
\> 4. QED   \reason{Implication, UG} \\
3. QED      \reason{Induction}\\
}

\begin{breakperiods}
The argument for the ??? involves fixing a particular $n+1$-step
execution $q_0,q_1,\ldots,q_{n+1}$.  The first part except for the
final state is an $n$-step execution.  So we use the inductive
hypothesis to say that its final state, $q_n$, consists of two
multiples of $3$.  So consider what happens at the final step.  There
are $6$ cases.  Each one preserves the property.
\end{breakperiods}

\structuredproof[30ex]{
\> 3. $P(n+1)$, that is, after $n+1$ steps, both jars have multiples
of $3$.\noreason \\
\> \> 1. Fix $q_0,q_1,\ldots,q_{n+1}$, an execution with $n+1$
steps. \noreason\\ 
\> \> 2. In $q_n$, both jars have multiples of $3$. 
      \reason{Inductive hypothesis.} \\
\> \> 3. In $q_{n+1}$, both jars have multiples of $3$.  \\
\> \> \> 1. If the last move is to fill the little jar, then \ldots\\
\> \> \> 2. If the last move is to fill the big jar, then\ldots\\
\> \> \> 3. If the last move is to empty the little jar\ldots\\
\> \> \> 4. If the last move is to empty the big jar\ldots\\
\> \> \> 5. Pour from little to big\ldots\\
\> \> \> 6. Pour from big to little\ldots\\
\> \> \> 7. QED \reason{Cases} \\
\> \> 4. QED \reason{UG}\\
}
\begin{breakperiods}
Each of the six cases can be written out in detail, all are easy. 

Inductive proofs of properties of reachable states are very common in
reasoning about program and system correctness. 

\end{breakperiods}

\section{A two-dimensional puzzle}

\forstudents[another toy example of a state machine]{
Consider two-dimensional board, represented by the integer grid. 
That is, a piece starts out at $(0,0)$, and is allowed to move in any
of these 4 ways: 
\begin{enumerate}
\item (+2,-1)   Right 2, down 1
\item (-2,+1)   Left 2, up 1 
\item (+1,+3) 
\item (-1,-3) 
\end{enumerate}

\forlecture{(draw in 4 points)}

Let's ask the following: can the piece ever reach $(1,1)$? 
\forlecture{
Draw in some points. \\
Seems not---how to prove? \\
}
To answer this question we can represent the problem as state machine, with: 
\begin{itemize}
\item $Q = \{ (x,y) \mid x, y \in Z \}$ 

\item $Q_0 = \{ (0,0) \}$ 
\item 
$\delta$ consists of all $(x,y) \rightarrow (x',y')$, where $(x',y')$
is one of the following: 
\begin{enumerate}

\item $(x+2,y-1)$ 

\item $(x-2,y+1)$ 

\item $(x+1,y+3)$ 

\item $(x-1,y-3)$ 
\end{enumerate}
\end{itemize}

Let's  use induction to prove that this machine can't reach
$(1,1)$. 
We can't let $P(n) =$ ``the state after $n$ steps isn't $(1,1)$''. 
\Eg, $(-1,2) \rightarrow (1,1)$. 

So we need to strengthen the hypothesis.  How?  Try to observe
something about the pattern.  Draw more dots.  We find that all the
points are on a bunch of parallel lines:\\
$x + 2y = 0$ \\ 
$x + 2y = 7$ \\ 
$x + 2y = -7$ \\ 
Etc. This suggests that we try:
\begin{quote}
$P(n)$: The state after $n$ steps satisfies the condition that $x + 2y$ is a
multiple of $7$. 
\end{quote}


In more concise notation: $x + 2y \cong 0 \mod 7$. 
That is, the LHS and RHS have the same remainder on division by $7$. 

\structuredproof[45ex]{
Prove: $\forall n \geq 0 (P(n))$ \\
1. (Base) $P(0)$ 
\reason{Start state is $(0,0)$, $0 + 2 \times 0$ is a multiple of $7$.} \\
2. (Inductive step) $\forall n \geq 0 (P(n) \Rightarrow P(n+1))$ \\
\> 1. Fix $n \geq 0$. \\
\> 2. Assume $P(n)$, that is, after $n$ steps, $x + 2y$ is a multiple of $7$. \\
\> 3. $P(n+1)$, that is, after $n+1$ steps, $x + 2y$ is a multiple of $7$. \\
\> \> 1. Fix $q_0,q_1,\ldots,q_{n+1}$, an execution with $n+1$ steps. \\
\> \> 2. In $q_n$, $x + 2y$ is a multiple of $7$. 
      \reason{Inductive hypothesis.} \\
\> \> 3. In $q_{n+1}$, $x + 2y$ is a multiple of $7$. \\
\> \> \> 1. If the last move is $(+2,-1)$ then in $q_{n+1}$, $x + 2y$
is a multiple of $7$. \\
\> \> \> 2. If the last move is $(-2,+1)$ then in $q_{n+1}$, $x + 2y$
is a multiple of $7$. \\
\> \> \> 3. If the last move is $(+1,+3)$ then in $q_{n+1}$, $x + 2y$
is a multiple of $7$. \\
\> \> \> 4. If the last move is $(-1,-3)$ then in $q_{n+1}$, $x + 2y$
is a multiple of $7$. \\
\> \> \> 5. QED
         \reason{Cases} \\
\> 4. QED    \reason{Implication, UG} \\
3. QED \reason{Induction}\\
}

\noindent We'll show two of the four cases; the others are similar.
\structuredproof[45ex]{
\> \> \> 1. If the last move is $(+2,-1)$ then in $q_{n+1}$, $x + 2y$
is a multiple of $7$. \\
\> \> \> \> 1. Assume the last move is $(+2,-1)$. \\
\> \> \> \> 2. Let $x$ and $y$ denote the values in state $q_n$, $x'$ and
$y'$ the values in state $q_{n+1}$. \\
\> \> \> \> 3. $x' = x + 2$, $y' = y-1$. 
            \reason{Definition of the move} \\
\> \> \> \> 4. $x + 2y \cong 0 \mod 7$ 
            \reason{Inductive hypothesis} \\
\> \> \> \> 5. $x' + 2y' = (x+2) + 2(y-1) = x + 2y \cong 0 \mod 7$ \\
\reason{Algebra} \\
\> \> \> \> 6. In $q_{n+1}$, $x + 2y$ is a multiple of $7$. \\
\> \> \> \> 7. QED \reason{Implication}\\
}

\structuredproof[35ex]{
\> \> \> 3. If the last move is $(+1,+3)$ then in $q_{n+1}$, $x + 2y$
is a multiple of $7$. \\
\> \> \> \> 1. Assume the last move is $(+1,+3)$. \\
\> \> \> \> 2. Let $x$ and $y$ denote the values in state $q_n$, $x'$ and
$y'$ the values in state $q_{n+1}$. \\
\> \> \> \> 3. $x' = x + 1$, $y' = y + 3$. 
            \reason{Definition of the move} \\
\> \> \> \> 4. $x + 2y \cong 0 \mod 7$ 
            \reason{Inductive hypothesis} \\
\> \> \> \> 5. $x' + 2y' = (x+1) + 2(y+3) = x + 2y + 7 \cong 0 \mod 7$ \\
\reason{Algebra} \\
\> \> \> \> 6. In $q_{n+1}$, $x + 2y$ is a multiple of $7$. \\
\> \> \> \> 7. QED
            \reason{Implication}\\
}

\begin{corollary}
$(1,1)$ is not reachable.
\end{corollary}

Because $x+2y = 3$, which is not congruent to $0$ mod $7$.
}

\section{Sequential algorithm examples}

\begin{breakperiods}
Now we move from puzzles to sequential algorithms.  We describe a few
typical algorithms involving the data types we've studied so far.  We
prove a few simple properties.

\subsection{Greatest Common Divisor}

Given 2 positive natural numbers, $a, b \in N^+$, find their GCD.  We
already considered a recursive algorithm for this problem, and proved
it correct by induction.  Let's consider an iterative algorithm
instead.  It's not especially efficient---a more efficient version of
this appears as the Euclidean GCD algorithm in Rosen. 

Recall the key insight: we proved before that
$\ms{GCD}(x,y) = \ms{GCD}(y,x-y)$.  \forstudents{This follows because a
  positive integer divides 2 positive numbers if and only if it
  divides one of the numbers and their sum, if and only if it divides
  one of the numbers and their difference.} 

Thus, to compute the GCD, keep working values $x$ and $y$, initialized
at $a$ and $b$.  Then: 
\begin{itemize}
\item If $x = y$, that's the answer
\item Else if $x > y$, then subtract $y$ from $x$ and continue
\item Else if $y > x$, then subtract $x$ from $y$ and continue
\end{itemize}

\begin{example} 
Find $\ms{GCD}(112, 84)$ = 
\begin{enumerate}
\item $112 - 84 = 28$, reduce to $(28,84)$. 
\item $84 - 28 = 56$, reduce to $(28,56)$. 
\item $56 - 28 = 28$, reduce to $(28,28)$. 
\end{enumerate}
Now we are done; the answer is $28$. 
\end{example}

We already presented this as a recursive algorithm, when we
were covering inductive proofs for correctness of recursive
algorithms.  We can instead present it as a state machine:
\begin{itemize}
\item $Q = \{ (a,b,x,y) \mid a, b, x, y, \in N^+ \}$ 
\item $Q_0 = \{ (a,b,x,y) \mid x = a \mbox{ and } y = b \}$ 
\item $\delta$ is defined by $(a,b,x,y) \rightarrow (a',b',x',y')$,
  where: 
\begin{itemize}
\item $a' = a$ 
\item $b' = b$ 
\item Either $x > y$, $y' = y$ and $x' = x-y$, or $y > x$, $x' = x$,
  and $y' = y-x$
\end{itemize}
\end{itemize}

An advantage of this iterative algorithm (and its state machine) is
that unlike the recursive version, we don't need to keep a stack of
recursive calls.  We just keep track of our two current numbers.

We will prove that this state machine correctly computes
$\ms{GCD}(a,b)$.  It is convenient to break this claim down into two
parts:

\begin{description}
\item[Partial Correctness.] if we ever finish, then we have the right
  answer.  In other words, if we ever reach a point where $x = y$,
  then in fact $x = \ms{GCD}(a,b)$.
\item[Termination.] We actually finish. In other words, eventually, $x=y$. 
\end{description}

The meaning of 2 may not be so clear yet.  We'll come back to it in a
minute.

\subsubsection{Partial Correctness}

First let's prove the algorithm is correct.

We want to prove: In any reachable state, if $x=y$ then $x =
\ms{GCD}(a,b)$.  To prove this by induction, we have to strengthen
the statement to say something about intermediate states:  
\begin{quote}
Define $P(n)$: After any $n$-step execution, $\ms{GCD}(x,y) =
\ms{GCD}(a,b)$.  
\end{quote}

This says we are correctly reducing the problem to equivalent problems. 
The property we want is a corollary of $\forall n (P(n))$: 
\end{breakperiods}

\structuredproof{
Prove: in any reachable state $q$, $x=y$ in $q$ implies $x
=\ms{GCD}(a,b)$ in $q$. \noreason\\ 
1. Fix reachable state $q$. \\
2. Assume $x=y$ in $q$ \\
3. $\ms{GCD}(x,x) = \ms{GCD}(a,b)$ in $q$. \reason{By $P(n)$ just above} \\
4. $\ms{GCD}(x,x) = x$ in $q$ \reason{Number theory} \\
5. $x = \ms{GCD}(a,b)$ in $q$. \reason{Algebra} \\
6. QED \reason{Implication, UG}\\
}

Now we prove $P$ by induction:
\structuredproof{
Prove: $\forall n (P(n))$ \\
1. (Base) $P(0)$ 
\reason{After $0$ steps, $x = a$ and $y = b$.} \\
2. (Inductive step) $\forall n \geq 0 (P(n) \Rightarrow P(n+1))$ \\
\> 1. Fix $n \geq 0$. \\
\> 2. Assume $P(n)$, that is, after $n$ steps, $\ms{GCD}(x,y) =
\ms{GCD}(a,b)$.\noreason  \\
\> 3. $P(n+1)$, that is, after $n+1$ steps, $\ms{GCD}(x,y) =
\ms{GCD}(a,b)$. \noreason \\
\reason{???} \\
\> 4. QED    \reason{Implication, UG} \\
3. QED                        
\reason{Induction}\\
}

\begin{breakperiods}
To show ???, we can consider cases based on whether $x$ is less than
or greater than $y$. 
We don't have to consider the case where they're equal, because
nothing (no transition) can happen in this case. 
The two cases are analogous, so we just show one:
\end{breakperiods}
%[[[handout]]]
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXX\=    \kill
\> 3. $P(n+1)$, that is, after $n+1$ steps, $\ms{GCD}(x,y) = \ms{GCD}(a,b)$. \\
\> \> 1. Fix $q_0,q_1,\ldots,q_{n+1}$, an execution with $n+1$ steps. \\
\> \> 2. In $q_n$, $\ms{GCD}(x,y) = \ms{GCD}(a,b)$. 
      \> \> \> Inductive hypothesis. \\
\> \> 3. In $q_{n+1}$, $\ms{GCD}(x,y) = \ms{GCD}(a,b)$. \\
\> \> \> 1. If $x>y$ in $q_n$ then in $q_{n+1}$, $\ms{GCD}(x,y) = \ms{GCD}(a,b)$. \\
\> \> \> \> 1. Assume $x>y$ in $q_n$. \\
\> \> \> \> 2. Let $x$ and $y$ denote the values in state $q_n$, $x'$ and
$y'$ the values in state $q_{n+1}$. \\
\> \> \> \> 3. $x' = x-y$, $y'=y$
            \> Definition of the step \\
\> \> \> \> 4. $\ms{GCD}(x,y) = \ms{GCD}(a,b)$. 
            \> Inductive hypothesis \\
\> \> \> \> 5. $\ms{GCD}(x',y') = \ms{GCD}(x-y,y)$ 
            \> Plug in \\
\> \> \> \> 6. $\ms{GCD}(x-y,y) = \ms{GCD}(x,y)$ 
            \> Number theory fact \\
\> \> \> \> 7. $\ms{GCD}(x',y') = \ms{GCD}(a,b)$ 
            \> Algebra \\
\> \> \> \> 8. In $q_{n+1}$, $\ms{GCD}(x,y) = \ms{GCD}(a,b)$ \\
\> \> \> \> 9. QED
            \> Implication \\
\> \> \> 2. If $x<y$ in $q_n$ then in $q_{n+1}$, $\ms{GCD}(x,y) =\ms{GCD}(a,b)$. \\
\> \> \> \> \> Analogous to the previous case \\
\> \> \> 3. QED
         \> \> Cases
\end{tabbing}
So, this shows that the answer, if it's ever produced, is correct. 

\subsubsection{Termination}

\begin{breakperiods}
Now we turn to the second property, that the answer is actually produced
at some point, \ie, eventually $x=y$. 
It is not obvious what this means. 
To make sense of this, we need to make explicit the assumption that
says that steps keep happening---an execution doesn't just stop for no
reason. 
The only situation in which the execution is allowed to stop is when
it reaches a state where no steps are ``enabled'' (defined starting
from that state). 

For example, in our GCD algorithm, the execution can legitimately stop
when $x=y$, because no steps are defined.  But we want to assume that
the execution continues as long as $x \neq y$.

This leads to a definition: 
\begin{definition}
  An execution is $\ms{live}$ if it is infinite (in length), or if it
  is finite and no transitions are defined from the last state.
\end{definition}

So, the way to state the ``eventuality'' requirement of the GCD
algorithm is: 
\begin{lemma}
Any live execution of GCD contains some state in which $x=y$. 
\end{lemma}

How can we prove this?  One way is to notice that something about the
size of the problem being considered is decreasing at every step.  For
example, the sum $x+y$.  This sum can't decrease forever, because it
would eventually have to reach its minimum possible value $1+1$.  But
if it ever reaches this value, the goal is reached.  Also, if it
hasn't reached the goal, another step is enabled.

One way to express all this in a proof by contradiction, assuming that the
execution goes on forever and showing that we must eventually reach a
nonsense situation.
\end{breakperiods}

%[[[handout]]]
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXX\=    \kill
Prove: Any live execution of GCD contains some state in which $x=y$. \\
1. Assume not, that is, $\exists$ a live execution in which we never have $x=y$.\\
2. Fix $q_0,q_1,q_2,\ldots$, a live execution in which it is never the
case that $x=y$. \\
\> \> \> \> \> EI \\
3. $q_0,q_1,q_2,\ldots$ is either finite with $x=y$ in the final
state, or is infinite. \\
\> \> \> \> \> Definition of ``live execution'' \\
4. $q_0,q_1,q_2,\ldots$ is infinite 
\> \> \> \> \> By 3 and the fact that we don't have $x=y$. \\
5. $\exists$ a smallest value of $x+y$ that occurs in the states of
the execution. \\
\> \> \> \> \> Well-ordering \\
6. Fix $q_k$ to be a state in which this smallest value is reached. \\
\> \> \> \> \> EI \\
7. The value of $x+y$ in $q_{k+1}$ is smaller than the value of $x+y$ in $q_k$.\\
\> \> \> \> \> By the way the steps are defined \\
8. $q_k$ does not have the smallest value of $x+y$ in the execution. \\
\> \> \> \> \> By 7 \\
9. QED
\> \> \> \> \> Contradiction, 6 and 8.
\end{tabbing}

\begin{breakperiods}
\subsection{Graph coloring}

In the puzzles and algorithm so far, all data have been numbers. 
Computational processes can involve other data types too, 
for example, graphs. 

Consider an (undirected) graph $G=(V,E)$ in which no node has more
than $d$ neighbors (that is, the maximum degree is at most $d$).  As
we have seen, it is possible to color the vertices of $G$ with at most
$d+1$ colors, in such a way that no two neighboring nodes are colored
the same color.  In fact, we proved this last time, using an inductive
proof.

Now we show this again by producing an iterative algorithm that actually
does the coloring.  The idea is to start out with all the vertices
uncolored.  Then, repeatedly choose a vertex and color it, assigning
it any color that has not already been used for a neighbor.  We can
represent this (iterative) algorithm as a state machine.  To do so, we
assume $G=(V,E)$ is fixed at the beginnning, and define the following
state machine:

\begin{description}

\item[$Q=$] the set of functions from $V$ to $\ms{colors} \cup 
\{ \ms{null} \}$.  ($\ms{null}$ is a special value meaning ``not yet  
    colored''.)  


  \item[$Q_0=$] the function mapping all elements of $V$ to the value
$\ms{null}$. 


\item[$\delta$:]
In words:  The mapping in the new state is the same as that in the old
state, except that one node that was previously uncolored (value null)
gets assigned a color different from any that has already been
assigned to any of its neighbors. 
\end{description}

What do we want to prove about this? 
\begin{description}
\item[Partial Correctness.]  In any  reachable state where all
  vertices are colored, no 2 neighbors are ever colored the same
  color.  
\item[Termination.] Eventually we finish coloring all the vertices. 
\end{description}

We can prove partial correctness by proving a stronger claim: the no
neighbors have the same color in \emph{any} reachable state.  We prove
this by induction on the number of steps in an execution.  It is
clearly true in the initial state, because nothing is colored.  Now
considr the inductive step.  If no two neighbors are colored the same
color, and we color one more node as allowed by $\delta$, then again
no two neighbors are colored the same color.  The new step colors a
node a different color from any of its neighbors, so doesn't introduce
any other counterexamples.  It doesn't change any of the previous
colorings, so they still yield no counterexamples.

To prove termination, remember that we only consider live executions
(Either infinite, or finite and nothing enabled in final state).
Let's consider for something that decreases at every step: namely, the
number of uncolored nodes.  It starts at $n$, and any step reduces by
$1$.  So the number can't decrease forever.  But we haven't colored
all the nodes, another step is always enabled.
\end{breakperiods}

%[[[handout]]]
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXX\=    \kill
Prove:  In any live execution, there exists some state in which all
the nodes are colored. \\
1. Fix $q_0,q_1,q_2,\ldots$, a live execution. \\
2. $q_0,q_1,q_2,\ldots$ is either finite with no step enabled in the
final state, or is infinite. \\
\> \> \> \> \> Definition of ``live execution''.\\
3. $q_0,q_1,q_2,\ldots$ isn't infinite 
\> \> \> \> \> The number of uncolored nodes decreases at \\
\> \> \> \> \>  every step, but can't go below $0$. \\
4. $q_0,q_1,q_2,\ldots$ is finite with no step enabled in the final state.\\
\> \> \> \> \> By 2. and 3. \\
5. All nodes are colored in the final state. \\
\> 1. If not all nodes are colored in the final state, then some step
is enabled. \\
\> \> \> \> \> Any uncolored node can be colored; \\
\> \> \> \> \> there are enough colors. \\
\> 2. QED
   \> \> \> \> Contradiction (5.1. and 4.) \\
6. QED
\> \> \> \> \> EG, UG
\end{tabbing}
EG:  We found a state with the property we want, so one exists. \\
UG:  Showed the property for a generic execution, so holds for all
executions. 

(Note that step 3 encapsulates the same proof as we did for GCD, that
we cannot go on forever).\\


\section{Programming Notation for Sequential Algorithms}
\begin{breakperiods}

\subsection{Overview}

Sequential algorithms are usually presented (in textbooks, papers),
not by describing their states and transitions, but using a
programming-language-style notation. 
Rosen, Appendix B, gives a typical such program notation. 
The basic constructs are assignment statements, conditionals,
loops. 
There are also statement grouping constructs like blocks and procedures. 
Procedures may have side-effects. 
Procedures can call other procedures, possibly recursively. 
The style of these programs is like PASCAL, Algol, or C. 
These programs denote step-by-step computational processes,
\ie\ state machines. 

\subsection{GCD, revisited}

Here is an iterative GCD algorithm written in a simple pseudo-language:
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXX\=    \kill
procedure $\ms{GCD}(a,b \in N^+)$ \\
declare $x,y \in N^+$ \\
$x := a$ \\
$y := b$ \\
while $x \neq y$ do \\
\> if $x > y$ then $x := x-y$ \\
\> else $y := y-x$ \\
return $x$
\end{tabbing}
This program is written in an {\em iterative\/} style, executing a
loop.

Any program can be translated into a state machine, with states and
transitions.  Here, the state consists of the values of variables $a,
b, x, y$ plus a program counter that says which line of the program we
are currently executing.  There may be additional bookkeeping
information in some cases.  We can prove the ``right answer'' and
termination properties for this state machine.

It's typical in state machines that represent programs to have
properties include mention of program counters and loop index
variables.  We say things like ``If control of processing is at a
particular place in the program code, then predicate $P$ (of the
program variables, possible bookkeeping variables) is true.

In fact, sometimes when properties are of this form, people {\em
  annotate\/} their programs, writing down the properties that hold at
the appropriate points in the code.  This is helpful in verifying the
correctness of code (and debugging what's not correct).


\subsection{Recursion}

The translations from pseudo-code to state machine were very simple
for GCD.  They get more complicated when the program includes
procedure calls, and especially recursion.  For instance, consider GCD
rewritten using (recursive) procedure calls:
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXX\=    \kill
procedure $\ms{GCD}(a,b \in N^+)$ \\
declare $\ms{ans} \in N^+$ \\
if $a = b$ then $\ms{ans} := a$ \\
else \\
\> if $a > b$ then $\ms{ans} := \ms{GCD}(a-b,b)$ \\
\> else $\ms{ans} := \ms{GCD}(a,b-a)$ \\
return $\ms{ans}$
\end{tabbing}
This recursive programming style is typical of languages like LISP or
Scheme. 

\begin{example} Computing $\ms{GCD}(112, 84)$ 
\begin{itemize}

\item We starts with $a = 112$, $b = 84$. 
The test says $a > b$, so we call $\ms{GCD}(28,84)$. 
We remember that when this returns, we want to set your $\ms{ans}$ to
that value and return it to the caller. 

\item Now we start over, with a new $a$ and $b$: This $a$ gets set to $28$,
this $b$ to $84$. 
Now the test says $b > a$, so call $\ms{GCD}(28,56)$ 

\item Another $(a,b)$, $a$ set to $28$, $b$ to $56$.  So it calls
  $\ms{GCD}(28,28)$. 


\item This one sets its $\ms{ans} := 28$, returns that value to its caller. 
That caller puts the result in ITS $\ms{ans}$, returns to ITS caller. 
Etc., top-level procedure returns value of its $\ms{ans}$ to the
original caller. 
\end{itemize}
\end{example}


How can we translate this into a state machine? 

First, why would you want to?  Well, in order for a recursive program
to execute, it must be translated into something machine-like.  That's
what a compiler does.  And actual computers are fundamentally state
machines.

We can't construct a state machine as we did before, letting the state
consist of just the program variables and a program counter.  Why?
Because nested calls of the recursive procedure are actually active at
the same time.  They use their own copies of arguments, program
variables, etc.  \Eg, in the example above, we use a separate $a$, $b$
and $\ms{ans}$ for each call.  

A state machine describing how this algorithm actually executes needs
to maintain separate copies of these variables.  They can be arranged
in a ``stack'', where we ``push'' variables on the stack when we make
the calls and ``pop'' them from the stack when we return.  This is
what the computer implementing the recursive algorithm does anyway.

For proving properties of such a recursive algorithm, you could use
the techniques we've been using so far: 
\begin{itemize}
\item  Induction on the number of steps in the state machine. 
\item  Defining a measure that decreases with each step. 
\end{itemize}
But this can get pretty complicated, because of the stack
manipulations.  So it's not usually done---such state-machine-style
proofs are usually done for state machines that are derived from
``iterative'' (loop-style) programs.  For recursions, we often resort
to the direct inductions you've seen in the past.

\end{breakperiods}

\section{Reflexive, transitive closure of relations}

\forstudents[Transitive Closures]{
\begin{breakperiods}
Here's another example---a computational process involving relations.
We'll consider a simple algorithm to compute the reflexive, transitive
closure of a binary relation $R$ on a finite set.  Recall that this is
equal to $I \cup R \cup R^2 \cup R^3 \cup \ldots R^n$, where $n$ is
the number of elements in the set.  Here, $I$ is the identity
relation, which just relates $(x,x)$ for every $x$.  We also can write
it as write as $I \cup R \cup R^2 \cup R^3 + \ldots$ (infinite union),
but recall that nothing new gets added after the $R^n$ term.

One way to compute this is to first calculate $I \cup R$. 
This new relation relates $x$ to $y$ provides that $x=y$ or $(x,y) \in
R$, that is, if $x$ is related to $y$ by $0$ or $1$ ``steps''. 

Now square the result: gives $(I \cup R)^2$, which is equal to $I \cup
R \cup R^2$.  This describes the existence of paths of length at most
$2$.  Square it again, yielding all paths of length at most 4.  Each
time we square, we double the length of the paths we've ``discovered''
in the relation.  So it doesn't take very long for this to stabilize.
\\ Only $\lceil \log{n} \rceil$ steps.   This is the relation analogue
of the fast exponentiation algorithm we studied for RSA.

\begin{example}
$R$ is the relation on set $S = \{ a,b,c,d,e \}$ consisting of the pairs
$(a,b)$, $(b,c)$, $(c,d)$, $(d,e)$. \\
Initially, $T$ contains $R$ augmented with the pairs $(a,a)$, $(b,b)$,
$(c,c)$, $(d,d)$, $(e,e)$. \\
First step squares $T$, which adds in the two-step paths $(a,c)$,
$(b,d)$ and $(c,e)$. \\
Next step squares $T$ again, which yields the 3-step and 4-step paths
$(a,d)$, $(b,e)$, $(a,e)$. \\
\end{example}

We can formalized this algorithm as a state machine: 
Fix an underlying finite set $S$, $n$ elements. 
\begin{itemize}

\item $Q = \{ (R,T) \}$, both binary relations 

\item $Q_0 = \{ (R,T) \mid T = R \cup I \}$ 

\item $\delta$: Steps of the form $(R,T) \rightarrow (R',T')$, where
$R' = R$, $T' = T^2$. 
\end{itemize}
As described, the state machine keeps squaring forever. 
So the only live executions are infinite. 
However, after a while, the state stops changing (self-loops). 

What might we prove about this state machine? 
\begin{enumerate}

\item  After $\lceil \log{n} \rceil$ steps, $T$ is the reflexive, 
transitive closure of $R$. 
This actually 
follows from more general property: 

\item  For any $k \geq 0$, after $k$ steps, $T = I \cup R \cup \ldots
  \cup R^{2^k}$.  
\end{enumerate}

Property 2 can be proved by induction on $k$, as usual. 
Relational algebra is used in the inductive step. 

Also, notice that all the live executions are infinite---another step
can always be done (will have self-loops at the end). 
So, in any live execution, eventually get $T =$ the reflexive, transitive
closure. 

Notice that in this example I didn't talk about how the relation was
actually represented (by lists, matrices, etc.) 
The example just talks about the high-level, abstract process of
computing the reflexive, transitive closure of a binary relation
by successive squaring.  
It doesn't talk about the details of doing the matrix squaring in
terms of lower-level matrix element operations. 
That could be done in another, more detailed state machine.
\end{breakperiods}

\subsection{Expressing as a program}

Here's a description of the abstract reflexive, transitive closure
algorithm using pseudocode like Rosen's. 

Assume positive integer $n$ and set $S$ are fixed\. 
Let $I$ be a constant denoting the identity relation on $S$. 
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXX\=    \kill
procedure reflexiveTransitiveClosure(R: binary relation on S) \\
declare T: binary relation on S \\
$T := R \cup I$ \\
while true do $T := T^2$
\end{tabbing}
Here, the loop executes forever, so the procedure never returns\. 
To get a return value, put a stopping condition in the loop:
\begin{tabbing}
XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXX\=    \kill
procedure transitiveClosure($R$: binary relation on $S$) \\
declare $T$: binary relation on $S$ \\
$T := R \cup I$ \\
for $i := 1$ to $\lceil \log{n} \rceil$ do $T := T^2$ \\
return $T$
\end{tabbing}

What's in the state? 
$T$ and $R$ of course.
A little more information is needed, for bookkeeping: 
An indication of what the processing is up to---the beginning,
at the loop, at the end. 
And if at the loop, which pass. \\
For example, we might include: 
\begin{itemize}
\item
A {\em program counter\/} saying where we're up to, in the
statements of the program, and 
\item
A {\em loop index counter\/}, keeping track of which pass of the
loop we're up to, when we're doing the loop. 
\end{itemize}
With this extra information, we can describe the allowable steps as state
transitions $(T,R,\ms{pc},i) \rightarrow (T',R',\ms{pc}',i')$. \\
These can be of several different kinds, for example:
\begin{itemize}
\item
Initialization of $T$: \\
$\ms{pc} = \ms{begin}$, $T' = R \cup I$, $R' = R$, $\ms{pc}' =
\ms{at-loop}$, and $i' = 1$.
\item
The $i$th pass through the loop, $i \leq \lceil \log{n} \rceil$: \\
$\ms{pc} = \ms{pc}' = \ms{at-loop}$, $T' = T^2$, $R'=R$, and $i'=i+1$. 
\item
Moving to after the loop: \\
$\ms{pc} = \ms{at-loop}$, $i > \lceil \log{n} \rceil$,
$T' = T$, $R'=R$, $\ms{pc}' = \ms{at-end}$, and $i'=0$. 
\end{itemize}
Even though the algorithm is represented a little differently, we
would still like to prove the same kinds of properties as before. \\
Properties come out looking slightly different. \\
\eg, might want to prove: \\
If $\ms{pc} = \ms{at-loop}$ then $T = I \cup R \cup R^2 \cup \cdots
\cup R^{2^{i-1}}$..\\
\\
It's typical in state machines that represent programs to have properties
include mention of program counters and loop index variables. \\
Say things like ``If control of processing is at a particular place
in the program code, then predicate $P$ (of the program variables,
possible bookkeeping variables) is true. \\
\\
In fact, sometimes when properties are of this form, people {\em
annotate\/} their programs, writing down the properties at the
appropriate points in the code. \\
\eg, can write the property: \\
If $\ms{pc} = \ms{at-loop}$ then $T = I \cup R \cup R^2 \cup \cdots
\cup R^{2^{i-1}}$..\\
by just writing the statement $T = I \cup R \cup \cdots R^{2^{i-1}}$
someplace in the code,
corresponding to the beginning of the execution of the body of the
loop. 

% A slight problem here. 
% What we really want is to have this statement just prior to the loop
% test. 
% But there's nowhere convenient to write this...
% Anyway, the general point is still worth making. 
}


\end{document}

\section{Abstract system descriptions}

One more type of example---a state machine used as an
abstract description of a complex system. \\
(Nondeterministic).

\subsection{Overview}

A caching system, may be used in a multiprocessor machine or a
distributed system. \\
\\
Has a ``memory'', which contains the latest versions of all data in
some application. \\
Also has one or more ``caches'', which contain some versions of some
of the data. \\
These caches are intended for fast access by individual clients. \\
\\
Examples:  Web pages.  Numerical data values in a multiprocessor. \\
\\
Model uses three basic sets:  $A$ ($\ms{addresses}$), $V$
($\ms{values}$), and $I$ ($\ms{locations}$) \\
Assume $V$ has a distinguished initial value $v_0$. \\
\\
The system contains: \\
$\ms{mem}$, a (total) function from $A$ to $V$ \\
$\ms{cache}$, a function from $A \times I$ to $V \cup \{ \ms{null} \}$ \\
\\
The $\ms{cache}$ function tells what value, if any, is held for each
memory address, at each location. \\
The cache for location $i$ is supposed to be used by client $i$. 

\subsection{Weak caching system}

What we want to express in the model: \\
The memory can be updated at any time. \\
This may leave any of the caches out-of-date. \\
Also, at any time, the latest value may be copied from the memory to a
cache, overwriting any older value that's there. \\
Also, at any time, a value may be dropped from a cache. \\
\\
As a state machine: \\
$Q$: $\{ (\ms{mem}, \ms{cache})$, of the types described above. \\
$Q_0$: $\ms{mem}$ maps everything to $v_0$, $\ms{cache}$ maps everything to $\ms{null}$. \\
$\delta$: 
$(\ms{mem}, \ms{cache}) \rightarrow (\ms{mem}', \ms{cache}')$, where
at least one of the following cases holds: \\
\\
1. New memory is same as old memory except that at most one of the addresses
gets a new value.  Caches unchanged. \\
$\exists a \in A, \forall b \in A - \{ a \} [ \ms{mem}'(b) = \ms{mem}(b)]$, and
$\ms{cache}' = \ms{cache}$.
\\
Actually, it's usually easier to write this in assignment form, in which
you just say what's changed: \\
$\ms{mem}(a) :=$ arbitrary $V$ (not $\ms{null}$) \\
\\
2. One address in $\ms{cache}$, at one location, gets updated from memory: \\ 
$\ms{cache}(a,i) := \ms{mem}(a)$ \\
\\
3. One value gets dropped from a $\ms{cache}$, at one location: \\
$\ms{cache}(a,i) := \ms{null}$ \\
\\
Nondeterministic. \\
\\
What might one prove about this service?  Not very much...\\
\\
Basic correctness: \\
Maybe something about $\ms{mem}$ having the most up-to-date value. \\
LTTR \\
\\
Eventuality: \\
Must be careful here. \\
Tricky, and we won't have time to do this so carefully in this course. \\
\Eg, we might want to say that the caches eventually get all the
values that are put in memory and never overwritten. \\
But to say this, we must first say which steps must happen. \\
\\
For sequential programs, I used the notion of ``live'' execution to
express this; it says that something keeps happening if anything is
enabled. \\
But that general definition doesn't usually give what we want for
service models. \\
\Eg, we'd like to allow the case where everything stabilizes and no
new memory updates happen. \\
But we'd like to disallow the case where memory updates keep
happening and the caches never get updated. \\
\\
Saying these kinds of things is a little complicated, and I won't sat
more about it here. 
% [[[What it is: Treat the memory updates as inputs; these have no
% requirement that they eventually occur.  For each address in each
% cache, have a separate ``task'' that gets turns to take steps
% infinitely often. At each turn, it has to perform a step of that
% task if any such step is enabled.
% The enabling condition for the task is that the value in the
% indicated cache for the indicated address differs from the value in
% memory for the same address. ]]]

\subsection{Strong caching system}

The weak caching system allows clients to obtain out-of-date information. \\
\Eg, memory value updated, but client still has old value. \\
Sometimes we want to make sure the clients never get old information,
which we can do by making sure the caches are never out-of-date. \\
One thing we could do is to make sure that, whenever the memory is updated,
the caches are cleaned out. \\
This just involves modifying the memory update step a little: \\
\\
$\ms{mem}(a) :=$ arbitrary $V$ (not null), and for all $i$, $\ms{cache}(a,i) := \ms{null}$ \\
% More generally, would only allow the memory to be updated if the
% caches have their values set to null.  
\\
Now get a stronger guarantee, which expresses the idea that
clients never see old values. \\
In all reachable states: \\
\\
$\forall a, i$, either $\ms{cache}(a,i) = \ms{mem}(a)$ or
$\ms{cache}(a,i) = \ms{null}$ \\
\\
In other words: \\
If $\ms{cache}(a,i) \neq \ms{null}$ then $\ms{cache}(a,i) = \ms{mem}(a)$. \\
\\
Also, could mix and match---some weak and some strong caches.  \\
The idea here is that the clients could say if they care whether their
values are always up-to-date. \\
Of course, if they say yes to this, they may sometimes have to wait to
get the new value.

\section{Kinds of properties proved for computational processes}

We've now seen many examples of computational processes, modeled as
state machines. \\
Now let's take a closer look at the kinds of properties we proved about
the computational processes. \\
Most of these fall into certain standard categories: 
\begin{enumerate}
\item
Some predicate (of the state variables) is true in all reachable states: \\
\\
Examples: Die Hard: The contents of each jar is a multiple of 3 gallons. \\
\\
$2$-dimensional puzzle: $x + 2y$ is a multiple of $7$. \\
\\
$\ms{GCD}$: $\ms{GCD}(x,y) = \ms{GCD}(a,b)$. \\
\\
Graph coloring: No $2$ neighbors are ever colored the same color. \\
\\
Strong caching: 
If $\ms{cache}(a,i) \neq \ms{null}$ then $\ms{cache}(a,i) = \ms{mem}(a)$. \\
\\
\item
Eventuality properties: \\
\\
Examples: $\ms{GCD}$: Eventually get $x=y$. \\
\\
Graph coloring: Eventually color all the vertices. \\
\\
Relation reflexive transitive closure: \\
Eventually get $T$ equal to the reflexive transitive closure of $R$. \\
\\
But note that some examples don't have termination properties, \eg,
Die Hard may go on forever. \\
Expect cache example to go on forever. 
\item
Time bound properties: \\
\\
Examples: Relation reflexive transitive closure: \\
After $\lceil \log{n} \rceil$ steps, $T$ is the reflexive transitive closure of
$R$. 
\end{enumerate}
These kinds of properties are so common that people have developed
stylized ways of stating and proving them, languages for expressing
them, computer tools for checking them,...\\
\\
The most important of the three kinds of properties is the first. \\
Such properties are called {\em invariants\/}. 
Focus on these next time. 


\end{document}

\endinput

