%The following hack from Frank.
%
% \makeatletter
% \def\providetabstops #1{%
%    \count@#1\relax
%    \newdimen\@gtempa
%    \chardef\@firsttab=\the\allocationnumber
%    \loop
%      \newdimen\@gtempa
%      \advance\count@\m@ne
%      \ifnum\count@>\z@
%    \repeat
%    \chardef\@maxtab=\the\allocationnumber
% }
% \makeatother
% 
% \providetabstops{20}


\documentclass[fleqn,leqno]{article}
\usepackage{hypertlabook}
\pdftitle{Principles}
\file{principles}
\makeindex

%%% Hack for showing index elements.  Suppresses writing
%% of the idx file.
%%
%% \let\mmath=\ensuremath
%% \def\icmd#1{\csname#1\endcsname}
%% \renewcommand{\tindex}[2]{\marginpar{\red #2 (#1)}}
%% \renewcommand{\ctindex}[3]{\marginpar{\red #2 (#1)}}


% The following doesn't work.
% \let\xtindex=\tindex
% \let\xctindex=\ctindex
% \renewcommand{\tindex}[2]{\xtindex{#1}{#2}{\let\mmath=\ensuremath
% \def\icmd##1{\csname##1\endcsname}%
% \marginpar{\red #2 (#1)}}}
% \renewcommand{\ctindex}[3]{\xctindex{#1}{#2}{#3}{\let\mmath=\ensuremath
% \def\icmd##1{\csname##1\endcsname}%
% \marginpar{\red #2 (#1)}}}




\setcounter{section}{\principlestrack}
\begin{document}

\renewcommand{\contentsname}{The \emph{Principles} Track\protect\target{top}}
\addtocounter{section}{-1}

\showversions
\tableofcontents
\hideversions
\vfill 
\newpage
\vspace*{-\baselineskip}

%try
\section{Mutual Exclusion}


\subsection{The Problem}

The mutual 
  \ctindex{1}{mutual exclusion}{mutex}%
exclusion problem was introduced by Edsger
 \ctindex{1}{Dijkstra, Edsger}{dijkstra}%
 Dijkstra in his
article \emph{Solution of a Problem in Concurrent Control}, published
in the \emph{Communications of the ACM}, Volume~8, Number~9
(September, 1965), page~569.  This seminal article launched the field
of concurrent algorithms.  Here is how Dijkstra began his statement of
the problem.
\begin{itemize}
\item[]
[C]onsider $N$ computers, each engaged in a
process which, for our aims, can be regarded as cyclic. In
each of the cycles a so-called ``critical 
  \tindex{1}{critical section}%
  \ctindex{1}{section!critical}{section-critical}%
section'' occurs and
the computers have to be programmed in such a way that
at any moment only one of these $N$ cyclic processes is in
its critical section. 
\end{itemize}
Dijkstra wrote about multiple computers, but the application he had in
mind was multiple processes running on the same computer.  The mutual
exclusion problem has come to be stated in terms of processes 
 \marginpar{\popref{process-vs-thread}{What is a process?}}
rather than computers, so that is the terminology that we will use.
%
The property that there is never more than one process in its
critical section is called \emph{mutual exclusion}. It is, of course,
an invariance property.

Dijkstra next stated what operations the processes could use.
\begin{itemize}
\item[] In order to effectuate this mutual
exclusion of critical-section execution the computers can
communicate with each other via a common 
 \marginpar[.5]{\commentcolor
   Dijkstra disliked the anthropomorphic term \emph{memory}
   and usually\\ wrote \emph{store} instead.}%
 \tindex{1}{store}%
store. Writing
a word into or nondestructively reading a word from this
store are undividable operations; i.e., when two or more
computers try to communicate (either for reading or for
writing) simultaneously with the same common location,
these communications will take place one after the other,
but in an unknown order.
\end{itemize}
%
Mutual exclusion is central to modern concurrent programming.  
% 
% Today's shared-memory multiprocess programs keep different processes
% from simultaneously accessing the same data by putting code that
% accesses the data into critical sections.  Modern programming
% languages provide constructs or library procedures for implementing
% mutual exclusion, using special instructions provided for the purpose
% by multiprocessor computers.  However, a new hardware or software
% architecture often requires a new algorithm to implement mutual
% exclusion.
% 
Today, multiprocess computers provide special instructions for
implementing mutual exclusion.  That was not the case in 1965.  The
only interprocess communication primitives were reading and writing a
shared memory register---operations that Dijkstra assumed to be atomic
actions.  Today, the \emph{mutual exclusion problem} is not restricted
to solutions based only on reading and writing shared memory.  For
example, there are distributed solutions in which processes
communicate with messages.  Of course, the problem becomes trivial if
we can use sufficiently powerful communication primitives.

Dijkstra next stated four requirements that a solution must satisfy.
The first was:
%
\begin{itemize}
\item[(a)] The solution must be symmetrical between the $N$ computers;
as a result we are not allowed to introduce a static priority.
\end{itemize}
%
%
% I don't know what Dijkstra meant by ``symmetrical''.  I can't think of
% a precise definition that neither is vacuous nor makes the problem
% unsolvable.  This was uncharacteristic of Dijkstra, who chose words
% carefully and used them precisely.  However, I think we can infer what
% he intended from the second clause, which disallows static priority.
% 
% Consider an execution of an algorithm in which just two processes try
% to enter their critical sections.  Suppose the processes execute ``in
% lock step'', alternately executing atomic steps.  How does the
% algorithm choose which one enters its critical section first?  There
% are two possibilities:
% \begin{itemize}
% \item The choice depends on the identity of the processes.  This
% is what Dijkstra means by static priority.
% 
% \item The choice depends on which one takes the first step.  This is
% what Dijkstra requires.  (This does \emph{not} mean that the
% process that takes the first step must be the one to enter its
% critical section first.)
% \end{itemize}
% When two processes both execute the same type of operation, there is
% only one way for them to determine which execution was performed
% first: the two operations must be writes of different values to the
% same memory location.  Hence, (a) requires that two or more processes
% write to the same memory location.
% 
% I find this requirement unsatisfying.  For reasons that will become
% clear much later, I am more interested in algorithms---especially
% mutual exclusion algorithms---in which a memory location is written by
% only one process.  I will therefore ignore requirement (a).  In fact,
% this requirement has largely been forgotten.
% 
%
Requirement (a) is the only part of this article that has turned out
not to be important, and it has been ignored.  We too will ignore it.
The next requirement was:
\begin{itemize}
\item[(b)] Nothing may be assumed about the relative speeds of the $N$
computers; we may not even assume their speeds to be constant in time.
\end{itemize}
This requirement is now taken for granted when studying concurrent
algorithms, and it requires no discussion.  Explicitly stating it for
the first time is one of the major contributions of the article.
The next requirement was:
\begin{itemize}
\item[(c)] If any of the computers is stopped well outside its
critical section, this is not allowed to lead to potential blocking of
the others.
\end{itemize}
The part of a process's code ``well outside its critical section'' is
now called the \emph{noncritical 
    \tindex{1}{noncritical section}%
    \ctindex{1}{section!noncritical}{section-noncritical}%
section}.  Implicit in this requirement is that a process is allowed
to stop in its noncritical section.  Requirement~(c) is a fundamental
part of the mutual exclusion problem.  Removing it makes the problem
much easier, both in principle and in practice.  For example, it is
quite easy to write an algorithm in which processes take turns
entering the critical section.  This satisfies mutual exclusion, but
stopping one process prevents the other from entering its critical
section more than one additional time, so it doesn't satisfy~(c).  In fact, we
have already written such an algorithm.
\begin{hproblem}{mutex-answer1} \sloppy
Show that a solution to the alternation problem, as described
in \rref{main}{\xlink{alt-revisited}}{Section~\xref{alt-revisited}},
satisfies the mutual exclusion condition for $N=2$, where
the $put$ and $get$ operations are the critical sections.
Generalize this to show that a round-robin synchronization
algorithm (\rref{main}{\xlink{round-robin}}{Section~\xref{round-robin}})
satisfies mutual exclusion for an arbitrary positive
integer $N$.
\end{hproblem}
%
Dijkstra's final requirement was:
\begin{itemize}
\item[(d)] If 
 \target{dijkstra-d}%
more than one computer is about to enter its critical
section, it must be impossible to devise for them such finite speeds,
that the decision to determine which one of them will enter its
critical section first is postponed until eternity.  In other words,
constructions in which ``After you''--``After you''--blocking is
still possible, although improbable, are not to be regarded as valid
solutions.
\end{itemize}
This asserts a liveness property that the algorithm must satisfy.
Today, this property would be expressed as: if at least one process is
trying to enter its critical section, then some process must
eventually enter its critical section.  However, it would be 10 years
before the concepts of safety and liveness were identified, and the
meaning of ``eventually'' would not have been clear to readers at the
time.  Dijkstra explained the requirement in a somewhat roundabout way
by saying what was not allowed, an explanation that readers were sure
to understand.

What Dijkstra called \emph{after-you, after-you blocking} is now known
as 
  \tindex{1}{livelock}%
\emph{livelock}.  Requirement (d) is now called
\emph{deadlock 
  \tindex{1}{deadlock freedom}%
freedom}.  This is a somewhat confusing name, since
deadlock usually means a state in which no process can take a step,
which is not the case in the \emph{livelock} that Dijkstra ruled out.

% When we 
% specify mutual exclusion more precisely, we will see that the name is
% not 
%  \marginpar[2]{\large\red Reference to unwritten text.}
% inappropriate.

Deadlock freedom assures only that some process enters its critical
section.  It doesn't assure that any particular process does.  
It allows the possibility that some process waits forever
trying to enter its critical section while other processes keep
entering and leaving their critical sections.  Such a process is said
to be \emph{starved}.  (The metaphor of starvation comes from the
\emph{dining 
  \tindex{1}{dining philosophers problem}%
philosophers problem}, another multiprocess
synchronization problem invented by Dijkstra.)  A stronger requirement
than deadlock freedom is 
  \target{starvation-freedom}%
\emph{starvation 
  \tindex{1}{starvation freedom}%
freedom}, which requires
that any process that tries to enter its critical section eventually
does so.  The solution that Dijkstra presented in his 1965 paper is
deadlock free but not starvation free.


\subsection{The One-Bit Protocol}

\subsubsection{The Protocol}

   \tindex{1}{One-Bit Protocol}%
Dijkstra's original algorithm uses a simple protocol for ensuring
mutual exclusion that appears in a number of subsequent algorithms.  I
call it the \emph{One-Bit Protocol}.  Here is how it works in the case
of two processes: Each process maintains a Boolean value.  It can
enter its critical section only by setting its value to $\TRUE$ and
reading the other process's variable equal to $\FALSE$.

Let's write the One-Bit Protocol more precisely.  Let the processes be
named 0 and 1 and let their Boolean values be $x[0]$ and $x[1]$.  Using
PlusCal notation, the algorithm of process $self$ is as follows.
(Note that $1-self$ is the process other than process $self$.)
\begin{display}
\begin{tabbing}
$e1$: \= $x[self] := \TRUE$ ; \V{.2}
$e2$: \> \pif\ $(\,~x[1\!-\!self]\,)$ \{ $cs$: critical section \} 
\end{tabbing}
\end{display}
We don't specify the critical section, except that we assume it does not
change the value of the array (function) $x$.  In particular, it need
not be an atomic action.  (In PlusCal notation, it could contain
labels.)

It's easy to see that this protocol ensures mutual exclusion.  Here's
a simple proof by contradiction.  
\begin{display}
Assume that both processes are in their critical sections.  The first
one that entered its critical section, call it process $i$, did so
after setting $x[i]$ to $\TRUE$.  Process $1-i$ entered the critical
section after $i$, so it read $x[i]$ in its \textbf{if} test after
process $i$ had set $x[i]$ to $\TRUE$.  Hence the read of
$x[i]$ by process $1-i$ in its \textbf{if} test obtained the value
$\TRUE$, so it couldn't have entered its critical section---contradicting
the assumption that both processes are in their critical section.
\end{display}
This is a correct and convincing proof.  It is a 
 \tindex{1}{behavioral proof}%
 \ctindex{1}{proof!behavioral}{proof-behavioral}%
\emph{behavioral}
proof, based on reasoning about the order in which operations are
executed.  This proof is quite informal.  Behavioral proofs can be
made more formal, but I don't know any practical way to make them
completely formal---that is, to write executable descriptions of real
algorithms and formal behavioral proofs that they satisfy correctness
properties.  This is one reason why, in more than 35 years of writing
concurrent algorithms, I have found behavioral reasoning to be
unreliable for more complicated algorithms.  I believe another reason
to be that behavioral proofs are inherently more complex than
state-based ones for sufficiently complex algorithms.  This leads
people to write less rigorous behavioral proofs for those
algorithms---especially with no completely formal proofs to serve as
guideposts.


To avoid mistakes, we have to think in terms of states, not in terms
of executions.  So, I will show you how to write a state-based proof.
Since I have not precisely specified the One-Bit Protocol (for
example, by writing a complete PlusCal algorithm), no proof of its
correctness can be completely formal.  However, even the informal
state-based proof is long and boring.  Please don't be discouraged by
this.  It's important to learn how to write a very rigorous
state-based proof, because that's the kind of proof you'll have to
write if you want to be sure that a more complicated algorithm is
correct.  Exciting proofs concentrate on the interesting parts that
display insight, skimming over unimportant details.  Unfortunately,
our insight is often not as good as we think, and we can too
easily miss a fatal flaw lurking in neglected details.  Although
finding a state-based proof requires insight, checking it does not.  A
careful attention to details is all it takes to avoid mistakes.

Still, behavioral reasoning provides a different way of thinking about
an algorithm, and thinking is always helpful.  
% I will therefore later
% show
%   \marginpar{\large\red Reference to unwritten text.}
% how behavioral reasoning can be made more rigorous.  
Behavioral reasoning is bad only if it is used instead of state-based
reasoning rather than in addition to it.



\subsubsection{An Assertional Proof} \xlabel{two-bit-protocol-proof}

Mutual exclusion is an invariance property.  Let $InCS(i)$ be the
state predicate that is true iff process $i$ is in its critical
section.  Mutual exclusion asserts the invariance of the state
predicate ${MutualExclusion}$, defined for our two processes by
 \[  {MutualExclusion} == ~(InCS(0) /\ InCS(1)) \]
Suppose that the complete algorithm is described by an initial
predicate $Init$ and next-state action $Next$.  We saw in
\rref{main}{\xlink{proving-invariance}}{Section~\xref{proving-invariance}}
that we prove a formula $Inv$ to be an invariant of the algorithm by
proving:
\begin{enumerate}
\item[I1.] $Init => Inv$
\item[I2.] $Inv /\ Next => Inv'$
\end{enumerate}
Condition~I1 asserts that $Inv$ is true initially, and condition~I2
asserts that any single step 
 \marginpar{\popref{stuttering-i2}{This is not quite correct.}}
of the algorithm executed when $Inv$ is
true leaves $Inv$ true.  A state predicate $Inv$ that satisfies
condition~I2 is called an 
   \ctindex{2}{invariant!inductive}{inv-inductive}%
   \tindex{2}{inductive invariant}%
\emph{inductive invariant} of the algorithm.  (More precisely, it's
an inductive invariant of the next-state action $Next$.)


To prove that ${MutualExclusion}$ is an invariant of the algorithm, we find an
invariant $Inv$ satisfying 1 and 2 such that the following condition
also holds:
\begin{enumerate}
\item[I3.] $Inv => {MutualExclusion}$
\end{enumerate}
If $Inv$ is an invariant, meaning it is true of every state of every
behavior of the algorithm, then condition~I3 implies that ${MutualExclusion}$ is
also an invariant.  Thus, to prove that ${MutualExclusion}$ is an invariant, we
have to find an inductive invariant $Inv$ that is true initially and
implies ${MutualExclusion}$.  Before reading further, see if you can find such an
invariant $Inv$.

\bigskip

We don't expect to be able to deduce anything about what a step might
do in a state not satisfying a type invariant, so $Inv$ will have a
type invariant $TypeOK$ as a conjunct.  Since, we want $Inv$ to imply
${MutualExclusion}$, our first guess might be to let $Inv$ equal
 $TypeOK /\ {MutualExclusion}$.  
However, this is not an inductive invariant.  Consider a state in
which process 0 is at $e2$, process 1 is in its critical section,
and $x[1]$ equals $\FALSE$.  This state satisfies 
 $TypeOK /\ {MutualExclusion}$,
but an $e2$ step by process 0 in that state makes ${MutualExclusion}$ false.

The invariance of ${MutualExclusion}$ depends on $x[i]$ equaling $\TRUE$
when process $i$ is in its critical section.  So, our next attempt
is to let $Inv$ equal
 \[ TypeOK \ /\ \ {MutualExclusion} \ /\ \ \A i \in \{0, 1\} : InCS(i) => x[i]
 \]
However, this formula is still not an inductive invariant.  Consider a
state satisfying this formula in which neither process is in its
critical section, $x[0]$ and $x[1]$ equal $\FALSE$, and some process
$i$ is at $e2$.  That process can then take an $e2$ step making
$InCS(i)$ true and leaving $x[i]$ false, making the formula false.
An inductive invariant must also assert that $x[i]$ is $\TRUE$ if process $i$
is at $e2$.  Remember that, for a PlusCal algorithm, process $i$ is at
label $e2$ iff $pc[i]$ equals $"e2"$.  Modifying the last conjunct to
assert this, we get:
 \[ \begin{conj}
    TypeOK \V{.2} {MutualExclusion} \V{.2}
   \A\, i \in \{0, 1\} : InCS(i) \/ (pc[i] = "e2") => x[i]
    \end{conj}
 \]
Further thought reveals no states satisfying this predicate from which
a step of the protocol can make the predicate false.  This doesn't
mean that there are no such states; it just means that we can't think
of them.  The only way to be sure that there are none is by proving
that this is the required inductive invariant.  So, we define $Inv$ to
equal this formula and try to prove that it satisfies conditions I1--I3.
It turns out that it does; but if it didn't, the proof would reveal
how it needed to be changed.

\medskip 

Before we write the proof, observe how $Inv$ was constructed.  We
started with the type invariant and the invariant ${MutualExclusion}$ that we want
to prove.  We then kept strengthening the invariant when we found a
state satisfying the formula that permitted a step that makes the
formula false.  This is a standard method for finding an inductive
invariant.  With experience, you will learn to see right away most of
the conditions that an inductive invariant must assert.

\medskip 

We must now verify conditions I1--I3.  I've been writing invariance
proofs for many years, and for such a simple protocol I can check
these conditions in my head.  You may not be so good at it, so let's
go through the dull, plodding proof.  The trick is to let the math
tell us what we must do.  This is tiresome for such a simple example.
With practice, you'll be able to quickly check the trivial steps of
the proof and concentrate on the ones that need careful reasoning.
However, you should understand how to write a complete proof before
you start cutting corners.  For complex algorithms, the only way to
prevent errors is by checking all the steps, as tiresome as that may
be.

We have three conditions to verify, so we do them one at a time---in
any order.  Let's check the simplest ones first.

\begin{sloppypar}
Condition~I3 is $Inv => {MutualExclusion}$.  It is obviously true because ${MutualExclusion}$ is a
conjunct of $Inv$.
\end{sloppypar}


Condition~I1 is $Init => Inv$.  We can't really prove this, since we
don't know what formula $Init$ is.  However, in writing the protocol's
code, I made two implicit assumptions about the initial predicate:
\begin{display}
\begin{itemize}
\item[Init1.] Variables have values of the proper type.

\item[Init2.] Each process is started outside the protocol code.  
\end{itemize}
\end{display}
With these assumptions, we can (informally) prove $Init => Inv$.
Since $Inv$ is the conjunction of three formulas, we have to prove
that $Init$ implies each of them.  
\popref{mutex-proof0}{Here is the proof.}

Condition I2 is $Inv /\ Next => Inv'$, where $Inv'$ is $Inv$ with all
the variables primed.  To prove this, we need to know what the
next-state action $Next$ is.  The protocol describes two actions
of each process:
\begin{display}
\begin{describe}{$e1(i)$}
\item[$e1(i)$] Describes the execution of statement $e1$.

\item[$e2(i)$] Describes the execution of the \textbf{if} test
of statement $e2$, which transfers control either to the critical
section or to the statement following the \textbf{if}.
\end{describe}
\end{display}
The next-state action of process~$i$ is the disjunction of those two
actions plus two others:
\begin{display}
\begin{describe}{$Rest(i)$}
\item[$CS(i)$] Describes the execution of process~$i$'s critical
section.  We make the following assumptions about it:
\begin{enumerate}
\item It is enabled only when control is in the critical section.

\item It leaves control either in the critical section or outside
       the protocol.
\item It leaves $x$ unchanged.

\item It does not make $TypeOK$ false.
\end{enumerate}

\item[$Rest(i)$] Describes the steps of process~$i$ outside the
protocol.  We make the following assumptions about it:
\begin{enumerate}
\item It is enabled only when control is outside the protocol.

\item It leaves control either outside the protocol or at label $e1$.

\item It leaves $x[1-i]$ unchanged.

\item It does not make $TypeOK$ false.
\end{enumerate}
Note that we allow the $Rest(i)$ action to change the value of
$x[i]$.  For example, the algorithm could set $x[i]$ to $\FALSE$
to allow the other process to enter its critical section.
\end{describe}
\end{display}
The next-state action $Next$ then equals
  \[ \E\, i \in \{0,1\} : e1(i) \;\/\; e2(i) \;\/\; CS(i) \;\/\; Rest(i)
  \]
and Condition~I3 becomes
 \[  Inv \,/\ \, (\E\, i \in \{0,1\} : e1(i) 
            \,\/\, e2(i) \,\/\, CS(i) \,\/\, Rest(i))
      \ => \ Inv'
 \]
The structure of the formula immediately leads to
\popref{mutex-proof1}{this high-level proof structure}.  We next prove
steps 1--4 separately, in any order.  Step~2 is the most interesting,
since it's an $e2(i)$ step by which process $i$ enters its critical
section.  Since $Inv'$ is a conjunction, here is the natural
\popref{mutex-proof2}{high-level proof of step~2}.  In writing step
2.3, I used the fact that to prove a formula $\A j \in S : P(j)$, it
suffices to assume $j \in S$ and prove $P(j)$.  I substituted $j$ for
the bound symbol $i$ in the third conjunct of $Inv'$ to avoid conflict
with the symbol $i$ introduced in the statement of step~2.

Let's consider step 2.2.  It's simple enough that you can probably see
right away why it's true.  However, if you're not absolutely sure that
it is true, you can write a proof like \popref{mutex-proof3}{this
one}.  If you're unsure of the correctness of any of its lowest-level
paragraph proofs, you can expand the paragraph proof to a sequence of
lower-level steps.

The rest of the proof is similar.  For example, here's
\popref{mutex-proof23}{a proof of step 2.3}.  The proofs of the
high-level steps 3 and 4 use the assumptions made above about the
actions $CS(i)$ and $Rest(i)$.  You can complete the proof yourself.

\begin{problem} 
(a)~Write a complete proof of condition I2, the inductive invariance of $Inv$.

(b)~Where does the proof of inductive invariance fail if we remove the
$TypeOK$ conjunct from $Inv$?
\end{problem}
%
This is a boring proof.  However, observe that once we discovered the
inductive invariant $Inv$, the proof required no insight or
creativity.  It was just a matter of repeatedly using the structure of
the formula to be proved to decompose the proof into simpler steps,
until we reach the point where the steps have such simple proofs that
it's easy to see they are correct.  If you have to go down to such a
low level of detail to be confident of the correctness of a proof, you
should consider checking the proof with 
\rref{proof}{\xlink{about-tlaps}}{TLAPS}\@.  Of course, that's
impossible for this proof without precise definitions of the operators
$e1$, $e2$, $CS$, and $Rest$.

Finding an inductive invariant can require creativity.  The method of
successively strengthening an invariant until it is inductive can
guide you.  But without insight, it could take quite a few iterations
until you find one---perhaps even an infinite number of iterations.
The only way to become proficient at finding an inductive invariant is
through practice.  However, TLC can help you.

\subsubsection{Using TLC to Check an Inductive Invariant}
   \xlabel{checking-inductive-invariant}

    \ctindex{1}{inductive invariant!checking with TLC}{inductive-check-tlc}%
As you get better at writing proofs, it becomes increasingly difficult
to prove something that isn't true.  So, before trying to prove
anything, you should first try to use TLC to check if it really is
true.  We can't use TLC (or any other tool) to check a property of the
One-Bit Protocol until we have specified it precisely.  Let's specify
it as a complete PlusCal algorithm called $OneBitProtocol$.

Other than the implicit variable $pc$, the algorithm uses only the
single variable $x$, where $x[i]$ can initially have either Boolean
value, for each process~$i$.  There are two processes, named 0 and~1.
The algorithm therefore has the following structure, where
  \ctindex{1}{BOOLEAN (TLA+ statement)@{\icmd{textsc}{boolean}} (\icmd{tlaplus} statement)}{BOOLEAN}{}%
\textsc{boolean} is a built-in \tlaplus\ symbol defined to equal the
set $\{\TRUE,\,\FALSE\}$ of Booleans.
\begin{display}
\begin{tabbing}
\algorithm\ $OneBitProtocol$ \{ \V{.2}
\s{1}\= \variable\ $x \in [\,\{0, 1\} -> \BOOLEAN\!]$ ;\+\V{.2}
\process\ $(P \in \{0, 1\})$  \{ \= \ldots\  \} \-\\
\,\,\}
% $ncs$: \= noncritical section; \+\+\V{.2}
% $e1$: \> $x[self] := \TRUE$; \V{.2}
% $e2$: \> \pif\ $(x[1-self])$ \{ \goto\ $e2$ \}; \V{.2}
% $cs$: \> critical section ;  \V{.2}
% $f$:  \> $x[self] := \FALSE$; \V{.2}
%      \> \goto\ $ncs$ \- \\
\end{tabbing}
\end{display}
The protocol can be repeated any number of times by a process, so 
the body of the \process\ statement should be:
\begin{display}
\begin{tabbing}
$r:$ \= \pwhile (\TRUE) \+\V{.2}
  \s{1}\= \{ \= $e1$: \= \+ \kill
  \{ \> \> {rest of process code}\+ \V{.2}
       $e1$: \> $x[self] := \TRUE$ ; \V{.2}
       $e2$: \> \pif\ $(\,~x[1\!-\!self]\,)$ \{ $cs$: critical section \} \- \\

  \}
\end{tabbing}
\end{display}
We now have to decide how to represent the critical section and the
\emph{rest of process code}.

The simplest way to represent the critical section is with a \pskip\
statement, which does nothing except advance the process's control
state.  This represents the critical section as a single atomic step,
with $InCS(i)$ equal to $pc[i]="cs"$.  We can do this for the same
reason that we could represent the $put$ and $get$ operations as
\textbf{skip} statements in \popref{altspec}{algorithm $AltSpec$}, the
specification of alternation in
  \rref{main}{\xlink{alt-revisited}}{Section~\xref{alt-revisited}}.
The \textbf{skip} statement is an abstraction that represents all but the
last step performed in executing the critical section as stuttering steps of
the algorithm with $pc[i]="cs"$.

% There are two reasons why this
% representation is good enough.  Here's the first:
% \begin{question}
% Show that if there is an execution that violates mutual exclusion when
% an execution of the critical section performs multiple steps, then
% there is an execution that violates mutual exclusion when the critical
% section is represented as a single atomic action.
% \end{question}
% The second reason involves stuttering.  We saw in 
%   \rref{main}{\xlink{stuttering-steps}}{Section \xref{stuttering-steps}}
% that a \tlaplus\ specification allows stuttering steps---ones that do
% not change any of the specification's variables.  Therefore, the
% PlusCal algorithm allows steps that leave $x$ and $pc$ unchanged, but
% can change any other variables.  Algorithm $OneBitProtocol$ is a
% high-level specification of the One-Bit Protocol.  An algorithm
% implements the protocol iff it implements $OneBitProtocol$ under a
%   \rref{main}{\xlink{refinement-mapping}}{refinement mapping}
% that maps a state $s$ of the implementation into a state \ov{s} of
% $OneBitProtocol$ such that: 
% \begin{itemize}
% \item The value of $x$ is the same in $s$ and \ov{s}.
% 
% \item $pc[i]$ equals $"cs"$ in state \ov{s} iff, in state $s$,
% process~$i$ is in its critical section.
% \end{itemize}
% Under the refinement mapping, an execution of a process's critical
% section is mapped into a sequence of stuttering steps of
% $OneBitProtocol$ followed by an execution of the statement 
%  \mbox{$cs$: \pskip}.

The \emph{rest of process code} in process \emph{self} is allowed only
to change $x[self]$ and $pc[self]$, and it can't jump to $e2$ or $cs$.
Since we don't want to worry about what the other process might do if
it reads $x[self]$ to be a non-Boolean value, we want $x[self]\in
\BOOLEAN$ to be an invariant.  Hence, process $self$ should set $x[self]$
only to a Boolean value.  Here is a PlusCal statement that sets
$x[self]$ to an arbitrarily (nondeterministically) chosen Boolean
value:
\begin{display}
\with\ $(v \in \BOOLEAN)$ \{ $x[self]:=v$  \}
\end{display}
\rref{main}{with-stmt}{Recall that} the PlusCal statement%
\,\mbox{\with\ $(id \in S)$ \{ $\Sigma$ \}}\,
executes the code $\Sigma$ with an arbitrarily chosen value in the set
$S$ substituted for the identifier $id$.  (There can be no labels in
$\Sigma$.)

The algorithm should allow this \with\ statement to be executed any
number of times before the process reaches $e1$.  We can express this
by letting the \pwhile\ loop begin:
\begin{display}
\begin{tabbing}
$r:$ \= \pwhile (\TRUE) \+\V{.2}
  \s{1}\= \{ \=\+\+ 
\peither\ \= \{ \= \with\ $(v \in \BOOLEAN)$ \{ $x[self]:=v$  \} ; \V{.2}
          \>    \> \goto\ $r$ \V{.2}
          \> \} \V{.2}
\por      \> \pskip\ ;
\end{tabbing}
\end{display}
The PlusCal statement%
   \ctindex{1}{either (PlusCal keyword)@\icmd{peither} (PlusCal keyword)}{either-pcal}%
   \ctindex{1}{or (PlusCal keyword)@\icmd{por} (PlusCal keyword)}{or-pcal}%
\begin{display}
\peither\ \{ $\Sigma_{1}$ \} \ \por\ \ \{ $\Sigma_{2}$ \} \ \ldots\ \ \por\ 
          \{ $\Sigma_{k}$ \}
\end{display}
executes a nondeterministically chosen $\Sigma_{i}$.  (The curly
braces are optional for a $\Sigma_{i}$ consisting of a single
statement.)  

Open a new specification $OneBitProtocol$ in the Toolbox.  It will
need to extend the $Integers$ module.  Insert the
\popref{onebitprotocol-ascii}{\textsc{ascii} text of the algorithm}
and run the PlusCal translator on it.  Create a new model and run TLC
on it.  TLC should find 35 reachable states.  The \tlaplus\
definitions of the state predicates used in our informal proof are:
\begin{display}
\begin{notla}
TypeOK == /\ pc \in [{0,1} -> {"r", "e1", "e2", "cs"}]
          /\ x \in [{0,1} -> BOOLEAN]
          
InCS(i) == pc[i] = "cs"

{MutualExclusion} == ~(InCS(0) /\ InCS(1))

Inv == /\ TypeOK
       /\ {MutualExclusion}
       /\ \A i \in {0,1} : InCS(i) \/ (pc[i] = "e2") => x[i]
\end{notla}
\begin{tlatex}
 \@x{ TypeOK \.{\defeq} \.{\land} pc \.{\in} [ \{ 0 ,\, 1 \} \.{\rightarrow}
 \{\@w{r} ,\,\@w{e1} ,\,\@w{e2} ,\,\@w{cs} \} ]}%
  \ascii{onebitprotocol-inv-ascii}
 \@x{\@s{56.14} \.{\land} x \.{\in} [ \{ 0 ,\, 1 \} \.{\rightarrow} {\BOOLEAN}
 ]}%
\par\vspace{8.0pt}%
\@x{ InCS ( i ) \.{\defeq} pc [ i ] \.{=}\@w{cs}}%
\par\vspace{8.0pt}%
\@x{ {MutualExclusion} \.{\defeq} {\lnot} ( InCS ( 0 ) \.{\land} InCS ( 1 ) )}%
\par\vspace{8.0pt}%
\@x{ Inv \.{\defeq} \.{\land} TypeOK}%
\@x{\@s{34.04} \.{\land} {MutualExclusion}}%
 \@x{\@s{34.04} \.{\land} \A\, i \.{\in} \{ 0 ,\, 1 \} \.{:} InCS ( i )
 \.{\lor} ( pc [ i ] \.{=}\@w{e2} ) \.{\implies} x [ i ]}%
\end{tlatex}
\end{display}
Add these definitions to the specification.  The first thing we should
have TLC check is that ${MutualExclusion}$ is an invariant.  We should actually
have done this before even trying to write our informal proof.
Writing the protocol as a PlusCal algorithm and checking its
correctness with TLC is easier than writing even an informal proof.
Since TLC can easily check all possible executions of this simple
algorithm, there was no need to write any proof.  We wrote the proof
as an exercise in proof writing, not to check correctness of the
protocol.  For an $N$-process mutual exclusion algorithm, TLC can
check correctness only for particular values of $N$---often for values
no greater than~3.

Before checking that $Inv$ is an inductive invariant, we should check
that it is an invariant.  This checks that it is true in the initial
state (the first of the three conditions in our proof).  Of course,
TLC does this in milliseconds (plus its startup time) for all
executions of this simple algorithm.

We \target{principles:tlc-inductive-check}% 
 want TLC to check that $Inv$ is an inductive invariant of the
next-state action $Next$ (the second of the three conditions in our
proof).  Inductive invariance means that if we take a $Next$ step
starting in any state satisfying $Inv$, we get a state that also
satisfies $Inv$.  However, TLC can check only ordinary
invariance---meaning that $Inv$ is true in every state obtained by
starting in a state satisfying the initial predicate and taking steps
satisfying the next-state action.  To check inductive invariance of
$Inv$, we consider the specification $ISpec$ having initial predicate
$Inv$ and next-state action $Next$.  (We can write $ISpec$ in
\tlaplus\ as
  $Inv /\ [][Next]_{<<x,\,pc>>}$.)  The key is:
\begin{question}
Show that $Inv$ is an inductive invariant of $Next$ iff it is an
ordinary invariant of the specification $ISpec$.
\end{question}
Let's check that $Inv$ is an invariant of $ISpec$.  Create a new model
having $Inv$ as the initial predicate and $Next$ as the next-state
action and add $Inv$ to the list of invariants to be checked.
Alternatively, you can use the temporal-formula specification:
\begin{display}
$Inv \, /\ \, [][Next]_{<<x,\,pc>>}$ 
\hfill
\verb|Inv /\ [][Next]_<<x, pc>>|
\end{display}
TLC will find that $Inv$ is an invariant of this specification, and it
will report that there are 35 reachable states.  That's the same
number of states it found for the original specification, which
implies that every state satisfying the inductive invariant $Inv$ is
reachable.  This is not always the case.  More often, the inductive
invariant allows states not reachable by the algorithm.  Some
of those unreachable states might be deadlock states, so you should 
unselect deadlock checking when using TLC to check
inductive invariance.

\medskip

Now change the definition of $Inv$ by reversing the order of the
conjuncts $TypeOK$ and ${MutualExclusion}$, and run TLC on the specification
$ISpec$ to check that $Inv$ is an inductive invariant of $Next$.
TLC reports the error:
\begin{display}
\tt In evaluation, the identifier pc is either 
  \tindex{1}{undefined or not an operator}%
undefined or not an operator.
\end{display}
To understand why this happens, review the description in
 \rref{main}{\xlink{sec:computing-clock-behaviors}}{Section~\xref{sec:computing-clock-behaviors}}
of how TLC computes the possible initial states of a spec.  It
explains why the type-correctness invariant must almost always be the
first conjunct of an inductive invariant that you check with TLC\@.

The way TLC computes the initial states for such a specification
implies that it first computes all states satisfying the
type-correctness invariant.  It then throws away states that don't
satisfy the other conjuncts.  For most specifications, there are a
huge number of type-correct states.  TLC can therefore usually check
inductive invariance for only very tiny models.  If there are too many
states satisfying the type-correctness invariant, TLC will report the
error:
\begin{display}
\tt Too many 
  \tindex{1}{next states, too many}%
possible next states for the last state in the trace.
\end{display}
The largest number of type-correct states that TLC can handle is
specified by a parameter called \textsf{Cardinality of 
 \tindex{1}{largest enumerable set}%
largest
enumerable set}, which has the default value of one million.  You 
can change its value in the \textsf{TLC Options} section of the
\textsf{Advanced Options} model page.

\medskip

Finding an inductive invariant can be difficult.  You'll need all the
help that TLC can provide.  Even a very tiny model can show that an
invariant needs to be strengthened to be inductive.  You can often use
tricks to reduce the number of states TLC must examine.

As an example, suppose the type invariant simply asserts that $p$ is
in the set $Nat$ of natural numbers.  TLC obviously cannot enumerate
all the values of $p$.  A simple solution to this problem is to
redefine $Nat$ in the \textsf{Definition Override} section of the
\textsf{Advanced Options} model page so it equals $0\dd 99$.  However,
if the algorithm can increment $p$ by 1, then TLC would not find the
type invariant to be inductive because it would find $99+1$ not to be
in $Nat$.  To prevent TLC from reporting this error, you can add the
\textsf{State 
  \ctindex{1}{TLC!state constraint}{tlc-state-constraint}%
  \ctindex{1}{state constraint, in TLC}{state-constraint}%
  \ctindex{1}{constraint, state}{constraint-state}%
Constraint} $p\leq 98$ on the \textsf{Advanced Options} model page.
(TLC checks that a state satisfies the invariant before checking if it
satisfies the state constraint, so the constraint $p\leq99$ wouldn't
prevent the error.)

In this same example, suppose there is another variable $q$ for which
the type invariant asserts that $q$ is a natural number but the rest
of the invariant implies it is always in $p\dd(p+2)$.  You could modify
the type invariant by replacing $q\in Nat$ with $q\in p\dd(p+2)$, so
TLC has to examine only $100*3$ pairs of $p$, $q$ values rather
than $100*100$.

Discovering that a predicate is not an inductive invariant by trying
to prove that it is can take a lot of time.  It's worth putting quite a
bit of effort into using TLC to catch errors.  And don't forget that
your inductive invariant must be an ordinary invariant of the
specification.  Whenever you make any changes to it, check first that
it's still an invariant.

\begin{question}
(a) Use TLC to show that $TypeOK$ is also an inductive invariant of $Next$.

(b) When you do this, or when you run TLC on the specification
$ISpec$, TLC reports that the diameter of the state graph is~1.  Why?
\end{question}

\subsection{The Two-Process One-Bit Algorithm}



\subsubsection{The Two-Process Algorithm}

  \ctindex{1}{One-Bit Algorithm!Two-Process}{one-bit-2-proc-alg}%
We now turn the one-bit protocol into a complete mutual exclusion
algorithm, starting with a two-process one.  We have seen that the
protocol ensures mutual exclusion, but we have not discussed deadlock
freedom.  Our $OneBitProtocol$ PlusCal algorithm is obviously not
deadlock free because it permits an execution in which $x[0]$ and
$x[1]$ both always equal \TRUE, so no process ever enters its critical
section.  

In a mutual exclusion algorithm, we want $x[i]$ to equal \FALSE\
except when process $i$ is in its critical section or trying to enter
it.  The obvious way to do this is to let each $x[i]$ initially equal
\FALSE\ and let the body of process $self$ be:
\begin{display}
\begin{tabbing}
$ncs$: \=\+ \pwhile\ $(\TRUE$) \V{.2}
        \s{1}\=\+ \{ \= $e1$:  \= \kill
         \{ \> \> \pskip\ ; \V{.2}
            \> $e1$:  \> $x[self] := \TRUE$ ; \V{.2}
            \> $e2$:  \> \pif\ $(~x[1-self])$ \{ $cs$: \pskip\ \}  \V{.2}
            \>        \> \pelse\ \{ \goto\ $e2$ \} ;   \V{.2}
            \> $f$:   \> $x[self] := \FALSE$   \V{.2}
             \}
\end{tabbing}
\end{display}
The $ncs$ action (execution from label $ncs$ to label $e1$) represents
the noncritical section.  For the same reason we can
represent the noncritical section as an atomic \pskip\ statement, we
can also represent the noncritical section as one.

Complete this code to a two-process algorithm named $OneBit$, and put it in
a new specification $OneBit2Procs$.  The result should look like
  \popref{onebit2proc-ascii-1}{this}.
Run the translator on the algorithm.  As we did for the protocol
specification, define:
\begin{display}
\begin{notla}
InCS(i) == pc[i] = "cs"
{MutualExclusion} == ~(InCS(0) /\ InCS(1))
\end{notla}
\begin{tlatex}
\@x{ InCS ( i ) \.{\defeq} pc [ i ] \.{=}\@w{cs}}\vs{.2}%
\@x{ {MutualExclusion} \.{\defeq} {\lnot} ( InCS ( 0 ) \.{\land} InCS ( 1 ) )}%
\end{tlatex}
\end{display}
and let TLC check that ${MutualExclusion}$ is an invariant of the algorithm.  You
can also check that the predicate $Inv$ we defined for the protocol,
except with a suitably modified definition of $TypeOK$, is an
inductive invariant of the algorithm.

\begin{problem}
Have TLC check that this algorithm $OneBit$ implements the algorithm
$OneBitProtocol$ defined above under the following refinement mapping:
\begin{display}
\begin{notla}
x  <-  x
pc <-  [i \in {0, 1} |-> IF pc[i] \in {"ncs", "f"} THEN "r"
                                                   ELSE pc[i]]
\end{notla}
\begin{tlatex}
\@x{ x\@s{3.92} \.{\leftarrow}\@s{4.1} x}\vs{.2}%
 \@x{ pc \.{\leftarrow}\@s{4.10} [ i \.{\in} \{ 0 ,\, 1 \} \.{\mapsto} {\IF}
 pc [ i ] \.{\in} \{\@w{ncs} ,\,\@w{f} \} \.{\THEN}\@w{r}}%
\@x{\@s{188.97} \.{\ELSE} pc [ i ]\, ]}%
\end{tlatex}
\end{display}
(See \rref{main}{\xlink{sec:refinement}}{
Section~\xref{sec:refinement}}.)
\end{problem}
%
Of course, we expected the algorithm to satisfy mutual exclusion since
the protocol does.  However, we want an algorithm that also is
deadlock free.  Deadlock freedom was Dijkstra's 
  \lref{dijkstra-d}{requirement (d)}.
Today, that requirement would be stated as:
\begin{display}
If any process tries to enter its critical section, then some
process eventually reaches its critical section.
\end{display}
To state this more precisely, we first define a state predicate
$Trying(i)$ that is true iff process $i$ is trying to enter its
critical section.  The definition is
 \[ Trying(i) == pc[i] \in \{"e1", "e2"\} 
 \]
Add the definitions of $Trying$ and $DeadlockFree$ to the
specification.

Deadlock\target{two-proc-deadlockfree} freedom means that if 
  $Trying(0) \/ Trying(1)$ 
ever becomes true, then eventually (at that point or some later point in 
the execution) 
  $InCS(0) \/ InCS(1)$
will be true.  This assertion is written as the temporal formula 
   \[ DeadlockFree == (Trying(0) \/ Trying(1))\; ~> \; (InCS(0) \/ InCS(1)) \]
In general, the 
     \ctindex{1}{+2rq@\mmath{\icmd{leadsto}} (leads to)}{+2rq}%
temporal operator $~>$ (read \emph{leads to} and written in
\textsc{ascii} as \texttt{\raisebox{-.2em}{\tilde}>})
is defined so that for any state
predicates $P$ and $Q$, the formula $P~>Q$ is true of a behavior
$s_{1} -> s_{2} -> \ldots$ iff, for any $i$ such that $P$ is true in
state $s_{i}$, there is a $j\geq i$ such that $Q$ is true in state
$s_{j}$.



The translation defines the specification $Spec$ of the algorithm to
be $Init /\ [][Next]_{vars}$.  This specification can't satisfy
deadlock freedom because it specifies only safety; it doesn't
require the algorithm to take any (non-stuttering) steps.  Thus, it
allows a behavior in which process~0 remains forever in its noncritical
section and process~1 reaches control point~$e2$ and stops.  We must
add some fairness assumption.

The traditional fairness assumption for multiprocess algorithms, and
the one implicitly assumed by Dijkstra, is
\rref{main}{main:weak-fairness}{weak fairness} of each process---that
is, of each process's next-state action.  As we saw in our
specification of alternation, this assumption is specified in PlusCal
by preceding the keyword \process\ with the keyword \fair.  Make this
change to the algorithm and run the translator.  The translator then
adds the conjunct
 \[ \A\, self \in \{0,1\} : \WF_{vars}(P(self))
 \]
to specification $Spec$, where $P(i)$ is the next-state action of
process~$i$.  

Have TLC check the property $DeadlockFree$ (by adding it to the
\textsf{Properties} list in the \textsf{What to check?} section of the
model's \textsf{Model Overview} page).  TLC reports that the property
is not satisfied; it gives an error trace that reaches the state with
$x[0]$ and $x[1]$ both equal to \TRUE\ and $pc[0]$ and $pc[1]$ both
equal to $"e2"$, and then stutters forever.  From this state, all the
algorithm can do is have either process~$i$ execute its $e2$ action, 
finding $x[1-i]$ equal to $\TRUE$ and remaining in the same state.
%
\begin{aquestion}{mutex-answer4a}
Explain why $\WF_{vars}(Proc(i))$ is true for a behavior in which
eventually $x[1-i] /\ (pc[i]="e2")$ is always true.
\end{aquestion}
%
To make the algorithm deadlock free, we must prevent both processes
from waiting forever at $e2$.  The One-Bit algorithm does this by
having one process $i$ set $x[i]$ to \FALSE\ and allowing the other
process to enter its critical section.  Let process~1 be the one to do
that.  We leave process~0 the same and replace the \pelse\ clause of
process~1 with
\begin{display}
\begin{tabbing}
$e3$: \= $x[1] := \FALSE$ ; \V{.2}
$e4$: \= \pwhile\ $(x[0])$ \{ \pskip \} ; \V{.2}
      \> \goto\ $e1$ 
% $e4$: \> \pif\ $(x[0])$ \{ \goto\ $e4$ \}\V{.2}
%     \> \pelse\ \{ \goto\ $e1$ \}
\end{tabbing}
\end{display}
The two processes now don't execute the same code.  We could declare
them with two separate \process\ statements, but it's more convenient
to use a single \process\ statement, replacing statement 
% \ascii{onebit2proc-ascii-2}%
$e2$ with:
\begin{display}
\begin{tabbing}
$e2$: \= \pif\ $(~x[1-self])$ \{ $cs$: \pskip\ \}%
  \`\makebox[0pt][l]{\popref{onebit2proc-ascii-2}{\textsc{ascii} version}}%
\V{.2}
      \> \pelse\ \= \{ \= \pif\ $(self = 0)$ \{ \goto\ $e2$ \} \V{.2}
      \>         \>    \> \pelse\ \= \{ \= \+\+\+\+\+
                            $e3$: \= $x[1] := \FALSE$ ; \V{.2}
                            $e4$: \= \pwhile\ $(x[0])$ \{ \pskip \} ; \V{.2}
                             \> \goto\ $e1$ 
%                            $e4$: \> \pif\ $(x[0])$ \{ \goto\ $e4$ \}\V{.2}
%                                   \> \pelse\ \{ \goto\ $e1$ \} 
                             \-\V{.2}
                               \} \-\- \V{.2}
                         \}
\end{tabbing}
\end{display}
Change the algorithm in module $OneBit2Procs$.  The definition of
$Trying$ also needs to be changed to reflect the change to the code.
A suitable definition is
 \[ Trying(i) == pc[i] \in \{"e1", "e2", "e3", "e4"\} \]
Since $pc[0]$ does not equal $"e3"$ or $"e4"$ in any reachable
state, we could also define $Trying$ by
 \[ Trying(i) == pc[i] \in \If{i=0}\Then \{"e1", "e2"\}
                     \Else \{"e1", "e2", "e3", "e4"\} \Fi
 \]
but the simpler definition will do just as well.  Run the translator
and run TLC on the same model as before.  TLC should verify that this
algorithm does satisfy property $DeadlockFree$.

\begin{aproblem}{mutex-answer6} \label{mutex-answer6}
 \target{mutex-answer6}%
 Find an inductive invariant of the algorithm that can be used to
prove the invariance of ${MutualExclusion}$.  Write the invariance proof.
\end{aproblem}

\subsubsection{Busy Waiting Versus Synchronization Primitives}

  \tindex{1}{synchronization primitive}%
  \tindex{1}{busy waiting}%
  \tindex{1}{waiting, busy}%
Consider the code
\begin{display}
\begin{tabbing}
$e4$: \= \pwhile\ $(x[0])$ \{ \pskip \} ; \V{.2}
      \> \goto\ $e1$ 
% $e4$: \= \pif\ $(x[0])$ \{ \goto\ $e4$ \}\V{.2}
%       \> \pelse\ \{ \goto\ $e1$ \} 
\end{tabbing}
\end{display}
executed by process~1.  This is the way Dijkstra might have written
that code, indicating that the process keeps reading $x[0]$ until
finding it equal to \FALSE, whereupon it goes to location $e1$.
Since Dijkstra posited reading and writing shared memory registers as
the only synchronization primitives, a process could wait for $x[0]$
to become false only by repeatedly reading it.

A more natural way to write this code in PlusCal is with an 
\await\
statement:
\begin{display}
\begin{tabbing}
$e4$: \= \await\ $~x[0]$ ; \V{.2}
      \> \goto\ $e1$ 
\end{tabbing}
\end{display}
In 1965, the two versions of $e4$ would have been considered to
produce two different algorithms.  The \await\ construct would have
been viewed as a special synchronization primitive, very different
from the \pwhile\ loop of the first version.  Most computer scientists
today would probably also consider them to be different.  However, the
two PlusCal algorithms are completely equivalent.

To see that the two versions of the code produce equivalent specs, we
need only examine their \tlaplus\ translations.  The translation of
both versions of the algorithm is the formula $Spec$, defined to equal
 \[Init \ /\ \ [][Next]_{vars} 
        \  /\ \ (
          \A \, self \in \{0,1\} : \WF_{vars}(P(self)))\]
where
\begin{display}
$Init$ is the initial predicate.\V{.6}
%
$Next$ is the algorithm's next-state action, which equals\V{.1}
 \s{2}$\E\,self \in \in \{0,1\} : P(self)$.\V{.6}
%
$P(self)$ is the next-state action of process $self$,
which equals\V{.1}
 \s{2}$ncs(self) \/ e1(self) \/ e2(self) \/ cs(self) \/ e3(self)
              \/ e4(self) \/ f(self)$.\V{.6}
%
$vars$ is the pair $<<x,\,pc>>$
\end{display}
The specifications of the two versions are the same
except for the definition
of $e4$.  In the version with the \pwhile\ loop, $e4$ is defined by:
\begin{display}
\begin{notla}
e4(self) == /\ pc[self] = "e4"
            /\ IF x[0]
                  THEN /\ TRUE
                       /\ pc' = [pc EXCEPT ![self] = "e4"]
                  ELSE /\ pc' = [pc EXCEPT ![self] = "e1"]
            /\ x' = x
\end{notla}
\begin{tlatex}
\@x{ e4 ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{e4}\vs{.2}}%
\@x{\@s{53.44} \.{\land} {\IF} x [ 0 ]\vs{.2}}%
\@x{\@s{76.71} \.{\THEN} \.{\land} {\TRUE}\vs{.2}}%
 \@x{\@s{108.02} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ]
 \.{=}\@w{e4} ]\vs{.2}}%
 \@x{\@s{76.71} \.{\ELSE} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [
 self ] \.{=}\@w{e1} ]\vs{.2}}%
\@x{\@s{53.44} \.{\land} x \.{'} \.{=} x}%
\end{tlatex}
\end{display}
In the version with \await, $e4$ is defined by:
\begin{display}
\begin{notla}
e4(self) == /\ pc[self] = "e4"
            /\ (~x[0])
            /\ pc' = [pc EXCEPT ![self] = "e1"]
            /\ x' = x
\end{notla}
\begin{tlatex}
\@x{ e4 ( self ) \.{\defeq} \.{\land} pc [ self ] \.{=}\@w{e4}\vs{.2}}%
\@x{\@s{53.44} \.{\land} ( {\lnot} x [ 0 ] )\vs{.2}}%
 \@x{\@s{53.44} \.{\land} pc \.{'} \.{=} [ pc {\EXCEPT} {\bang} [ self ]
 \.{=}\@w{e1} ]\vs{.2}}%
\@x{\@s{53.44} \.{\land} x \.{'} \.{=} x}%
\end{tlatex}
\end{display}
When $pc[self]$ equals $"e4"$ and $x[0]$ equals $\TRUE$, the first
definition allows an $e4(self)$ step that leaves $pc$ and $x$
unchanged---that is, a stuttering step.  (Setting the new value of
$pc[self]$ to equal its old value is the same as not changing it.)
With those values of $pc[self]$ and $x[0]$, the second definition does
not allow an $e4(self)$ step.  Hence the definitions of $Next$ and
$P(self)$ differ only in whether or not they allow certain stuttering
steps (ones that leave $x$ and $pc$ unchanged).  Since action
$[Next]_{vars}$ allows stuttering steps, the two definitions of
$e2(self)$ yield equivalent definitions of $[Next]_{vars}$.  They also
yield equivalent definitions of $<<P(self)>>_{vars}$, which allows
only the non-stuttering steps allowed by $P(self)$.  Hence, the
definition of $\WF$ implies that they yield equivalent definitions of
$\WF_{vars}(P(self))$.  The two definitions therefore yield equivalent
definitions of the specification $Spec$.

\begin{problem}
Use TLC as follows to show that the two specifications $Spec$ are
equivalent.  Put the two versions of the algorithm in two different
specifications, with root modules that I will call here $M1$ and $M2$.
Add the following statement to $M1$
\begin{display}
$Other == \INSTANCE M2 \WITH x <- x, pc <- pc$
\end{display}
and use TLC to check that the algorithm of $M1$ satisfies the property
$Other!Spec$.  Explain why this shows that formula $Spec$ of $M1$
implies formula $Spec$ of $M2$.  Then use the analogous procedure
to show that formula $Spec$ of $M2$ implies formula $Spec$ of $M1$,
showing that the two formulas are equivalent.
\end{problem}
%
The equivalence of the two algorithms doesn't mean that busy waiting
is the same as using an operating-system primitive to wait for a
condition to be true.  What it does mean is that the PlusCal code
describes the algorithm at a high enough level of abstraction that the
distinction between these two ways of waiting disappears.  In the
algorithm's abstraction, waiting means not changing $pc$ or $x$.  This
describes implementations in which a waiting process repeatedly reads
the value of $x[0]$, as well as implementations in which a waiting
process ``sleeps'' until it is notified that $x[0]$ has been changed.

PlusCal is not a programming language.  It is a convenient way to
write certain kinds of system specifications---including ones that are
usually called ``algorithms''.  Like any system specification, an
algorithm is not a system; it is a mathematical formula that serves as
a blueprint of a system.  What matters is the mathematical formula,
not the syntax of the PlusCal code that generated it.


\subsubsection{Requirement (c)} \xlabel{requirement-c}

TLC has checked that the two-process One-Bit algorithm satisfies
deadlock freedom, which is the precise statement of Dijkstra's
  \lref{dijkstra-d}{requirement~(d)}.
We have decided to ignore his requirement~(a), which was symmetry of
the processes' code.  His requirement~(b), that there is no assumption
about the relative speeds, is built into our method of specifying
algorithms.  (Any such assumption would have to be explicitly
asserted.)  What about his requirement~(c)? 

As we observed above, requirement~(c) implicitly requires that either
process be able to stop in its noncritical section.  In our algorithm,
a process $i$ is in its noncritical section iff it is at control point
$ncs$---that is, iff $pc[i]="ncs"$.  Our liveness requirement of weak
fairness on the next-state action $P(i)$ of each process~$i$ means
that the process cannot stop taking non-stuttering steps if such a
step remains enabled.  When $pc[i]="ncs"$, the process can execute the
\pskip\ statement, which is a non-stuttering step (it sets $pc[i]$ to
$"e1"$).  Hence weak fairness of $P(i)$ implies that process~$i$
cannot stop in its noncritical section, violating requirement~(c).

As we saw for the \rref{main}{label-decoration}{finer-grained
$Handshake$ algorithm}, PlusCal allows us to modify the fairness
requirement so that it does not apply to a process when control is at
$ncs$ by putting
  \ctindex{2}{+2pl@\mmath{-} after PlusCal label}{+2pl}%
\,\verb|-|\,
after the label, like this:
\begin{display}
$ncs$\,:\,- \pwhile\ $(\TRUE)$ \ldots 
\end{display}
This causes the translation to produce the fairness assumption:
 \[\A\, self \in \{0,1\} : \WF_{vars}((pc[self] # "ncs") /\ P(self))\]
Weak fairness of the action $(pc[i] # "ncs") /\ P(i)$ requires
process $i$ eventually to take a $P(i)$ step only when $pc[i]$ does
not equal $"ncs"$, so it allows the process to stop in its noncritical
section.  Have TLC check that the algorithm still satisfies deadlock
freedom with this weaker fairness assumption.

It's not clear whether a process should be allowed to remain forever
in its critical section.  Dijkstra's article says nothing about this
possibility, and I don't know if he considered it.  Most computer
scientists seem to assume that a process must eventually leave its
critical section.  Indeed, my statement of starvation freedom---that
any process trying to enter its critical section eventually
succeeds---makes it impossible to satisfy if a process can remain
forever in its critical section.  However, it can be argued that the
only assumption a mutual exclusion algorithm should make about the
noncritical and critical sections is that they do not modify the
values of any variables used by the algorithm---except for the obvious
changes to the value of $pc$.

For deadlock freedom, it makes little difference whether or not we
allow a process to remain forever in its critical section.  However,
assuming that it can't allows a simpler definition of
starvation freedom.  I will therefore make the customary assumption
that a process in its critical section eventually exits from it.
\begin{question}
What is the weak fairness property that allows processes to stop
inside their critical and noncritical sections?  Compare your answer
to the fairness condition produced by the translator when you modify
the PlusCal code to allow this possibility.  Use TLC to check
that deadlock freedom is satisfied even with this weaker fairness
assumption.
\end{question}
\begin{aquestion}{mutex-answer3} \targetlabel{mutex-question3}
% (a)~
%
Assuming the appropriate definitions of $Trying$ and $InCS$, write
the fairness formula expressing the customary statement of starvation
freedom for an algorithm with an arbitrary set $Proc$ of processes.

% (b) What is the appropriate definition if processes can stop inside
% their critical sections?
\end{aquestion}

% \begin{hquestion}{mutex-answer5}
% In \rref{main}{\xlink{main:proc-wf}}{Question~\xref{main:proc-wf}},
% you showed that, in the absence of labels followed by ``:\,-'', weak
% fairness of a process is equivalent to weak fairness of every action
% of the process.  Show that, in general, weak fairness of a process is
% equivalent to weak fairness of each of its actions that correspond to
% a label not followed by ``\,:\,-\,''.  
% \end{hquestion}
%


% \subsubsection{Proof of Safety}
% 
% There is no need to prove correctness of the Two-Process algorithm,
% since TLC can check it for all possible executions.  However, this is
% an exceptional situation.  TLC can find errors, and for some
% algorithms it will be able to check large enough models to convince us
% that the algorithm is probably true.  Rarely can TLC guarantee
% correctness.  For that, we almost always need a proof.  
% 
% The proof of liveness is deferred to the next section.
% Here, we prove safety---namely, that the algorithm satisfies mutual
% exclusion.
% 
% 
% We know that it should, since it obeys the one-bit
% protocol.  However, our reasoning that it does obey that protocol is
% rather informal.  We know how to write a rigorous proof: find an
% inductive invariant that is implied by the initial predicate and
% implies mutual exclusion.  Our invariance proof for the protocol in
% \lref{\xlink{two-bit-protocol-proof}}{Section~\xref{two-bit-protocol-proof}}
% suggests that the appropriate invariant is
% \begin{display}
%   $\begin{conj} 
%    TypeOK \V{.2}
%    {MutualExclusion} \V{.2}
%    \A i \in \{0,1\} : InCS(i) \/ (pc[i] = "e2") => x[i]
%    \end{conj}$
% \end{display}
% Although this is an invariant of the algorithm, it is not an inductive
% invariant.
% \begin{aquestion}{mutex-answer7}  \targetlabel{mutex-question7}
% Determine why this formula is not an inductive invariant by trying to
% prove that it is.  (You can use TLC to check inductive invariance and
% find the problem for you, but you will learn more by finding it
% yourself.)  Add a conjunct to the formula to make it an inductive
% invariant.
% \end{aquestion}
%

\subsection{Proving Liveness}

\subsection{An Informal Proof}

In \lref{mutex-answer6}{Problem \ref{mutex-answer6}}, you proved the
safety property of the Two-Process One-Bit Algorithm---namely, that it
satisfies mutual exclusion.  Let's now prove liveness.  The liveness
property satisfied by this algorithm is deadlock freedom.  Letting
$Trying(i)$ mean that process~$i$ is trying to enter its critical
section and $InCS(i)$ to mean that it is in its critical section, 
we expressed this condition \lref{two-proc-deadlockfree}{above}
by the formula
    \[ DeadlockFree == (Trying(0) \/ Trying(1))\; ~> \; (InCS(0) \/ InCS(1)) \]
For our algorithm, we have
   \[ \begin{noj}
      Trying(i) == pc[i] \in \{"e1", "e2", "e3", "e4"\} \V{.2}
      InCS(i) == pc[i] = "cs"
      \end{noj}
   \]
(It's an invariant of the algorithm that $pc[0]$ never equals $"e3"$ or
$"e4"$.)  
We now give an informal proof of this property.  We must prove that it
is true for some arbitrary behavior $s_{1} -> s_{2} -> s_{3} ->
\cdots$ satisfying the algorithm's specification.  For linguistic
convenience, we say that something is true at time $t$ if it is true
in state $s_{t}$ or in the suffix $s_{t} -> s_{t+1} -> \cdots$ of this
behavior.

For brevity, let's define
   \[ \begin{noj}
      T0 == Trying(0) \s{2} T1 == Trying(1) \s{2}
      Success == InCS(0) \/ InCS(1)
      \end{noj}
  \]
We have to show that if $T0 \/ T1$ is true at some time $t_{1}$, then
$Success$ is true at some time $t\geq t_{1}$.  In general, proving
a formula $F$ by contradiction is 
  \marginpar{We can prove $F$ by assuming $~F$ and
   proving $F$, since $~F \land F$ implies $\FALSE$.} 
easier than proving it directly because we have the additional
hypothesis $~F$.  To prove by contradiction that a formula $F$ is
eventually true, we get to assume not just that $~F$ is true, but that
it is always true.  This makes proof by contradiction especially
useful.  We are therefore led to the following high-level proof.
\begin{display}
\pflongnumbers%{0}
%\pflongindent
\beforePfSpace{10pt, 2pt, 2pt}
\afterPfSpace{10pt, 5pt, 5pt}
\interStepSpace{4pt}
\begin{proof}
\step{1}{It suffices to assume that $T0 \/ T1$
is true at some time $t_{1}$ and $~Success$ is true at all times $t\geq
t_{1}$, and to obtain a contradiction.}

\step{2}{$T0$ is false at time $t_{1}$.}

\step{3}{$T1$ is false at time $t_{1}$.}

\qedstep
\begin{proof}
\pf\ By \stepref{2}, \stepref{3}, and the step \stepref{1} assumption.
\end{proof}
\end{proof}
\end{display}
When writing the proof of step~3, we discover that we need to
know that $T0$ is false at some time $t_{2}\geq t_{1}$.  We can avoid
a separate proof of this fact by strengthening step~2 to:
\begin{display}
\pflongnumbers
\begin{proof}
\nostep{1}
\step{2}{$T0$ is false at all times $t\geq t_{1}$.}
\end{proof}
\end{display}
\popref{2-proc-mutex}{Here is the algorithm} and
\popref{tla-pf-1}{here is the proof}, carried down to a reasonable
level of detail.  I have omitted the proof of step~2.

\medskip

\noindent\textsf{If you are not interested in writing more rigorous proofs,
\lref{\xlink{sec:alternation}}{skip to Section~\xref{sec:alternation}}.
Otherwise, \rref{math}{temporallogic}{detour to a discussion
of temporal logic} before continuing to the next section.}

\target{tlaproof}
\subsection{A More Formal Proof}
\xlabel{more-formal-proof}

We now give a more formal version our informal proof of deadlock
freedom---a proof in which each assertion is a \tlaplus\ formula.  For
convenience in writing the proof, let's define $Fairness$ to be the
formula expressing the fairness property of the algorithm, so $Spec$
equals
  $Init /\ [][Next]_{vars} /\ Fairness$.  
The \tlaplus\ translation of the algorithm tells us
that its definition is:
\begin{widedisplay}
\begin{notla}
Fairness == \A self \in {0,1} : WF_vars((pc[self] \notin {"ncs", "cs"}) /\ P(self))
\end{notla}
\begin{tlatex}
 \@x{ Fairness \.{\defeq} \A\, self \.{\in} \{ 0 ,\, 1 \} \.{:} {\WF}_{ vars}
 ( ( pc [ self ] \.{\notin} \{\@w{ncs} ,\,\@w{cs} \} ) \.{\land} P ( self )
 )}%
\end{tlatex}
\end{widedisplay}
However, we won't carry our proof down to the level of detail for
which the formal definition of $Fairness$ matters.  The only formal
property of $Fairness$ that we need to know is that it's a
\rref{math}{box-formula}{$\Box$ formula}.  This follows from the fact
that the definition of $\WF$ implies that any $\WF$ formula is a
$\Box$ formula.  However, you should be able to verify intuitively
from the meaning of this fairness condition that $Fairness$ is true of
a behavior $\sigma$ iff it is true of all suffixes of $\tau$, which
implies that it is a $[]$ formula.

To prove that the algorithm is deadlock free, we must prove the
theorem $Spec => DeadlockFree$.  The usual way to prove such an
implication is to assume $Spec$ and prove $DeadlockFree$.  However,
this is a temporal theorem, and assumptions in temporal proofs should
be {$\Box$ formulas}.  Formula $Spec$ is not a
$[]$ formula because of its conjunct $Init$, which is a state predicate.

We should not expect assuming $Spec$ to be useful.  To prove that an
arbitrary behavior $\sigma$ satisfying $Spec$ satisfies a liveness
property, we reason about states that occur at arbitrary points in the
behavior.  In other words, we reason about suffixes of $\sigma$.  The
formula $Spec$ is true of $\sigma$ but not necessarily of a suffix of
$\sigma$, because the initial predicate $Init$ is not true for an
arbitrary state in $\sigma$.  Therefore, the fact that $Spec$ is true
of $\sigma$ cannot be used directly to reason about suffixes of
$\sigma$.

To prove a liveness property, instead of using $Init$, we need to use
a state predicate that is always true---in other words, we must use an
invariant.  Let's call the invariant $LInv$.  Our proof begins as
follows, where we first prove that $LInv$ is an invariant and then use
$[]LInv$ as an assumption.
\begin{display}
\pflongnumbers
\interStepSpace{.5em}
\begin{proof}
\step{0}{$Spec => []LInv$}

\step{1}{\sassume{$[]LInv \, /\ \, [][Next]_{vars} \, /\ \, Fairness$}
\prove{$DeadlockFree$}}
\end{proof}
\end{display}
The invariant $Inv$ that we used to prove mutual exclusion is not
strong enough for proving deadlock freedom.  For example, step 3.3 of
\popref{tla-pf-1}{our informal proof} uses the fact that $x[0]$ equals
$\FALSE$ when process~0 is at $ncs$.  However, that fact was not
needed to prove mutual exclusion and is not implied by $Inv$.  Here is
an invariant that is strong enough.  It strengthens $Inv$ by
specifying the value of $x[i]$ as a function of
$pc[i]$, for each process~$i$.
\begin{display}
\begin{notla}
LInv == /\ TypeOK
        /\ {MutualExclusion}
        /\ pc[0] \notin {"e3", "e4"}
        /\ \A i \in {0,1} : x[i] <=> (pc[i] \in {"e2", "e3", "cs", "f"})
\end{notla}
\begin{tlatex}
\@x{ LInv \.{\defeq} \.{\land} TypeOK}%
\@x{\@s{40.31} \.{\land} {MutualExclusion}}%
\@x{\@s{40.31} \.{\land} pc [ 0 ] \.{\notin} \{\@w{e3} ,\,\@w{e4} \}}%
 \@x{\@s{40.31} \.{\land} \A\, i \.{\in} \{ 0 ,\, 1 \} \.{:} x [ i ]
 \.{\equiv} ( pc [ i ] \.{\in} \{\@w{e2} ,\,\@w{e3} ,\,\@w{cs} ,\,\@w{f} \}
 )}%
\end{tlatex}
\end{display}
Since $DeadlockFree$ equals $T0 \/ T1 ~> Success$, we use a standard
temporal proof by contradiction with the next proof step:
\begin{display}
\pflongnumbers
\begin{proof}
\nostep{0} \nostep{1}
\step{1a}{\sassume{$[]~Success$}\prove{$(T0 \/ T1) ~> \FALSE $}}
\end{proof}
\end{display}
When you get used to writing these proofs, you will save space by combining
steps 2 and 3 into:
\begin{display}
\pflongnumbers
\begin{proof}
\nostep{0} 
\step{1a}{\sassume{$[]LInv \, /\ \, [][Next]_{vars} \, /\ \, Fairness
     \, /\ \, []~Success$}\prove{$(T0 \/ T1) ~> \FALSE $}}
\end{proof}
\end{display}
\popref{2-proc-mutex-liveness}{Here is the full proof.}
 % To allow me to refer proof steps, each step's long number appears
 % {\commentcolor in this color} in the margin.  
If you'd like to read the proof in the Toolbox, using its commands for
hiding subproofs, \popref{2-proc-mutex-liveness-ascii}{click here for
an \textsc{ascii} version}.  (It does not contain the graphs that
explain the uses of Leads-To Induction.)


\subsection{The \emph{N}-Process One-Bit Algorithm} 
  \xlabel{sec:n-proc-alg}

  \ctindex{1}{One-Bit Algorithm!\mmath{N}-Process}{one-bit-N-proc-alg}%
It's easy to generalize the basic 2-process one-bit protocol to $N$
processes.  Each process $i$ sets its bit $x[i]$ to \TRUE\ and can
enter its critical section if it then sees $x[j]$ equal to $\FALSE$
for every other process $j$.  We first write this protocol in 
pseudo-PlusCal.

Let $Procs$ be the set of processes, which following Dijkstra we take
to be the set $1\dd N$ of integers from 1 through $N$.  As in PlusCal,
we let $self$ be the name of the current process.  We let process
$self$ read the other bits $x[j]$ in an arbitrary,
nondeterministically chosen order.  We let $unchecked$ be a variable
local to process $self$ that holds the set of all processes $j$ for
which $self$ has not yet read $x[j]$.  Process $self$ sets $unchecked$
to the set of all processes in $Procs$ other than $self$ itself---that
is, the set $Procs :\: \{self\}$.  It
then repeatedly sets a local variable $other$ to any process in the
set $unchecked$, removes $other$ from $unchecked$, and then continues
only if $x[other]$ is $\FALSE$.  The pseudo-code for the protocol is:
\begin{display}
\begin{minipage}{.8\textwidth}
\begin{tabbing}
$e1$: \= $x[self] := \TRUE$ ; \V{.2}
      \> $unchecked := Procs :\: \{self\}$ ; \V{.2}
$e2$: \pwhile $(unchecked # \{\})$ \V{.2}
    \> \s{1} \= \{  \= Set $other$ to any element of $unchecked$ ; \V{.2}
    \>       \>      \> $unchecked := unchecked :\: \{other\}$ ;\V{.2}
    \>       \>       \> \await\ $~x[other]$ \V{.2}
    \>       \> \} \V{.2}
$cs$: \> critical section
\end{tabbing}
\end{minipage}
\end{display}
As we have seen in the case $N=2$, this algorithm can deadlock---each
process waiting for the other's variable to become false.  The
two-process algorithm breaks this deadlock by having process~1 set its
variable false, allowing process~0 to enter the critical section.  The
generalization to $N$ processes is to have each process wait for any
lower-numbered process that it observes also to be waiting to enter
the critical section.  Here is \popref{onebitmutex}{the algorithm in
PlusCal}, where $Procs$ is defined to be the set $1\dd N$ of
processes.  As in the two-process version, we assume fairness of each
process, but not of its non-critical section action.

Create a new specification with \popref{onebitmutex-ascii}{the
\textsc{ascii} version} of the algorithm and run the translator.
(You will have to declare $N$ to be a constant and define $Procs$.)
Use TLC to check that the algorithm satisfies mutual exclusion 
by checking that
 \[ {MutualExclusion} == \A \, i, j \in Procs : (i # j) => ~(InCS(i) /\ InCS(j))
 \]
is an invariant, and check that the algorithm is deadlock 
  \target{deadlock-free}%
free by checking that it satisfies the property
 \[ DeadlockFree == (\E\, i \in Procs : Trying(i)) ~> 
            (\E i \in Procs : InCS(i))
\] 
where $Trying$ and $InCS$ are defined by:
 \[ \begin{noj}
    Trying(i) == pc[i] \in \{"e1", "e2", "e3", "e4", "e5", "e6"\} \V{.4}
    InCS(i) == pc[i] = "cs"
    \end{noj}
\]
TLC will check these properties in a few seconds for $N=3$ and in around
20 minutes for $N=4$.  

To prove mutual exclusion, we first define the state predicate
$Past(i, j)$ to assert that process $i$ is trying to enter its critical
section and has ``passed'' process~$j$, meaning that it has
seen $x[j]$ equal to $\FALSE$ when executing the 
\pif~{$(x[other])$} test of statement~$e3$.  The precise definition is:%
  \marginpar{In the \tlaplus\ translation, the process-local variables
             $unchecked$ and $other$ becomes arrays indexed by
             $Proc$.}
\begin{display}
\begin{notla}
Past(i, j) == \/ (pc[i] = "e2") /\ (j \notin unchecked[i])
              \/ /\ pc[i] \in {"e3",  "e6"} 
                 /\ j \notin unchecked[i] \cup {other[i]}
              \/ pc[i] = "cs"
\end{notla}
\begin{tlatex}
 \@x{ Past ( i ,\, j ) \.{\defeq} \.{\lor} ( pc [ i ] \.{=}\@w{e2} ) \.{\land}
 ( j \.{\notin} unchecked [ i ] )\vs{.2}}%
 \@x{\@s{61.63} \.{\lor} \.{\land} pc [ i ] \.{\in} \{\@w{e3}
 ,\,\@s{4.1}\@w{e6} \}}%
 \@x{\@s{72.74} \.{\land} j \.{\notin} unchecked [ i ] \.{\cup} \{ other [ i ]
 \}\vs{.2}}%
\@x{\@s{61.63} \.{\lor} pc [ i ] \.{=}\@w{cs}}%
\end{tlatex}
\end{display}
The basic reason the algorithm achieves mutual exclusion is that, when
$Past(i, j)$ is true, $Past(j,i)$ cannot become true because $x[i]$ is
true.  In other words, the following formula is an invariant of the
algorithm:
 \[ \A\, i \in Procs : \A\, j \in Procs :\: \{i\} :
                   Past(i, j) => ~Past(j, i) /\ x[i]
 \]
Use TLC to check that this is an invariant.  

An inductive invariant should contain a type-correctness invariant,
which I like to name $TypeOK$, as a conjunct.  However, the
conjunction of $TypeOK$ and the formula above isn't an inductive
invariant.  If you try writing a proof, you'll quickly discover why it
isn't.  However, for fun, let TLC show you it isn't.  Use 
 \lref{principles:tlc-inductive-check}{the method described above}
to have TLC check if this invariant is inductive.  (Use $N=2$.)
Examine the error trace and figure out why it isn't inductive.  (Don't
peek at what comes below.)

\bigskip

The error trace reveals that the invariant allows $Past(i,j)$ to be
true when $x[i]$ is false, which allows a step to make $Past(j,i)$
also true.  We need to add a conjunct asserting that $x[i]$ is true at
those points in the code where it obviously is true.  This leads us
to the following invariant:
\begin{display}
\begin{notla}
Inv == /\ TypeOK
       /\ \A i \in Procs : 
             /\ (pc[i] \in {"e2", "e3", "e6", "cs"}) => x[i] 
             /\ \A j \in Procs \ {i} : Past(i, j) => ~Past(j, i) /\ x[i]
\end{notla}
\begin{tlatex}
\@x{ Inv \.{\defeq} \.{\land} TypeOK\vs{.2}}
\ascii{onebitmutex-ascii2}%
\@x{\@s{34.04} \.{\land} \A\, i \.{\in} Procs \.{:}\vs{.2}}%
 \@x{\@s{52.37} \.{\land} ( pc [ i ] \.{\in} \{\@w{e2} ,\,\@w{e3} ,\,\@w{e6}
 ,\,\@w{cs} \} ) \.{\implies} x [ i ]\vs{.2}}%
 \@x{\@s{52.37} \.{\land} \A\, j \.{\in} Procs \.{\,\backslash\,} \{ i \}
 \.{:} Past ( i ,\, j ) \.{\implies} {\lnot} Past ( j ,\, i ) \.{\land} x [ i
 ]}%
\end{tlatex}
\end{display}
Use TLC to check that this is an inductive invariant for $N=2$.


\begin{aquestion}{mutex-answer9}
How many states must TLC generate in the course of checking that
$Inv$ is an inductive invariant for $N=3$?
\end{aquestion}

\begin{question}
Write a proof that $Inv$ is an inductive invariant of the algorithm,
and that it implies ${MutualExclusion}$.
\end{question}
%
%
Let's now show that the algorithm is deadlock free.  For that, it
suffices to assume that, at some time during the execution, some
process is trying to enter its critical section but no process ever
does, and to obtain a contradiction.  
 %
A naive argument goes as follows: Consider the smallest $i$ for which
$Trying(i)$ ever becomes true.  Since any non-trying process $j$
eventually sets $x[j]$ false, eventually process $i$ never reads
$x[j]$ true for any $j$ less than $i$, so it never sets $x[i]$ false.
Therefore, every other waiting process must eventually reach $e5$ and
wait forever for $x[i]$ to become false.  At this point, $x[j]$ is
false for all $j#i$, so process $i$ must eventually enter the critical
section, which is the required contradiction.

This kind of reasoning about executions is unreliable; it's easy to
miss a possible sequence of actions.  In fact, the argument above is
wrong because it ignores the possibility that process~$i$ is waiting
for $x[j]$ to become false, for some $j>i$, but $j$ is one of a group
of processes that keep continually looping from $e1$ to $e5$ and back.
Process $j$ keeps setting $x[j]$ alternately false and true, and
process $i$ is unlucky and keeps reading $x[j]$ when it is true,
remaining forever at $e6$.  We need a more rigorous proof.

A rigorous liveness proof needs an invariant.  Once again, the
invariant $Inv$ used to prove mutual exclusion isn't strong enough to
prove deadlock freedom because it asserts when $x[i]$ must be true,
but not when it must be false.  An inductive invariant that does the
job is:
\begin{display}
\begin{notla}
LInv == /\ Inv
        /\ \A i \in Procs : 
              /\ i \notin unchecked[i]
              /\ (pc[i] \in {"ncs", "e5"}) => ~x[i]
              /\ (pc[i] = "e3") => (other[i] # i)
              /\ (pc[i] \in {"e4", "e5"}) => (i > other[i])
              /\ (pc[i] = "e6") => (other[i] > i)
\end{notla}
\begin{tlatex}
\@x{ LInv \.{\defeq} \.{\land} Inv}%
\@x{\@s{40.31} \.{\land} \A\, i \.{\in} Procs \.{:}}%
\@x{\@s{58.64} \.{\land} i \.{\notin} unchecked [ i ]}%
 \@x{\@s{58.64} \.{\land} ( pc [ i ] \.{\in} \{\@w{ncs} ,\,\@w{e5} \} )
 \.{\implies} {\lnot} x [ i ]}%
 \@x{\@s{58.64} \.{\land} ( pc [ i ] \.{=}\@w{e3} ) \.{\implies} ( other [ i ]
 \.{\neq} i )}%
 \@x{\@s{58.64} \.{\land} ( pc [ i ] \.{\in} \{\@w{e4} ,\,\@w{e5} \} )
 \.{\implies} ( i \.{>} other [ i ] )}%
 \@x{\@s{58.64} \.{\land} ( pc [ i ] \.{=}\@w{e6} ) \.{\implies} ( other [ i ]
 \.{>} i )}%
\end{tlatex}
\end{display}
\begin{question}
Use TLC to check that $LInv$ is an inductive invariant of the algorithm, then
prove that it is
\end{question}
Here is
  \popref{n-proc-mutex-liveness}{a more rigorous proof of deadlock freedom}.
\begin{question}
Make this liveness proof more rigorous by expanding the proof sketches
of steps 7--9 into another level of structured proof.
\end{question}


\subsection{The Bakery Algorithm}

  \tindex{1}{bakery algorithm}%
Dijkstra's 1965 paper inspired the publication of many mutual
exclusion algorithms.  The first, published four months later by
Harris 
  \tindex{1}{Hyman, Harris}%
Hyman, was incorrect.  Four months after that, Donald 
  \tindex{1}{Knuth, Donald Ervin}%
Knuth
published an article pointing out the error in Hyman's algorithm and
presenting the first starvation-free mutual exclusion algorithm.
Since then, there have probably been hundreds of published mutual
exclusion algorithms.  My favorite is called the \emph{bakery
algorithm}.  It's my favorite because it's the first one that I
invented, because it's simple, and because it has a remarkable
property that I'll discuss \lref{real-bakery}{later}.

The inspiration for the bakery algorithm comes from a common method
for serving customers that I first saw as a child in a neighborhood
bakery.  Each arriving customer gets a numbered ticket from a
dispenser, tickets being numbered successively.  The waiting customer
with the lowest numbered ticket is the next one served.

In the bakery algorithm, each process that wants to enter its critical
section obtains a number, and the process with the lowest number
enters its critical section.  In keeping with the metaphor, we say
that a process that is \emph{not} in its non-critical section is in
the bakery.  Upon entering the bakery, a process obtains its number by
reading the numbers of all other processes in the bakery and setting
its own number to a number higher than any that it reads.  (The
obvious such number is one greater than the highest number it reads,
but any larger number also works.)  Processes outside the bakery have
their numbers equal to 0, so a process entering the bakery simply sets
its number to be greater than that of any other process, inside or
outside the bakery.

The obvious problem with this approach is that two processes entering
the bakery at the same time can choose the same number.  This problem
is easily solved by naming the processes with numbers and using
process names to break ties: if two processes choose the same number,
the one with the smallest name enters its critical section first.

\subsubsection{The Big-Step Algorithm}

\tindex{1}{big-step bakery algorithm}%
We first write a version of the bakery algorithm called the
\emph{big-step} 
algorithm in which a process's entire operation of
choosing its number is a single step.  Having a process read every
other process's number and set its own number all in a single step
makes the algorithm rather uninteresting.  In fact, it makes it
impossible for two different processes ever to have the same non-zero
number.  However, to make the transition to the finer-grained
algorithm easier, we'll ignore that and write the big-step algorithm
as if it were necessary to use process names to break ties.

\paragraph{The Algorithm}\mbox{}\\
We start by declaring the number $N$ of processes and defining $Procs$
to be the set of processes---more precisely, the set of process names,
which are numbers from 1 through $N$.
\begin{display}
\begin{notla}
-------------------------- MODULE BigStepBakery -------------------------
EXTENDS Integers

CONSTANT N
ASSUME N \in Nat

Procs == 1..N
\end{notla}
\begin{tlatex}
\@x{}\moduleLeftDash\@xx{ {\MODULE} BigStepBakery}\moduleRightDash\@xx{}%
\@x{ {\EXTENDS} Integers}%
\@pvspace{8.0pt}%
\@x{ {\CONSTANT} N}%
\@x{ {\ASSUME} N \.{\in} Nat}%
\@pvspace{8.0pt}%
\@x{ Procs \.{\defeq} 1 \.{\dotdot} N}%
\end{tlatex}
\end{display}
The algorithm uses an array $num$, where $num[p]$ is process $p$'s
number.  We define $\prec$ on pairs of integers so that, if processes
$p$ and $q$ are in the bakery, then $p$ enters its critical section
before $q$ does iff $<<num[p],p>> \prec <<num[q], q>>$.  This is the
case iff either $num[p]$ is less than $num[q]$ or else they are equal
and $p<q$.  The \tlaplus\ definition of $\prec$ is
\begin{display}
\begin{notla}
a \prec b == \/ a[1] < b[1]
             \/ (a[1] = b[1]) /\ (a[2] < b[2])
\end{notla}
\begin{tlatex}
\@x{ a \.{\prec} b \.{\defeq} \.{\lor} a [ 1 ] \.{<} b [ 1 ]}%
 \@x{\@s{43.33} \.{\lor} ( a [ 1 ] \.{=} b [ 1 ] ) \.{\land} ( a [ 2 ] \.{<} b
 [ 2 ] )}%
\end{tlatex}
\end{display}
The relation $\prec$ is called the \emph{lexicographical 
  \tindex{1}{lexicographical ordering}%
  \ctindex{1}{order!lexicographic}{order-lexicographic}%
ordering} on the
set of pairs of numbers.  It is a total ordering on pairs of numbers,
meaning that for any pairs $A$, $B$, and $C$ of numbers:
\begin{itemize}
\item $A \prec B$ and $B \prec C$ imply $A \prec C$.

\item Exactly one of the relations $A \prec B$, $B \prec A$, or
$A = B$ holds.
\end{itemize}
%
Upon entering the bakery, process $p$ can set $num[p]$ to any
natural number that is greater than $num[q]$ for every other process $q$.
The set of all such numbers is:
 \[ \{ j \in Nat : \A q \in Procs :\: \{p\}: j > num[q] \}
 \]
Since $num[p]$ equals 0 at that point, this expression can be simplified
a bit to:
  \[ \{ j \in Nat : \A q \in Procs : j > num[q] \}
  \]
\popref{bigstepbakery}{Here is the PlusCal code.} In addition to the
variable $num$, it declares the process-local variable $unchecked$.  A
process uses $unchecked$ to store the set of other processes that it
has determined it does not have to wait for.  To simplify the
type-correctness invariant, $unchecked$ is initialized to the empty
set even though its initial value is never used.  Here are what the
algorithm's atomic actions do:
\begin{itemize}
\item The actions corresponding to the labels $cs$ and $ncs$ represent
the critical and non-critical sections, respectively.

\item The $enter$ action sets $num[self]$ to an arbitrary integer
greater than $num[i]$ for all processes $i$.  It also initializes 
$unchecked$ to the set of all processes except $self$.

\item The $wait$ statement's \textbf{while} loop chooses an arbitrary
process $i$ in $unchecked$ and, if $num[i]$ equals 0 (so $i$ is not in
the bakery) or $<<num[self], self>>$ precedes $<<num[i],i>>$ in the
lexicographical ordering (so process $self$ should enter its critical
section before process $i$ does), then it removes $i$ from $unchecked$.
The loop terminates and $self$ enters its critical section when
$unchecked$ is empty.

\item After leaving the critical section, the process executes the $exit$
statement to set $num[self]$ to 0 and enters the non-critical section.
\end{itemize}


\paragraph{Safety}\mbox{}\\
The type-correctness invariant and the invariant asserting the mutual
exclusion property are:
\begin{display}
\begin{notla}
TypeOK == /\ num \in [Procs -> Nat]
          /\ unchecked \in [Procs -> SUBSET Procs]
          /\ pc \in [Procs -> {"ncs", "enter", "wait", "cs", "exit"}]
          
MutualExclusion == 
    \A p, q \in Procs : (p # q) => ~((pc[p] = "cs") /\ (pc[q] = "cs"))
\end{notla}
\begin{tlatex}
\@x{ TypeOK \.{\defeq} \.{\land} num \.{\in} [ Procs \.{\rightarrow} Nat ]}%
 \@x{\@s{56.14} \.{\land} unchecked \.{\in} [ Procs \.{\rightarrow} {\SUBSET}
 Procs ]}%
 \@x{\@s{56.14} \.{\land} pc \.{\in} [ Procs \.{\rightarrow} \{\@w{ncs}
 ,\,\@w{enter} ,\,\@w{wait} ,\,\@w{cs} ,\,\@w{exit} \} ]}%
\@pvspace{8.0pt}%
\@x{ MutualExclusion \.{\defeq}}%
 \@x{\@s{16.4} \A\, p ,\, q \.{\in} Procs \.{:} ( p \.{\neq} q ) \.{\implies}
 {\lnot} ( ( pc [ p ] \.{=}\@w{cs} ) \.{\land} ( pc [ q ] \.{=}\@w{cs} ) )}%
\end{tlatex}
\end{display}
\popref{bigstepbakery-ascii}{Here is the \textsc{ascii} version} of a
module containing the algorithm and the \tlaplus\ declarations and
definitions.  Use it to create a new specification in the Toolbox.  It
will report undefined operator errors until you run the PlusCal
translator.

To check the algorithm with TLC, you will have to use a model that
redefines $Nat$ to be a finite set of numbers.  For the assumption $N
\in Nat$ and type correctness to hold, $Nat$ must contain 0 and $N$.
A model with $N$ equal to 3 and $Nat$ defined to equal $0\dd 5$ has
only 2528 reachable states, and TLC quickly checks that it satisfies
the two invariants.  TLC finds no errors on the small models it can
check quickly.  While we let it run on a larger model, it's time to
prove that the algorithm satisfies mutual exclusion.

You will probably find the following argument the most intuitively
appealing.  Suppose process $p$ has entered the bakery and set
$num[p]$.  Any process $q$ that then enters the bakery sets $num[q]$
greater than $num[p]$, and therefore $q$ cannot enter the critical
section while $p$ is still in the bakery.  Two processes therefore
can't be in their critical sections at the same time, since one of
them must have set its number after the other did.  To make this proof
more rigorous, we must recast it in terms of an invariant.

Mutual exclusion clearly depends on the invariance of:
\begin{display}
\textbf{NumPos } If a process $p$ is at its $wait$ statement or
critical section, then $num[p]>0$ holds.
\end{display}
Liveness also depends on the fact that $num[p]=0$ when $p$ is in its
noncritical section.  To avoid having two separate invariants for
safety and liveness, we strengthen NumPos to
\begin{display}
\textbf{NumPos } $num[p]>0$ iff process $p$ is at its $wait$
statement, its critical section, or its $exit$ statement.
\end{display}
To write the more interesting part of the invariant, let's define:
\begin{display}
\begin{notla}
Before(p, q) == \/ num[q] = 0
                \/ <<num[p], p>> \prec <<num[q], q>>
\end{notla}
\begin{tlatex}
\@x{ Before ( p ,\, q ) \.{\defeq} \.{\lor} num [ q ] \.{=} 0}%
 \@x{\@s{72.87} \.{\lor} {\langle} num [ p ] ,\, p {\rangle} \.{\prec}
 {\langle} num [ q ] ,\, q {\rangle}}%
\end{tlatex}
\end{display}
(For the proof of the big-step algorithm, we could replace the second
disjunct by $num[p]<num[q]$.)  The key invariant is:
\begin{display}
\textbf{Before } If a process $p$ is either at the $wait$
statement and has executed the \textbf{while} loop iteration for
process $q$, or is in its critical section, then $Before(p, q)$ is
true.
\end{display}
The NumPos and Before invariants imply mutual exclusion because:
\begin{display}
\pflongindent
\pflongnumbers
\beforePfSpace{0pt}
\afterPfSpace{0pt, .3em}
\interStepSpace{.5em}
\begin{proof}
\step{1}{It suffices to assume two different processes $p$ and $q$ are in 
         their critical sections and obtain a contradiction.}
\begin{proof}
\pf\ Obvious.
\end{proof}
\step{2}{$Before(p,q) \;/\ \; Before(q,p)$}
\begin{proof}
\pf\ By \stepref{1} and invariant Before.
\end{proof}

\step{3}{$(num[p]>0) \;/\ \; (num[q]>0)$}
\begin{proof}
\pf\ By \stepref{1} and invariant NumPos.
\end{proof}

\step{4}{$(<<num[p],p>>\prec <<num[q],q>>) \; /\ \; 
    (<<num[q],q>>\prec <<num[p],p>>) $}
\begin{proof}
\pf\ By \stepref{2}, \stepref{3}, and the definition of $Before$.
\end{proof}

\qedstep
\begin{proof}
\pf\ Since $\prec$ is a total ordering on the set of pairs
of integers, \stepref{4} is impossible.
\end{proof}
\end{proof}
\end{display}
%
The conjunction of invariants NumPos and Before and the
type-correctness invariants is an inductive invariant.  To define it
precisely, we observe that the set $unchecked[p]$
 \marginpar{ Remember that $unchecked[p]$ is $p$'s \\ ``copy''
 of the local \\ variable $unchecked$.}
contains the processes for which $p$ has not yet executed the
\textbf{while} loop body.  
% 
% Because $unchecked[p]$ is the empty set when $p$ is in its critical
% section, we can write our complete inductive invariant as:
% 
\begin{display}
\begin{notla}
Inv == /\ TypeOK
       /\ \A p \in Procs : 
             /\ (pc[p] \in {"wait", "cs", "exit"}) <=> (num[p] > 0) 
             /\ \A q \in (Procs \ {p}) :
                   \/ (pc[p] = "wait") /\ (q \notin unchecked[p])
                   \/ pc[p] = "cs" 
                   => Before(p, q)
\end{notla}
\begin{tlatex}
\@x{ Inv \.{\defeq} \.{\land} TypeOK}%
\@x{\@s{34.04} \.{\land} \A\, p \.{\in} Procs \.{:}}%
 \@x{\@s{52.37} \.{\land} ( pc [ p ] \.{\in} \{\@w{wait} ,\,\@w{cs}
 ,\,\@w{exit} \} ) \.{\equiv} ( num [ p ] \.{>} 0 )}%
 \@x{\@s{52.37} \.{\land} \A\, q \.{\in} ( Procs \.{\,\backslash\,} \{ p \} )
 \.{:}}%
 \@x{\@s{70.70} \.{\lor} ( pc [ p ] \.{=}\@w{wait} ) \.{\land} ( q \.{\notin}
 unchecked [ p ] )}%
\ascii{bigstepinv-ascii}%
\@x{\@s{70.70} \.{\lor} pc [ p ] \.{=}\@w{cs}}%
\@x{\@s{70.70} \.{\implies} Before ( p ,\, q )}%
\end{tlatex}
\end{display}
\begin{problem}
(a)~Using the method described in 
  \lref{\xlink{checking-inductive-invariant}}{Section~\xref{checking-inductive-invariant}},
check that $Inv$ is an inductive invariant of the big-step algorithm.

(b)~Prove that $Inv$ is an inductive invariant of the algorithm,
completing the proof that the big-step algorithm satisfies mutual
exclusion.
\end{problem}

\paragraph{Liveness}\mbox{}\\
%
Let us now check that the big-step bakery algorithm is starvation
free.  First, we need to add a fairness assumption for the algorithm.
As usual, we assume fairness for each process by adding the keyword
\textbf{fair} before the keyword \textbf{process} in the PlusCal code.
As we observed in
  \lref{\xlink{requirement-c}}{Section~\xref{requirement-c}},
satisfying Dijkstra's requirement (c) means we must allow a process to
stop in its non-critical section, which we do by putting
``\texttt{-}'' after the label ``\texttt{ncs:}''.  Make those changes
and re-translate the algorithm.

Recall the \lref{deadlock-free}{definition of $DeadlockFree$}
given above for the one-bit algorithm.  Modifying the definitions
for the big-step bakery algorithm yields:
\begin{display}
\begin{notla}
Trying(p) == pc[p] \in {"enter", "wait"}
InCS(p)   == pc[p] = "cs"
DeadlockFree == (\E p \in Procs : Trying(p)) ~> (\E p \in Procs : InCS(p))
\end{notla}
\begin{tlatex}
\@x{ Trying ( p ) \.{\defeq} pc [ p ] \.{\in} \{\@w{enter} ,\,\@w{wait} \}\vs{.2}}%
\ascii{big-step-deadlock-free-ascii}
\@x{ InCS ( p )\@s{6.18} \.{\defeq} pc [ p ] \.{=}\@w{cs}\vs{.2}}%
 \@x{ DeadlockFree \.{\defeq} ( \E\, p \.{\in} Procs \.{:} Trying ( p ) )
 \.{\leadsto} ( \E\, p \.{\in} Procs \.{:} InCS ( p ) )}%
\end{tlatex}
\end{display}
Add those definitions to the module and have TLC check the property
$DeadlockFree$.  It should succeed.

In \lref{\xlink{mutex-question3}}{Question~\xref{mutex-question3}},
you defined starvation freedom by:
 \[ StarvationFree == \A \,p \in Procs : Trying(p) ~> InCS(p) \]
(We are using the simpler definition, which assumes that a process
may not stop in its critical section.)  Add that definition to the
model and have TLC check that the algorithm satisfies it.
TLC reports that the property is not satisfied!  Have we made a 
mistake?  Before reading further, examine the error trace and see
if you can figure out what happened.

\bigskip

When I check starvation freedom for the model with $N <- 3$ and $Nat
<- 0\dd5$, TLC produces an error trace that ends with processes 1 and
2 always at statement $enter$, and process 3
forever repeating the following sequence of steps:
\begin{itemize}
\item Enter the bakery.

\item Set $num[3]$ to 5.

\item Execute the $wait$ loop, seeing $num[1]$ and $num[2]$ equal to
0, and enter the critical section.

\item Exit the critical section and return to the non-critical section.
\end{itemize}
This behavior is not allowed by the algorithm.  Processes 1 and 2 have
stopped at statement $enter$ even though the $enter$ action is always
enabled.  (Since there are a finite number of processes, it is always
possible to choose a natural number that is greater than $num[p]$ for
all processes $p$.)  Hence, this behavior does not satisfy the
assumption of weak fairness for all processes, so it is not a behavior
of the algorithm.

TLC reports the violation because it isn't checking if the algorithm
is starvation free; it's checking if a \emph{model} of the algorithm
is starvation free.  In my model, $Nat$ is defined to equal $0\dd5$.
There is no element of $0\dd5$ greater than 5.  Hence, the $enter$
action of processes 1 and 2 is not enabled if $num[3]=5$.  The model
allows this behavior because weak fairness does not require a process
to execute an action that is continually disabled.

TLC can check only models of the algorithm in which $Nat$ is replaced
with a bounded set of numbers, and any such model will allow behaviors
that are not starvation free because some process $p$ keeps setting
$num[p]$ equal to the largest number in $Nat$.  To check if the
algorithm is starvation free, we have to tell TLC to ignore this class
of behaviors.  We do this by adding a 
  \emph{state
  \ctindex{2}{state constraint}{state-constraint}%
  \ctindex{2}{constraint, state}{constraint-state}%
constraint} to the model.  A state constraint is a state predicate $P$
(a formula containing no primes or temporal operators) that tells TLC
to examine only behaviors in which each state satisfies $P$.  More
precisely, when it finds a reachable state $s$ that does not satisfy
$P$, it does not look for states that are reachable from $s$.
(However, it will test if $s$ satisfies the invariants it is
checking.)  For my model with $Nat$ equal to $0\dd5$, I enter the
state constraint
 \[ \A p \in Procs : num[p] < 5
 \]
in the \textsf{State Constraint} field on the \textsf{Advanced
Options} model page.  TLC then reports that property $StarvationFree$
is satisfied by the model.

The problem of errors that occur in a model but not in the actual
algorithm can occur when checking any kind of property with TLC\@.
However, it seems to be more common when checking liveness than when
checking safety.  For safety properties, a state constraint usually
provides a satisfactory solution.  For liveness properties, the
constraint could easily cause TLC not to check actual behaviors of the
algorithm that violate the property.  For example, TLC could not find
a failure of starvation freedom in the bakery algorithm caused by a
process never entering its critical section because other processes
kept setting their numbers to ever increasing values.  We need to
prove that this is impossible.  Still, we should let TLC try to find
whatever errors it can.  There's no point trying to write a proof if
TLC can find a counterexample.


\begin{aquestion}{mutex-answer10}
Find an algorithm that satisfies an invariant, but for which the
invariant is violated by any model TLC can check---if the model doesn't
use a state constraint.
\end{aquestion}
%
Let's now prove that the big-step bakery algorithm is starvation free.
It, and the actual bakery algorithm, satisfy the stronger property of
being first-come-first-served%
  \tindex{1}{first-come-first-served}
(FCFS%
  \tindex{1}{FCFS}).  
Not only does each process trying to enter its critical section do so,
but it enters before any process that enters the bakery algorithm
after it does.  More precisely, if process $p$ executes the $enter$
statement before process $q$ does, then $p$ enters the critical
section before $q$ does.  First-come-first-served is described
formally by the property $FCFS$, defined as follows.
\begin{display}
\begin{notla}
InNCS(p)   == pc[p] = "ncs"

Waiting(p) == pc[p] = "wait"

FCFS  == 
   \A p, q \in Procs : 
       [](Waiting(p)  /\  InNCS(q)  /\  []~InCS(p)  =>  []~InCS(q))
\end{notla}
\begin{tlatex}
\@x{ InNCS ( p )\@s{8.2} \.{\defeq} pc [ p ] \.{=}\@w{ncs}}%
\@pvspace{4.0pt}%
\@x{ Waiting ( p )\@s{3.42} \.{\defeq} pc [ p ] \.{=}\@w{wait}}%
\@pvspace{4.0pt}%
\@x{ FCFS\@s{4.1} \.{\defeq}}%
\@x{\@s{12.29} \A\, p ,\, q \.{\in} Procs \.{:}}%
 \@x{\@s{25.26} {\Box} ( Waiting ( p )\@s{4.1} \.{\land}\@s{4.1} InNCS ( q
 )\@s{4.1} \.{\land}\@s{4.1} {\Box} {\lnot} InCS ( p )\@s{4.1}
 \.{\implies}\@s{4.1} {\Box} {\lnot} InCS ( q ) )}%
\end{tlatex}
\end{display}
It is easy to see why this property holds.  From 
  $Waiting(p) /\ []~InCS(p)$, we deduce that $Waiting(p)$ remains
forever true, with $num[p]>0$.  From $InNCS(q)$ we can then deduce
that if $q$ tries to enter its critical section, it will set $num[q]$
greater than $num[p]$ and will wait forever in its \textbf{await}
statement with $i=p$.  Here is \popref{bakery-fcfs}{a more rigorous
proof}.

FCFS is a \rref{safe-live-intro}{top}{safety property}; starvation
freedom is a liveness property.  A safety property cannot imply a
liveness property---except in trivial cases.  (For example, the safety
property \FALSE\ implies every liveness property.)  Starvation freedom
is implied by FCFS and deadlock freedom.  The idea of the proof is
simple.  Suppose a process $p$ is trying to enter its critical
section.  FCFS implies that no process that later tries to enter its
critical section can succeed before $p$.  Deadlock freedom implies
that as long as $p$ is trying to enter, processes must keep entering
and leaving the critical section.  Since there can be only a finite
number of processes waiting at any time, eventually no process other
than $p$ will be able to enter the critical section, so it must do so.
Here is \popref{fcfs-starvation-free}{a more rigorous proof} of this
result.  Thus, to prove that the big-step bakery algorithm is starvation
free, we just have to prove that it is deadlock free.  This is left as
an exercise:
\begin{problem}
Prove $Spec => DeadlockFree$.
\end{problem}

   \tindex{2}{grain of atomicity}%
   \ctindex{2}{atomicity!grain of}{atomicity-grain}%
   \vspace{-1.5\baselineskip}%
\subsubsection{Choosing the Grain of Atomicity} \xlabel{atom-grain}

The big-step bakery algorithm isn't a useful algorithm because it
assumes that process $self$ can read $num[i]$ for all other processes~$i$
and set $num[self]$ all in a single step.  The only way I know of making
such an operation act like an atomic step is to put it in the critical
section of a mutual exclusion algorithm---not helpful if we're trying
to implement mutual exclusion.  So, we want a finer-grained algorithm.

The algorithm's \textbf{process} declaration should look something 
   \popref{badbakery1}{like this},
where the \textbf{with} statement of the Big-Step algorithm has been
refined to a \textbf{while} loop that reads the 
values $num[i]$ individually, for all
$i#self$, and then sets $num[self]$.  I have not yet added the labels
that specify exactly what the atomic steps are.  We
now consider how that should be done.

Dijkstra assumed that reading or writing a single word of memory is an
atomic action.  Viewing Dijkstra's paper from the perspective of our
standard model, we would phrase this assumption as follows.  The
system's state consists of a collection of memory words that can be
read and written by all the processes, together with a collection of
registers, each local to a single process.  An operation of a process
may be taken to be atomic if it reads or writes at most one word of
memory.  The operation may perform arbitrary operations on its local
registers.  We would justify this assumption by arguing that, because
the operations to the local registers cannot affect or be affected by
operations performed by another process, we can assume that they all
occur at the same instant, which is the same instant as the read or
write of memory (if there is such a read or write) is performed.

Memory and registers are meaningful concepts for a computer, but not
for an algorithm.  When computer scientists generalized from computers
to processes, they (often implicitly) partitioned the state of an
algorithm into elementary 
  \tindex{1}{elementary data item}%
  \tindex{1}{data item, elementary}%
data items, some shared by multiple
processes and others local to individual processes.  Typically, an
integer-valued variable was taken to be an elementary data
item---tacitly assuming that an implementation would ensure that its
value remained small enough to fit in a single word of physical
memory.  For now, let us take $num[i]$, $unchecked[i]$, $max[i]$, and
$pc[i]$, for all processes $i$, to be the elementary data items of the
bakery algorithm.  (Remember that process $i$'s copies of the
process-local variables $unchecked$ and $max$ are the array elements
$unchecked[i]$ and $max[i]$.)

Dijkstra's assumption translates to the requirement that an atomic
action contain at most one read or write of at most one
shared elementary data item.  A closer look at its justification,
which involves grouping together operations that are invisible to
another process into a single atomic action, shows that we can weaken
that requirement to the following:
\begin{display}
\textbf{Single Access Rule } 
  \tindex{1}{single access rule}\target{single-access}%
A single atomic action of a process may
contain either (a)~a single write to a shared elementary data item or
(b)~a single read of a shared data item that may be written by another
process (but not both).
\end{display}
For example, the following atomic action $a$
\begin{display}
\begin{nopcal}
a: num[self] := num[self] + max ;
   unchecked[self] := Procs ;
b: 
\end{nopcal}
\begin{tlatex}
 \@x{ a\@s{.5}\textrm{:}\@s{3} num [ self ] \.{:=} num [ self ] \.{+} max
 {\p@semicolon}}%
\@x{\@s{12.15} unchecked [ self ] \.{:=} Procs {\p@semicolon}}%
\@x{ b\@s{.5}\textrm{:}\@s{3}}%
\end{tlatex}
\end{display}
would satisfy the Single Access Rule for the bakery algorithm.  
It writes to the single data item $num[self]$, which is
allowed by condition~(a).  It also reads $num[self]$ and $max[self]$,
neither of which is written by any process other than $self$, and it
writes $unchecked[self]$, which is not shared.  (The constant $Procs$ is
not a data item because it is not part of the state.)

We want to represent the bakery algorithm as the coarsest-grain
PlusCal algorithm possible (the one with the biggest atomic steps)
that satisfies the Single Access Rule.  \popref{badbakery2}{Here is
how} we can add labels to do that.  (Note that statements $e2$ and
$wait$ both contain two occurrences of the shared data item $num[i]$.
We consider those two occurrences to represent a single read of
$num[i]$, since a sensible implementation of those statements would
read $num[i]$ only once.)  Before we examine this algorithm, let's
take a more critical look at the Single Access Rule.

\medskip

Let $\Pi$ be an algorithm satisfying the rule.  We can view it as an
abstract model of a finer-grained algorithm $\widehat{\Pi}$ that more
accurately models a real system.  What we would like to be
true is that the correctness of $\Pi$ implies the correctness of
$\widehat{\Pi}$, assuming that $\widehat{\Pi}$ maintains the atomicity
of reads and writes to shared elementary data items.  Whether or not
it \emph{is} true depends on what constitutes correctness.  For
example, suppose $x$ is an array of shared data items and $h$ is a
process-local variable.  A PlusCal algorithm $\Pi$ containing the
following action $a$
\begin{display}
\begin{nopcal}
a: h := h+1 ; 
   x[self] := h ; 
b: 
\end{nopcal}
\begin{tlatex}
\@x{ a\@s{.5}\textrm{:}\@s{3} h \.{:=} h \.{+} 1 {\p@semicolon}}%
\@x{\@s{12.15} x [ self ] \.{:=} h {\p@semicolon}}%
\@x{ b\@s{.5}\textrm{:}\@s{3}}%
\end{tlatex}
\end{display}
might satisfy the invariance property $[](x[i] = h[i])$ for every
process $i$.  However that property is not satisfied by the
finer-grained version $\widehat{\Pi}$ containing the steps:
\begin{display}
\begin{nopcal}
a:  h := h+1 ; 
a2: x[self] := h ; 
b: 
\end{nopcal}
\begin{tlatex}
\@x{ a\@s{.5}\textrm{:}\@s{3}\@s{5.00} h \.{:=} h \.{+} 1 {\p@semicolon}}%
\@x{ a2\@s{.5}\textrm{:}\@s{3} x [ self ] \.{:=} h {\p@semicolon}}%
\@x{ b\@s{.5}\textrm{:}\@s{3}}%
\end{tlatex}
\end{display}
We shouldn't expect an invariant of $\Pi$ to be an invariant of
$\widehat{\Pi}$ if it depends on the values of process-local data
items, since $\Pi$ combines multiple operations to those items in a
single atomic action.  However, we are doing that when 
we apply the Single Access Rule
to a mutual exclusion algorithm, whose correctness condition is the
invariance of a formula depending on the values of the process-local
data items $pc[i]$.

Even an invariant of $\Pi$ depending only on shared data items need
not be an invariant of $\widehat{\Pi}$.  Suppose $x$ is an array
of shared data items, $h$  is a process-local variable, and $\Pi$
contains the statement:
\begin{display}
\begin{nopcal}
a: with (i \in Nat) { h := i } ;
   x[self] := h ;
   await h = 42 ;
b: 
\end{nopcal}
\begin{tlatex}
 \@x{ a\@s{.5}\textrm{:}\@s{3} {\p@with} {\p@lparen} i \.{\in} Nat {\p@rparen}
 {\p@lbrace} h \.{:=} i {\p@rbrace} {\p@semicolon}}%
\@x{\@s{12.15} x [ self ] \.{:=} h\@s{9.74} {\p@semicolon}}%
\@x{\@s{12.15} {\p@await} h \.{=} 42 {\p@semicolon}}%
\@x{ b\@s{.5}\textrm{:}\@s{3}}%
\end{tlatex}
\end{display}
(Examining its \tlaplus\ translation shows that statement $a$ is a
complicated way of writing \tlabox{h := 42;\;x[self] := 42}.)  Algorithm
$\Pi$ might satisfy the invariance property $[](x[i] = 42)$ for all
processes~$i$.  Now let $\widehat{\Pi}$ be obtained by adding a label
to this code:
\begin{display}
\begin{nopcal}
a:  with (i \in Nat) { h := i } ;
    x[self] := h ;
a2: await h = 42 ;
b:
\end{nopcal}
\begin{tlatex}
 \@x{ a\@s{.5}\textrm{:}\@s{3}\@s{4.1} {\p@with} {\p@lparen} i \.{\in} Nat
 {\p@rparen} {\p@lbrace} h \.{:=} i {\p@rbrace} {\p@semicolon}}%
\@x{\@s{17.15} x [ self ] \.{:=} h\@s{9.74} {\p@semicolon}}%
\@x{ a2\@s{.5}\textrm{:}\@s{3} {\p@await} h \.{=} 42 {\p@semicolon}}%
\@x{ b\@s{.5}\textrm{:}\@s{3}}%
\end{tlatex}
\end{display}
(The modified code sets $h$ and $x[self]$ to an arbitrary natural number and
then stops unless $h=42$.)  Algorithm $\widehat{\Pi}$ does not satisfy that
invariance property.

In this example, the invariant of $\Pi$ fails to be an invariant of
$\widehat{\Pi}$ because the section of code consisting of statements
$a$ and $a2$ of $\widehat{\Pi}$ that implements the atomic action
$a$ of $\Pi$ allows executions that don't correspond to
executions of that atomic action.  It turns out that this is the
only way there can be a safety property satisfied by $\Pi$ that depends
only on shared data items but is not satisfied by $\widehat{\Pi}$.
In general, for any atomic action $A$ of $\Pi$, let $\widehat{A}$
be the section of PlusCal code that implements $A$ in $\widehat{\Pi}$.
Any safety property satisfied by $\Pi$ that depends only on shared
data items is also satisfied by $\widehat{\Pi}$ if the following condition
holds:
\begin{display}
For every atomic action $A$ of $\Pi$ and any states $s$ and $t$,
if executing $\widehat{A}$ starting in state $s$ can produce state $t$,
then executing $A$ in state $s$ can produce state $t$.
\end{display}
I will not try to state this result more rigorously.  In most modern
multiprocessor computers, each processor has its own cache, and
reading or writing a single word of memory cannot be regarded as an
atomic action.  The rationale behind the Single Access Rule is
therefore no longer valid.  Understanding the Single Access Rule will
help you determine the appropriate grain of atomicity for an algorithm.
However, determining if an algorithm is a useful model of a real system
requires an understanding of the algorithm, the system, and the
properties you are trying to check.

\medskip

I will let you convince yourself that \popref{badbakery2}{the
algorithm given above} has an appropriate grain of atomicity for
checking mutual exclusion, assuming that reads and writes of each data
item $num[i]$ are atomic.

\tindex{1}{atomic bakery algorithm}%
\ctindex{1}{bakery algorithm!atomic}{bakery-algorithm-atomic}%

\subsubsection{The Atomic Bakery Algorithm}

We now develop the \emph{atomic bakery algorithm}, so called because
reads and writes of each $num[i]$ are taken to be atomic.  I presented
an initial attempt at such an algorithm above.  Here is its 
\popref{badbakery-ascii}{complete ascii version}.  It does not implement
mutual exclusion.  Before reading any further, run TLC to see why not.

\bigskip

Here is the incorrect behavior that TLC produces for a model with $N<-2$
and $Nat <- 0\dd 4$.
\begin{itemize}
\item Both processes execute statement $e1$ and $e2$, reaching $e3$ with
$max=0$.  Process 1 then executes $e3$, setting $num[1]=2$, executes the
$wait$ loop (seeing $num[2]=0$), and reaches $cs$.

\item Process 2 then executes $e3$, setting $num[1]=1$, executes the
$wait$ loop (seeing $num[1]=2$, so \tlabox{<<num[2],2>>\prec<<num[1],1>>}),
and reaches $cs$, making $MutualExclusion$ false.
\end{itemize}
This incorrect execution would not occur if, instead of setting $num[self]$
to an arbitrary integer greater than $max$, it set $num[self]$ to $max+1$.
Make that change to the algorithm and use TLC to show that it is still
incorrect. 

\bigskip

With this change to the algorithm, TLC will find a behavior in which both
processes reach $e3$ with $max=1$.  Process~2 then executes the
waiting loop, sees $num[1]=0$, and reaches $cs$.  Process~1 then
executes the waiting loop, sees $num[2]=1$ and also reaches $cs$
because \tlabox{<<1,1>>\prec<<1,2>>}.

The scenario that must be prevented is processes $p$ and $q$ starting
in their non-critical sections and:
\begin{itemize}
\item Process $p$ reaches $e3$ after seeing $num[q]=0$.

\item Process $q$ reaches its critical section before $p$ sets $num[p]$.

\item Process $p$ then sets $num[p]\leq num[q]$, so $p$ does not
have to wait for process $q$ before entering its critical section.
\end{itemize}
We prevent the second item in the scenario by requiring $q$ to wait
for $p$ when $p$ has left its non-critical section but not yet set
$num[p]$.  To do this, we have process $p$ indicate that it is in this
part of its code by setting $flag[p]$ to $\TRUE$, where
$flag$ is a global variable of the algorithm.

\popref{atomic-bakery}{Here is the algorithm.} The 
  \ascii{atomic-bakery-ascii}%
Single Access Rule requires that the body of the waiting loop consist
of two separate actions: one reading $flag[i]$ and another reading
$num[i]$, for each process~$i$ in $unchecked$.  We therefore need an
additional local variable, which we call $nxt$, to remember which
process $i$ has been chosen from $unchecked$.  To simplify an
invariance proof, we initialize the local variables to type-correct
values even though those initial values are never used.

You can let TLC check that this algorithm does satisfy mutual
exclusion.  On my computer, it checks a model with $N<-3$ and
$Nat<-0\dd5$ in less than 1.5 minutes.  How large a model do you have
the patience to check?  Note that checking this model also checks any
model with $N\leq 3$ and $N$ a subset of $0\dd 5$, since it includes
executions in which a smaller number of processes actually take steps
and the $num[i]$ take only values in that subset.  Writing a rigorous
invariance proof of the atomic bakery algorithm is good practice.

\begin{aproblem}{atomic-bakery-inv}
Write a rigorous proof that the atomic bakery algorithm's specification 
implies $[]MutualExclusion$.  (Use TLC to help you find the inductive
invariant.)
\end{aproblem}
%
The bakery algorithm has the inelegant property that the values of the
data items $num[i]$ can get arbitrarily large.  We can keep them from
getting too large by replacing statement $e3$ with
\tlabox{num[self]:=max+1}.  It's easy to see that this keeps $num[i]$
at most equal to the number of times some process has tried to enter
its critical section.  So, if processes enter their critical section
no more than once a nanosecond, the value of $num[i]$ will fit in 64
bits of memory for 50000 years.  

It seems that by restricting $e3$ in this way, the non-zero values of
$num[i]$ at any one time will all lie within about $N$ of one another,
so we could allow the values of the $num[i]$ to cycle through a finite
set of integers.  In the following problem, you will show that this is
not possible.

\begin{hproblem}{bakery-ans1}
If $N\geq3$, then even if $e3$ is replaced by \tlabox{num[self]:=max+1},
for any two natural numbers $M$ and $P$, there is an execution in which
$num[i]=M$ and $num[j]=P$ for two processes $i$ and $j$.
\end{hproblem}
%
However, there is a two-process algorithm with a bounded
set of values.
\begin{aproblem}{2proc-bakery}
For $N=2$, find a version of the bakery algorithm in which there
is a finite set of values that always contains the value of each
$num[i]$.
\end{aproblem}
%
%
For liveness, as usual we turn the \textbf{process} declaration into a
\textbf{fair process} and allow a process to stop in its
non-critical section by putting ``\texttt{-}'' after the label
``\texttt{ncs:}''.  The proof that the atomic bakery algorithm is
starvation free is essentially the same as for the big-step algorithm.

\btarget{real-bakery}
\subsubsection{The Real Bakery Algorithm} 

While it may be useful, an algorithm that assumes atomic reads and
writes of shared data items cannot really be said to solve the mutual
exclusion problem.  Implementing those atomic reads and writes would
seem to require mutually exclusive access to the data items.  From a
scientific point of view, an algorithm that assumes lower-level mutual
exclusion cannot be said to solve the mutual exclusion problem.  

The most remarkable property of the bakery algorithm is that it does
not require atomic reads and writes of individual data items.  It
needs only two properties of reads and writes: (i)~a read that does
not overlap a write obtains the correct value, and (ii)~any read
obtains a value of the correct type.  For example, a read of $num[i]$
by a process other than process~$i$ returns the current value of
$num[i]$ if~$i$ is not writing the value during that read, and it
always returns a natural number.  Thus, $num[i]$ could be implemented
with an array of bits; process~$i$ can write $num[i]$ by writing the
bits one at a time in any order; another process can read $num[i]$ by
reading the bits in any order.  Reading and writing of an individual
bit need not even be atomic.

Here is one way to model such non-atomic reads and writes of $num[i]$:
Process~$i$ sets $num[i]$ to a number $m$ by first setting $num[i]$ to
a special value $\bot$ and then setting it to $m$.  A read by another
process reads the current value of $num[i]$ atomically, and it returns
an arbitrarily chosen natural number if it sees $num[i]$ equal to
$\bot$.

This way of modeling reads and writes is probably the best one for
model checking, since it seems to minimize the number of reachable
states.  However, there is another way that is more convenient for
reasoning about the algorithm: A process sets $num[i]$ to $m$ by first
performing a sequence of writes of arbitrarily chosen natural numbers
to $num[i]$, and then setting $num[i]$ to $m$.  A read just atomically
reads the current value of $num[i]$.  Here's the PlusCal code for the
bakery algorithm's $exit$ statement that sets $num[self]$ to $0$:
\begin{display}
\begin{nopcal}
exit: either {  with (k \in Nat) { num[self] := k } ;
                goto exit }
      or     { num[self] := 0 }
\end{nopcal}
\begin{tlatex}
 \@x{ exit\@s{.5}\textrm{:}\@s{3} {\p@either} {\p@lbrace}\@s{4.1} {\p@with}
 {\p@lparen} k \.{\in} Nat {\p@rparen} {\p@lbrace} num [ self ] \.{:=} k
 {\p@rbrace} {\p@semicolon}}%
\@x{\@s{69.70} {\p@goto} exit {\p@rbrace}}%
 \@x{\@s{22.85} {\p@or}\@s{18.84} {\p@lbrace} num [ self ] \.{:=} 0
 {\p@rbrace}}%
\end{tlatex}
\end{display}
Here is \popref{bakery-pcal}{the algorithm}.  (You can compare it to
\popref{atomic-bakery}{the atomic bakery algorithm}.)  Note that because
$flag[self]$ is Boolean-valued, we can simplify our modeling of writes
to it.  Here is \popref{bakery-ascii}{the \textsc{ascii} version}.  

TLC can check this algorithm on a model with $N<-2$ and $Nat <- 0\dd6$
in a couple of seconds.  It takes a couple of minutes for a model
with $N<-3$ and $Nat <- 0\dd3$.  TLC will not check a large enough model
to give us very much confidence in the algorithm's correctness; that
requires a proof.

\begin{hproblem}{bakery-hint}
Write a rigorous invariance proof that the specification $Spec$
of the bakery algorithm implies $[]MutualExclusion$.
\end{hproblem}
%
Making the \textbf{process} declaration a \textbf{fair process} does
not ensure that any process ever enters its critical section.  For
example, a process could loop forever in step $e1$, always choosing to
execute the \textbf{either} clause.  We need an additional fairness
condition to require that, if a process keeps executing $e1$, then it
will eventually execute the statement's \textbf{or} clause.  I think
it is impossible to express this requirement in PlusCal.  However, it
is expressed in \tlaplus\ by weak fairness of the action
  \marginpar{This action is equivalent to
              $e1(i) \land (pc'[i] = \mbox{\textsf{``$e2$''}})$.}
$e1(i) /\ (pc'[i] # pc[i])$, for 
each process~$i$.  When process
$i$ is looping at $e1$, this action is continuously enabled.  Weak fairness
implies that this action must eventually occur, which means that the
$e1$ \textbf{or} clause must eventually be executed.  Similar fairness
requirements are needed to prevent infinite looping at $e3$, $e4$,
and $exit$.  We can express these requirements with the formula
\begin{display}
\begin{notla}
\A i \in Procs : WF_vars(/\ e1(i) \/  e3(i) \/ e4(i) \/ exit(i)
                         /\ (pc'[i] # pc[i]))
\end{notla}
\begin{tlatex}
 \@x{ \A\, i \.{\in} Procs \.{:} {\WF}_{ vars} ( \.{\land} e1 ( i )
 \.{\lor}\@s{4.1} e3 ( i ) \.{\lor} e4 ( i ) \.{\lor} exit ( i )}%
\@x{\@s{94.46} \.{\land} ( pc \.{'} [ i ] \.{\neq} pc [ i ] ) )}%
\end{tlatex}
\end{display}
Define $FairSpec$ to be the conjunction of the formula $Spec$ of the
algorithm's \tlaplus\ translation with this formula.  Use TLC to check
that algorithm $FairSpec$ is deadlock free and starvation free.
(Remember that you have to use a state constraint when checking
starvation freedom.)  Checking liveness properties takes TLC longer
that checking safety properties, so you may want to use smaller models
than you used to check mutual exclusion.

The proofs of these liveness properties have the same general form
as the proofs for the other versions of the bakery algorithm.


\ctindex{1}{mutual exclusion!in modern computers}{mutex-modern}%
\subsection{Mutual Exclusion in Modern Programs}
 \xlabel{modern-mutex}

Most early solutions of the mutual exclusion problem assumed that
reading or writing a single value is an atomic action.  These
algorithms could easily be implemented in real programs because, in
the few multiprocess computers that existed, reading or writing a
single word of memory could be modeled was an atomic action.  Those
days are long gone.  In modern computers, each individual processor
(now usually called a \emph{core}) has its own memory cache.  Reading
or writing a single memory word is a complex operation that may
involve communication among multiple caches and main memory.  A read
or write is no longer accurately modeled as an atomic action.  A naive
implementation of an algorithm like the one-bit algorithm does not
ensure mutual exclusion.  Even the method of representing reads and
writes used in the bakery algorithm is not an accurate model for a
modern computer.  That model assumes a read or write operation is
completed before the next step is executed, but a modern computer will
continue executing the next program steps while actions that are part
of the operation are still being performed in various parts of the
memory system.

In today's multiprocess programs, processes don't communicate solely
by ordinary reading and writing of memory.  Modern computers provide
special instructions for interprocess synchronization.  These
instructions make it trivial to implement mutual exclusion.  Modern
programming languages also provide constructs for implementing mutual
exclusion.  A common construct is a 
  \tindex{1}{lock}%
\emph{lock} that can be acquired
and released by a process.  (Processes are usually called
\emph{threads}.)  At most one process can ``own'' a lock; another
process that tries to acquire the lock will wait until its owner
releases it.  Processes can use locks to execute multiple separate
mutual exclusion algorithms, each with its own critical section.

The function of mutual exclusion is to make execution of a process's
entire critical section act like an atomic action.  Consider a
multiprocess program in which each process has a single critical
section.  If the shared variables that are accessed in each process's
critical section are accessed by other processes only in their
critical sections, then an execution of each critical section can be
considered to be an atomic action.  Here is a more precise statement
of what ``can be considered to be an atomic action'' means: Let $\Psi$
be the the original program and let $\Pi$ be the program with the
critical sections made atomic actions.  Program $\Psi$ implements
program $\Pi$ under a refinement mapping such that, for every variable
$v$ of the two programs, \ov{v} equals $v$ in every state in which no
process is in its critical section.  (For the variable $pc$ of $\Pi$
such that $pc[p]$ represents the location of process $p$ in its code,
when $p$ is in its critical section, $\ov{pc}[p]$ equals the control
point either at or immediately after the atomic action that executes
the critical section.)

The generalization to processes that execute multiple mutual exclusion
algorithms is straightforward.  Here is the condition that allows
every critical section to be considered an atomic action: For each
critical section of each process $p$, the shared variables accessed in
that critical section cannot be accessed by any other process while
$p$ is executing the critical section.

If all shared variables are accessed only in critical sections and we
can consider those critical sections to be atomic actions, then we can
apply the \lref{single-access}{Single Access Rule}.

\begin{sloppypar}
I have been discussing programs as if they were precisely described by
\tlaplus\ specifications.  In principle, any discrete system,
including a multiprocess program, can be accurately described by such
a specification.  In practice, that's seldom the case.  The meaning of
the C statement \verb|x = x+1| in a real multiprocess program executed
on a real operating system running on a real computer would be quite
complicated (assuming it even had a precise meaning).  In an accurate
model of the program, an execution of the statement would probably
consist of dozens of steps.  An accurate model of an arbitrary
non-trivial multiprocess program would be impossible.
\end{sloppypar}

For this reason, we don't write arbitrary multiprocess programs.  We
write programs that access shared variables only in critical sections,
so we can consider those critical sections to be atomic actions, and
we can then apply the Single Access Rule.  In this way, we can obtain
an accurate model of the program---a model that we can describe
precisely in \tlaplus\ (or PlusCal).  A sensible programmer thinks
about the program in terms of such a model even if she doesn't write it
explicitly.  





\newpage


   \tindex{1}{bounded channel}%
\vspace{-\baselineskip}%
\section{The Bounded Channel and Bounded Buffer} \xlabel{sec:alternation}

\subsection{The Bounded Channel} \xlabel{sec:bded-channel}

\subsubsection{The Specification}
We now consider a two-process system in which a sender process puts
messages in a \emph{channel} that are removed in sequence by a
receiver process.  This is a
 \tindex{1}{FIFO (first in, first out)}%
FIFO (first in, first out) channel, meaning that messages are received
in the order in which they are sent.  We consider a \emph{bounded}
channel, which is one that can hold at most some number $N$ of
messages.  If the channel contains $N$ messages, then the sender
cannot send another message until a message is removed from the
channel by the receiver.  We use a variable $ch$ to represent the
sequence of messages in the channel.
We might draw a picture of the system like this:
\begin{center}
\begin{picture}(200,40)
\thicklines
\put(0,0){\framebox(50,40){$Sender$}}
\put(50,20){\vector(1,0){60}}
%\put(70,12.5){\framebox(80,15){\emph{channel}}}
%\put(70,12.5){\framebox(80,15){}}
%\put(110,29.5){\makebox(0,0)[b]{\emph{channel}}}
%\put(150,20){\vector(1,0){20}}
\put(80,22){\makebox(0,0)[b]{$ch$}}
\put(110,0){\framebox(50,40){$Receiver$}}
\end{picture}
\end{center}
Such pictures convey almost no useful information, but they help many
people understand the actual specification.

% We consider a \emph{bounded} channel, which is one that can hold at
% most some number $N$ of messages.  If the channel contains $N$ messages,
% then the sender cannot send another message until a message is removed
% from the channel by the receiver.

To model the sender and receiver, we pretend that the sequence of all
messages that the sender will send is known in advance.  Let's call it
$Input$.  We add a variable $in$ that holds the sequence of messages
that the sender has yet to send, initially equal to $Input$; and a
variable $out$ that holds the sequence of messages that the receiver
has received thus far, initially equal to the empty sequence.  Our
picture then becomes:
\begin{center}
\begin{picture}(200,40)
\thicklines
\put(-20,22){\makebox(0,0)[b]{$in$}}
\put(-40,20){\vector(1,0){40}}
\put(0,0){\framebox(50,40){$Sender$}}
\put(50,20){\vector(1,0){60}}
%\put(70,12.5){\framebox(80,15){\emph{channel}}}
%\put(70,12.5){\framebox(80,15){}}
%\put(110,29.5){\makebox(0,0)[b]{\emph{channel}}}
%\put(150,20){\vector(1,0){20}}
\put(80,22){\makebox(0,0)[b]{$ch$}}
\put(110,0){\framebox(50,40){$Receiver$}}
\put(180,22){\makebox(0,0)[b]{$out$}}
\put(160,20){\vector(1,0){40}}
\end{picture}
\end{center}
To model a system that runs forever, we let $Input$ be an infinite
sequence of messages.

Here is the \popref{pseudo-bounded-channel}{specification of the
bounded channel in pseudo-PlusCal}.  The processes are named $Send$
and $Rcv$ and have identifiers 0 and 1, respectively.  To turn this
pseudo-code into real PlusCal code, we need to know how to represent
operations on sequences.  

In \tlaplus, a finite
   \ctindex{1}{sequence!finite}{seq-finite}%
sequence is the same as a
  \ctindex{1}{tuple!same as sequence}{tuple-same-as-sequence}%
tuple.  Finite sequences/tuples are explained in 
  \rref{math}{\xlink{math:function-domains}}{Section~\xref{math:function-domains}}
and
  \rref{math}{\xlink{math:tuples}}{Section~\xref{math:tuples}}.
Therefore, the empty sequence is the empty tuple $<<\,>>$, so the variable
declarations can be written:
\begin{display}
\begin{nopcal}
variables in = Input, out = << >>, ch = << >>;
\end{nopcal}
\begin{tlatex}
 \@x{ {\p@variables} in \.{=} Input ,\, out \.{=} {\langle}\,{\rangle} ,\, ch
 \.{=} {\langle}\,{\rangle} {\p@semicolon}}%
\end{tlatex}
\end{display}
For writing the spec, you will need to know only these
operators that are defined in  the 
  \rref{math}{math:sequences-module}{standard $Sequences$ module}:
$Seq$, $Len$, $Append$, $Head$, and $Tail$.  Since $ch$ and $out$ are
finite sequences, we can write the body of the receiver's \textbf{while}
loop as:
%
\begin{display}
\begin{nopcal}
await Len(ch) # 0 ;
out := Append(out, Head(ch)) ;
ch := Tail(ch)
\end{nopcal}
\begin{tlatex}
\@x{ {\p@await} Len ( ch ) \.{\neq} 0 {\p@semicolon}}%
\@x{ out \.{:=} Append ( out ,\, Head ( ch ) ) {\p@semicolon}}%
\@x{ ch \.{:=} Tail ( ch )}%
\end{tlatex}
\end{display}
If $in$ were a finite sequence, we could write the body of the sender's
\textbf{while} loop as:
\begin{display}
\begin{nopcal}
await Len(ch) # N ;
ch := Append(ch, Head(in)) ;
in := Tail(in)
\end{nopcal}
\begin{tlatex}
\@x{ {\p@await} Len ( ch ) \.{\neq} N {\p@semicolon}}%
\@x{ ch \.{:=} Append ( ch ,\, Head ( in ) ) {\p@semicolon}}%
\@x{ in\@s{1.02} \.{:=} Tail ( in )}%
\end{tlatex}
\end{display}
Since $in$ is an infinite sequence, we need to replace $Head$ and $Tail$
with operators to take the head and tail of an infinite sequence.  To do
that, we have to decide how to represent an infinite sequence in terms of
the mathematical sets and operators we have at our disposal.  

A length-$k$ sequence $s$ is a function with domain $1\dd k$, where
$s[i]$ is the $i$\tth\ element of $s$.  
 \tindex{1}{infinite sequence}%
 \ctindex{1}{sequence!infinite}{sequence-infinite}%
Let's define infinite
sequences so $s[i]$ is also the $i$\tth\ element of an infinite
sequence $s$.  This means that an infinite sequence should be a
function whose domain is the set of positive integers---a set we can
write $Nat :\: \{0\}$.  Therefore, we define the set $ISeq(S)$ of
all infinite sequences of elements in a set $S$ by
 \[ ISeq(S) == [Nat :\: \{0\} -> S]
 \]
We can then define the operators $IHead$ and $ITail$, the $head$
and $tail$ operators for infinite sequences, by
 \[ \begin{noj3}
    IHead(iseq) & \deq & iseq[1]  \V{.3}
    ITail(iseq) & \deq & [i \in (Nat :\: \{0\}) |-> iseq[i+1]]
    \end{noj3}
 \]
Compare these definitions with the definitions of $Head$ and $Tail$ in
\popref{Sequences}{the Sequences module}.  The definition of $IHead$
is identical to that of $Head$, but it makes the specification a
little easier to understand if we write $Head(s)$ when $s$ is a finite
sequence and $IHead(s)$ when it is an infinite sequence.

Let's now use TLC to check that we haven't made any errors.  Using
this \popref{BoundedChannel-ascii}{\textsc{ascii} version} of the
specification, open the spec in the Toolbox and run the PlusCal
translator on it.  To run TLC, we have to create a model.  This
requires specifying values for the constants $N$, $Msg$, and $Input$.
This is easy for $N$ and $Msg$; let $N$ equal a small integer (say 4),
and let $Msg$ equal some small set of \popref{model-value}{model
values} (say $\{m1, m2, m3\}$).  But what value should we choose for
$Input$, which must be an infinite sequence of messages.  There are infinitely
many choices---for example, $<<m1, m2, m1, m2, \ldots>>$, which can be
written:
\begin{twocols}
\begin{notla}
[i \in Nat \ {0} |-> 
        IF i % 2 = 1 THEN m1 ELSE m2]
\end{notla}
\begin{tlatex}
\@x{ [ i \.{\in} Nat \.{\,\backslash\,} \{ 0 \} \.{\mapsto}}%
\@x{\@s{16.86} {\IF} i \,\.{\%}\, 2 \.{=} 1 \.{\THEN} m1 \.{\ELSE} m2 ]}%
\end{tlatex}
\midcol
\begin{verbatim}
[i \in Nat \ {0} |-> 
     IF i % 2 = 1 THEN m1 ELSE m2]
\end{verbatim}
\end{twocols}
However, you should by now have enough of a feeling for how TLC works
to realize that it's unlikely to be able to handle a spec in which the
value of a variable is an infinite sequence.  Give it try and see
what error TLC produces.

To let TLC model check the spec, we create a model that substitutes
finite objects for infinite sequences.  The obvious approach is to
substitute finite sequences for infinite ones.  We do this by
\popref{definition-override}{overriding the definitions} of $ISeq$ and
$ITail$ by $Seq$ and $Tail$, respectively.  (There's no need to
override the definition of $IHead$ because it's equivalent to the
definition of $Head$.)  You can then let the model assign to $Input$
any short finite sequence of messages.  Do that and run TLC on the
model.  This should produce an error message that ends approximately
as follows:
\begin{display} \small\tt
The error occurred when TLC was evaluating the nested\\
expressions at the following positions:\\
0. \underline{Line 41, column 12 to line 69, column 22 in BoundedChannel}\\
1. \underline{Line 42, column 12 to line 70, column 38 in BoundedChannel}\\
2. \underline{Line 42, column 18 to line 70, column 38 in BoundedChannel}\\
3. \underline{Line 42, column 29 to line 70, column 37 in BoundedChannel}\\
4. \underline{Line 8, column 16 to line 8, column 22 in BoundedChannel}
\end{display}
You can probably figure out why the error happened by reading the
beginning of the message.  But let's suppose you can't.  Click on the
last line (numbered 4) in the message.  It highlights and jumps to the
expression $iseq[1]$ in the definition of $IHead$.  This tells you
that the error occurred when evaluating $IHead(iseq)$ for some
expression $iseq$.  Clicking on the preceding line (numbered 3).
Shows you that this evaluation occurred when TLC was evaluating the
$Send$ action, and $iseq$ equaled $in$.  (The definition of $Send$ is
part of the \tlaplus\ translation of the PlusCal code.  If you hold
the \textsf{Control} key down when clicking on line 3, it will take
you to the occurrence of that expression in the PlusCal code.)  TLC
evaluates $Send$ when trying to find a possible next state.  The error
occurred when TLC was doing this for the last state in the
error-trace.  The value of $in$ in that state is the empty sequence
$<<\,>>$.  The error occurred because TLC was evaluating
$Head(<<\,>>)$, which it obviously doesn't know how to do since
\tlaplus\ doesn't specify what that value is.

Examining the error trace, we see that the error occurred because the
sender had already sent all the messages in $Input$---something that
could not happen if $Input$ were an infinite sequence, like it's
supposed to be.  Since we want to find all the errors we can, we want
to prevent TLC from being stopped by this error.  To do that, we tell
TLC not to look for any successor states to a state with $in$ equal to
$<<\,>>$.  As we've seen before, we do this by adding the
\textsf{State Constraint} $in # <<\,>>$ on the model's
\textsf{Advanced Options} page.  TLC should now report no errors.

\subsubsection{Safety}

We regard module $BoundedChannel$ as the specification of the bounded
channel.  A specification is essentially a definition, and we cannot
prove the correctness of a definition.  However, we can check that a
specification means what we think it does by checking that it
satisfies properties we expect it to satisfy.  The first property
we should  usually check is type correctness.  The type invariant 
for the $BoundedChannel$ spec is:
\begin{twocols}
\begin{notla}
TypeOK == /\ in \in ISeq(Msg)
          /\ out \in Seq(Msg)
          /\ ch \in Seq(Msg)
\end{notla}
\begin{tlatex}
\@x{ TypeOK \.{\defeq} \.{\land} in \.{\in} ISeq ( Msg )}%
\@x{\@s{56.14} \.{\land} out \.{\in} Seq ( Msg )}%
\@x{\@s{56.14} \.{\land} ch \.{\in} Seq ( Msg )}%
\end{tlatex}
\midcol
\begin{verbatim}
TypeOK == /\ in \in ISeq(Msg)
          /\ out \in Seq(Msg)
          /\ ch \in Seq(Msg)
\end{verbatim}
\end{twocols}
Add that definition to the module and have TLC check that $TypeOK$
is an invariant of the spec.

The interesting safety property we want to check is that the receiver
receives the correct messages.  This means that the sequence $out$
of received messages is an initial part of the infinite sequence
$Input$.  This requirement is expressed by the invariance of
the following state predicate:
 \[ CorrectReceipt == \A i \in 1..Len(out) : out[i] = Input[i] \]
Another invariance property we want is that there are always at most
$N$ messages that have been sent but not received.  This invariant
and the invariance of $CorrectReceipt$ are implied by the invariance
of the following assertion:
  \[ \begin{conj}
     Len(inv) \leq N \\
     \mbox{$Init$ equals the concatenation of $out$, $ch$, and $in$} 
     \end{conj}
  \]
We can't write the second conjunct mathematically yet because $in$ is
an infinite sequence and our concatenation operator $\o$ is defined
only for finite sequences.  The only kind of concatenation that makes
sense for infinite sequences is the concatenation of a finite sequence
and an infinite one.  We define the operator \,$**$\, as follows so
\,$seq ** iseq$\, is the concatenation of the finite sequence $seq$ and the
infinite sequence $iseq$.  (Compare this with the definition of \,$\o$\,
in \popref{Sequences}{the Sequences module}.)
\begin{display}
\begin{notla}
seq ** iseq == [i \in (Nat \ {0}) |-> 
                  IF i =< Len(seq) THEN seq[i]
                                   ELSE iseq[i - Len(seq)]]
\end{notla}
\begin{tlatex}
 \@x{ seq \,\.{\stst}\, iseq \.{\defeq} [ i \.{\in} ( Nat \.{\,\backslash\,} \{ 0
 \} ) \.{\mapsto}}%
\@x{\@s{72.92} {\IF} i \.{\leq} Len ( seq ) \.{\THEN} seq [ i ]}%
\@x{\@s{140.68} \.{\ELSE} iseq [ i \.{-} Len ( seq ) ] ]}%
\end{tlatex}
\end{display}
Using \,$**$\, to express the invariant stated informally above, and combining
it with type correctness, we obtain the following invariant:
\begin{display}
\begin{notla}
Inv == /\ TypeOK
       /\ Len(ch) =< N
       /\ Input = (out \o ch) ** in
\end{notla}
\begin{tlatex}
\@x{ Inv \.{\defeq} \.{\land} TypeOK}%
\@x{\@s{34.04} \.{\land}  Len ( ch ) \.{\leq} N }%
\@x{\@s{34.04} \.{\land} Input \.{=} ( out \.{\circ} ch ) \.{\stst} in}%
\end{tlatex}
\end{display}
Add \popref{BoundedChannel-ascii2}{the \textsc{ascii} version}
of the definitions of \,$**$\, and $Inv$ to module $BoundedChannel$
and have TLC check that $Inv$ is an invariant.

\subsubsection{Liveness} \xlabel{bchan-liveness}

The natural liveness requirement on the channel is that any message
that is sent should be received.  We do not require that any message
is actually sent.  This requirement is expressed in \tlaplus\ by
 \rref{main}{main:weak-fairness}{weak fairness} of the receiver's action---the
$Rcv$ action defined by the algorithm's \tlaplus\ translation.  It is
specified in PlusCal by adding the keyword \textbf{fair} before the
receiver's \textbf{process} declaration.  Add it and run the
translator.  This adds the conjunct $\WF_{vars}(Rcv)$ to the
specification $Spec$.

Let's check that this fairness condition really does imply that every
message that's sent eventually gets received.  The invariant implies
only messages that are sent are received, and that they are received
in the correct order.  This implies that to ensure that sent messages
are received, we need only ensure that if messages have been sent,
then some messages are received.  More precisely, it suffices to show
that for every message in $ch$, another message is eventually added to $out$.
This is expressed in temporal logic by requiring that if there are ever
$i$ messages in $ch$ and $j$ messages in $out$, then eventually there
are $i+j$ messages in $out$:
 \begin{display}
  \mbox{}\ascii{channel-liveness-ascii}%
    $Liveness == 
      \begin{noj}
      \A i \in Nat, \; j \in 1\dd N : \\ \s{1}
          (Len(out) = i) /\ (Len(ch) = j) ~> (Len(out) = i+j)
      \end{noj}
 $
 \end{display}
Of course, to get TLC to check this property, you will have to use a
model that overrides the definition of
$Nat$.
%
\begin{aquestion}{lifo-queue-answer}
(a)~How would you rewrite the PlusCal specification of the bounded
channel to turn it into a bounded \emph{stack}, in which the receiver
always receives the most recently sent message?  

(b)~Explain why fairness of the $Rcv$ process in that specification
does not imply that every message sent is eventually received.
\end{aquestion}


\subsubsection{Implementing The Bounded Channel}\xlabel{impl-bchan}

The variables $in$ and $out$ are not meant to be implemented in a real
system.  Real systems don't maintain an infinite sequence of inputs to
be sent, and they usually don't record the entire sequence of messages
that are received.  What I'm interested in implementing are the steps
of adding a message to the end of $ch$ and removing it from the head
of $ch$.  I want to implement these operations in terms of lower-level
operations---ones that are closer to the primitive operations
performed by computers.  I am therefore looking for an algorithm that
uses the same variables $in$ and $out$, but refines the variable $ch$.
More precisely, I want an algorithm that implements algorithm $BChan$
under a refinement mapping that is the identity on $in$ and $out$, meaning
that $\ov{in}=in$ and $\ov{out}=out$.

Another way of saying this is that I want $in$ and $out$ to be the
  \tindex{1}{observable variable}%
  \ctindex{1}{variable!observable}{variable-observable}%
``observable'' variables whose behavior must be preserved.  The
variable $ch$ is an ``internal'' variable whose only function is to
help describe the behavior of $in$ and $out$.  An implementation 
is free to use other internal variables, but must maintain the same
behavior of $in$ and $out$.


% \subsubsection{A Philosophically Correct Specification}
% 
% Our specification of the bounded channel is the formula that mentions
% the variable $ch$ representing the sequence of messages that have been
% sent but not yet received.  Philosophically inclined computer
% scientists might object that Our specification should describe only
% the sending and receipt of messages, which are observable as changes
% to the variables $in$ and $out$.  


\subsection{The Bounded Buffer}

We next give a ``lower-level'' PlusCal implementation of the bounded
channel.  But first, we need a brief mathematical digression.

%% The following commands are for drawing pictures of the bounded buffer.
%% They are for placement in a picture environment, with the bounded buffer 
%%  circle will be centered at (0,0)
%%
%% \cptr{angle}, \pptr{angle}
%%   Draw the c and p pointer at the indicated angle (in degrees)
%%  
%% \cpt(x,y), \ppt(x,y)
%%   Puts the $c$ and $p$ at the indicated coordinates
%%
%% \cptN(x,y), \pptN(x,y)
%%   Like \cpt, and \ppt, but puts the c % N and p % N at the indicated 
%%   coordinates
%%
%%  \bbuf
%%    Draws the buffer.
%%
%%  \kbuf
%%     Like \bbuf, except uses $K$ instead of $N$.
%%
%%  \gpp
%%     Draws graph paper
\newcommand{\cptr}[1]{\put(0,0){\rotatebox{-#1}{\begin{picture}(0,0)
\put(0,25){\vector(0,1){20}} 
%\put(0,20){\makebox(0,0)[t]{\normalsize $c$}}         
\end{picture}}}}
\newcommand{\pptr}[1]{\put(0,0){\rotatebox{-#1}{\begin{picture}(0,0)
\put(0,85){\vector(0,-1){20}}        
\end{picture}}}}
\def\cpt(#1,#2){\put(#1,#2){\makebox(0,0){$c$}}}
\def\ppt(#1,#2){\put(#1,#2){\makebox(0,0){$p$}}}
\def\cptN(#1,#2){\put(#1,#2){\makebox(0,0){$c\,\%\,N$}}}
\def\pptN(#1,#2){\put(#1,#2){\makebox(0,0){$p\,\%\,N$}}}
\newcommand{\gpp}{{\gray \graphpaper(-100,-100)(200,200)}}
\newcommand{\bbuf}{\qbezier(0,50)(20.7,50)(35.35,35.35)
\qbezier(50,0)(50,20.7)(35.35,35.35)
\qbezier(0,-50)(20.7,-50)(35.35,-35.35)
\qbezier(50,0)(50,-20.7)(35.35,-35.35)
\qbezier(0,-50)(-20.7,-50)(-35.35,-35.35)
\qbezier(-50,0)(-50,-20.7)(-35.35,-35.35)
\qbezier(0,50)(-20.7,50)(-35.35,35.35)
\qbezier(-50,0)(-50,20.7)(-35.35,35.35)
\put(-46,19){\circle*{3}}
\put(-57,22.2){\makebox(0,0){\small $N\!-\!$3}}
\put(-35.35,35.35){\circle*{3}}
\put(-47,41){\makebox(0,0){\small $N\!-\!2$}}
\put(-19,46){\circle*{3}}
\put(-24,53){\makebox(0,0){\small $N\!-\!1$}}
\put(0,50){\circle*{3}}
\put(0,58){\makebox(0,0){\small 0}}
\put(19,46){\circle*{3}}
\put(22.2,53.6){\makebox(0,0){\small 1}}
\put(35.35,35.35){\circle*{3}}
\put(41,41){\makebox(0,0){\small 2}}
\put(46,19){\circle*{3}}
\put(53.6,22.2){\makebox(0,0){\small 3}}
\put(50,0){\circle*{3}}
\put(46,-19){\circle*{3}}
\put(35.35,-35.35){\circle*{3}}
\put(19,-46){\circle*{3}}
\put(0,-50){\circle*{3}}
\put(-19,-46){\circle*{3}}
\put(-35.35,-35.35){\circle*{3}}
\put(-46,-19){\circle*{3}}
\put(-50,0){\circle*{3}}
}%
\newcommand{\kbuf}{\qbezier(0,50)(20.7,50)(35.35,35.35)
\qbezier(50,0)(50,20.7)(35.35,35.35)
\qbezier(0,-50)(20.7,-50)(35.35,-35.35)
\qbezier(50,0)(50,-20.7)(35.35,-35.35)
\qbezier(0,-50)(-20.7,-50)(-35.35,-35.35)
\qbezier(-50,0)(-50,-20.7)(-35.35,-35.35)
\qbezier(0,50)(-20.7,50)(-35.35,35.35)
\qbezier(-50,0)(-50,20.7)(-35.35,35.35)
\put(-46,19){\circle*{3}}
\put(-57,22.2){\makebox(0,0){\small $K\!-\!$3}}
\put(-35.35,35.35){\circle*{3}}
\put(-47,41){\makebox(0,0){\small $K\!-\!2$}}
\put(-19,46){\circle*{3}}
\put(-24,53){\makebox(0,0){\small $K\!-\!1$}}
\put(0,50){\circle*{3}}
\put(0,58){\makebox(0,0){\small 0}}
\put(19,46){\circle*{3}}
\put(22.2,53.6){\makebox(0,0){\small 1}}
\put(35.35,35.35){\circle*{3}}
\put(41,41){\makebox(0,0){\small 2}}
\put(46,19){\circle*{3}}
\put(53.6,22.2){\makebox(0,0){\small 3}}
\put(50,0){\circle*{3}}
\put(46,-19){\circle*{3}}
\put(35.35,-35.35){\circle*{3}}
\put(19,-46){\circle*{3}}
\put(0,-50){\circle*{3}}
\put(-19,-46){\circle*{3}}
\put(-35.35,-35.35){\circle*{3}}
\put(-46,-19){\circle*{3}}
\put(-50,0){\circle*{3}}
}

\subsubsection{Modular Arithmetic} \xlabel{modular-arithmetic}
The 
  \tindex{1}{modular arithmetic}%
  \tindex{1}{arithmetic, modular}%
$Integers$ module defines the \emph{modulus} 
  \tindex{4}{modulus operator}%
operator 
  \ctindex{3}{+5w@\mmath{\%} (modulus)}{+5w}%
\,$\%$\, so that
$a\,\%\, b$ is the remainder when $a$ is divided by $b$.  More precisely,
for any integers $a$ and $b$ with $b$ positive, $a\,\%\, b$ is
the unique number satisfying the two conditions:
 \[ a\,\%\, b \,\in\, 0\dd (b-1) \s{2}
    \E\,q \in Int : a\, = \, b*q \, + \,  a\,\%\, b
 \]
\newcommand{\mmp}[1]{\ensuremath{+_{\s{-.2}\raisebox{-.1em}{\mbox{$_{#1}$}}}}}%
\newcommand{\mmm}[1]{\ensuremath{-_{\s{-.2}\raisebox{-.1em}{\mbox{$_{#1}$}}}}}%
\newcommand{\mplus}{\mmp{K}}%
\newcommand{\mminus}{\mmm{K}}%
For any positive integer $K$, let us define the operators \mplus\ 
and \mminus\ by
\begin{display}
$a \mplus b == (a + b) \,\%\, K$\V{.3}
$a \mminus b == (a - b) \,\%\, K$
\end{display}
%
The symbols \mplus\ and \mminus\ can't be written in \tlaplus, but it's
convenient to use them here anyway.  We are interested in these two
operators when applied to numbers in the set \,$0\dd (K-1)$\,.  To
understand their meaning, we write this set of numbers in a circle, as
shown \popref{modular-arithmetic-fig-1}{in this picture}.

If $a$ and $b$ are in \,$0\dd (K-1)$\,, then \,$a \mplus b$\, is the number
obtained by starting at $a$ and moving clockwise $b$ numbers.  For
example, we see from the picture that \,$(K-2) \mplus 5$\, equals~3.
We can characterize \,$a \mminus b$\, as the distance from $b$ to 
$a$ going counterclockwise around the circle.  For example, 
\,$3\mminus(K-2)$\, equals~5.

If you have studied group theory, you may recognize $0\dd (K-1)$ as
the Abelian (commutative) group known to mathematicians as $Z_{K}$,
where \mplus\ and \mminus\ are its addition and subtraction operators.
This means that, when applied to elements of $0\dd (K-1)$, the
operators \mplus\ and \mminus\ obey most of the same rules of
arithmetic that $+$ and $-$ do on the set $Int$ of integers.
For example, if $a$, $b$, and $c$ are in $0\dd (K-1)$, then:
 \[ a \mplus (b \mminus c) \;=\; (a \mminus c) \mplus b
 \]

\subsubsection{The Algorithm} \xlabel{main:bbuf-alg}

Our \emph{bounded buffer} algorithm implements the bounded channel by
implementing the sequence $ch$ of messages with a function (array)
$buf$.  Each message in $ch$ is contained in some element $buf[i]$ of
$buf$.  Since $ch$ can contain up to $N$ messages, $buf$ must contain
at least $N$ elements.  We let it be a function with domain $0\dd
(N-1)$.  (In programming terms, $buf$ is an $N$-element array indexed
by $0\dd (N-1)$.)  
   
The value of $buf$ will be a function from $0\dd (N-1)$ to the set
$Msg$ of messages.  This means that it will be a function with domain
$0\dd (N-1)$ such that $buf[i]\in Msg$ for all $i$ in its domain.
The set of all such functions is written in \tlaplus\ as
  \ctindex{1}{+4mf@\mmath{[S\rightarrow T]} (set of functions)}{+4mf}%
%  \ctindex{1}{+2r@\mmath{\rightarrow} (set of functions)}{+2r}%
$[0\dd (N-1) -> Msg]$.  Thus, our bounded buffer algorithm will 
satisfy the type invariant
 \[ buf \in [0\dd(N-1) -> Msg] \]
In addition to $buf$, our algorithm uses two variables $p$ and $c$
whose values are ``pointers'' to elements in $0\dd(N-1)$.  The value
of $c$ points to the buffer element that contains (or will contain)
the next message to be received; the value of $p$ points to the buffer
element into which the next message sent will be put.


\newcommand{\nplus}{\ensuremath{+_{\s{-.2}\raisebox{-.1em}{\mbox{$_{N}$}}}}}%
\newcommand{\nminus}{\ensuremath{-_{\s{-.2}\raisebox{-.1em}{\mbox{$_{N}$}}}}}%


As explained in 
    \lref{\xlink{modular-arithmetic}}{Section~\xref{modular-arithmetic} above}%
, we think of the elements of the domain $0\dd(N-1)$ of $buf$ as being
arranged in a ring.  The sequence of messages that have been sent but
not yet received is the sequence of elements in the buffer starting
from one pointed to by $c$ and, moving clockwise, ending with the
element right before the one pointed to by $p$.  
\popref{modular-arithmetic-fig-2}{In this picture},
the sequence of messages equals
%
 \[ << buf[N-2],\; buf[N-1],\; buf[0],\; buf[1],\; buf[2]>> \]
%
Observe that the length of this sequence is 5, which equals
$3\nminus (N-2)$, where \nminus\ is defined in 
   \lref{\xlink{modular-arithmetic}}{Section~\xref{modular-arithmetic}}.  
As this example illustrates, in general the length of the sequence of messages
is $p\nminus c$.

However, this can't be correct.  The value of $p\nminus c$ is an
integer from 0 through $N-1$, but the bounded channel can contain
sequences of messages of length $N$.  The problem is that if $c$
points to the buffer element containing the next message to be
received and $p$ points to the element into which the next message
sent is to be put, then $p$ equals $c$ both when the channel is empty
(equals the empty sequence) and when it is full (it is a sequence of
$N$ messages).  We must find a way to disambiguate these two cases.
%

One solution is to use an $N+1$ element buffer, with one buffer
element always unused.  The channel is then empty when $p$ and $c$
point to the same buffer element; it is full when $p$ points to the
element just before the one pointed to by $c$.

Instead, we use what I find to be a more elegant solution.  We let $p$
and $c$ be elements of $0\dd (2N-1)$, and we let $p\,\%\,N$ and
$c\,\%\,N$ be the buffer pointers---as shown 
\popref{modular-arithmetic-fig-3}{in this picture}.
The length of the sequence of messages is then equal to
$p\mmm{2N}c$.  The buffer is empty when $p$ equals $c$ and is full
when $p$ equals $c \mmp{2N}\!N$.  In general, the sequence of
messages is
 \[ <<\,buf[c\,\%\,N],\; buf[(c\mmp{2N}1)\,\%\,N],\; \ldots\,, \;
       buf[(p\mmm{2N}1)\,\%\,N]\,>>
 \]
The bounded buffer algorithm works because of the following property
of numbers:
\begin{enumerate}
\item[BB.] For any $N\in Nat:\:\{0\}$, $c \in 0\dd(2N-1)$,
and $j\in 0\dd N$, the $j$ numbers $c\%N$, $(c\mmp{2N}1)\%N$, \ldots, 
$(c\mmp{2N} (j-1))\%N$
are all distinct.
\end{enumerate}
%
Property BB is true with $2N$ replaced by $kN$ for any integer
$k>1$, so we could use $kN$ instead of $2N$ in the algorithm.  For
simplicity, we use $2N$.

We can now write our algorithm.  Like the bounded channel algorithm,
the bounded buffer algorithm will have a variable $in$ containing the
infinite sequence of messages yet to be sent on the channel and a
variable $out$ containing the (finite) sequence of messages that have
been received from the channel.  We will need the same definitions of
$ISeq$, $ITail$, $IHead$, and \,$**$\, as in the bounded channel
specification.  We could just copy and paste them into the bounded
buffer spec, but it's a little nicer to use a separate module that's
imported into each specification.  Create a new module $ISequences$
using \popref{ISequences-ascii}{this \textsc{ascii} text}.  Delete the
definitions of those four operators from module $BoundedChannel$ 
and add $ISequences$ to that module's \textsc{extends} statement.

Now create a new spec with root module $BoundedBuffer$.  The module
begins just like module $BoundedChannel$.
%
%
%
%
\begin{twocols}
\begin{notla}
EXTENDS Integers, Sequences, ISequences
CONSTANT N, Msg, Input
ASSUME /\ N \in Nat \ {0}
       /\ Input \in ISeq(Msg)
\end{notla}
\begin{tlatex}
\@x{ {\EXTENDS} Integers ,\, Sequences ,\, ISequences}%
\@x{ {\CONSTANT} N ,\, Msg ,\, Input}%
\@x{ {\ASSUME} \.{\land} N \.{\in} Nat \.{\,\backslash\,} \{ 0 \}}%
\@x{\@s{38.24} \.{\land} Input \.{\in} ISeq ( Msg )}%
\end{tlatex}
\midcol
%\begin{verbatim*}
\verb*|EXTENDS Integers, Sequences|\V{.2}
\verb*|CONSTANT N, Msg, Input|\V{.2}
\verb*|ASSUME /\ N \in Nat \ {0}|\V{.2}
\verb*|       /\ Input \in ISeq(Msg)|
%\end{verbatim*}
\end{twocols}
The module next defines $\oplus$ and $\ominus$ (typed \verb|(+)| and
\verb|(-)|) to be the operators that we have been calling $\mmp{2N}$
and~$\mmm{2N}$.
\begin{twocols}
\begin{notla}
a (+) b == (a + b) % 2*N
a (-) b == (a - b) % 2*N
\end{notla}
\begin{tlatex}
\@x{ a \.{\oplus} b \.{\defeq} ( a \.{+} b ) \,\.{\%}\, 2 \.{*} N\vs{.2}}%
\@x{ a \.{\ominus} b \.{\defeq} ( a \.{-} b ) \,\.{\%}\, 2 \.{*} N}%
\end{tlatex}
\midcol
\verb*|a (+) b == (a + b) % 2*N|\V{.2}
\verb*|a (-) b == (a - b) % 2*N|
\end{twocols}
We now come to the algorithm, which we name $BBuf$.  In this type of
bounded buffer algorithm, it is customary to call the two processes
the \emph{producer} and \emph{consumer}, rather than the \emph{sender}
and \emph{receiver}.  We therefore name the processes $Producer$ and
$Consumer$, giving them the identifiers $"P"$ and $"C"$, respectively.
  \popref{pcal-bbuffer}{Click here to see the algorithm's code.}

The \variables\ statement declares the same variables $in$ and $out$
as in the bounded channel spec, plus the three variables $buf$, $p$, and $c$,
along with their initial values.  We let $buf$ initially equal an
arbitrary function from $0\dd(N-1)$ to $Msg$.  Since we want the
sequence of messages in the channel to be initially empty, we must let
$p$ and $c$ both initially equal the same element of $0\dd(N-1)$.  For
simplicity, we let them both equal~$0$.
%
\begin{aquestion}{bbuf-answer-1}
How would you write the declarations of $p$ and $c$ so they
both initially equal the same arbitrary element of $0\dd(N-1)$?
\end{aquestion}
As in the bounded channel's PlusCal code, each
process executes a \,\pwhile~(\TRUE)\, loop whose body is a single atomic
action.  I used the labels $p1$ and $c1$ because later we will add labels $p2$,
$p3$, $c2$, and $c3$.
  \marginpar{\popref{renaming-note}{Note}}%
You should have no trouble understanding these processes by comparing
them with the processes of the bounded channel algorithm in
 \lref{\xlink{sec:bded-channel}}{Section~\xref{sec:bded-channel}}.
As in the bounded channel, we require that sent messages are
eventually received by making the $Consumer$ a \textbf{fair} process.

Here is the complete \popref{PCalBoundedBuffer}{\textsc{ascii}
version} of the $BoundedBuffer$ module.  Use it to complete the module
in the Toolbox, and run the translator.

To check that we haven't made any simple mistakes, we should check
that the spec is type correct---i.e., that is satisfies a
type-correctness invariant.  Here is a suitable invariant:
\begin{twocols}
\begin{notla}
TypeOK == /\ in  \in ISeq(Msg)
          /\ out \in Seq(Msg)
          /\ buf \in [0..(N-1) -> Msg]
          /\ p \in 0..(2*N-1)
          /\ c \in 0..(2*N-1)
\end{notla}
\begin{tlatex}
\@x{ TypeOK \.{\defeq} \.{\land} in\@s{5.69} \.{\in} ISeq ( Msg )}%
\@x{\@s{56.14} \.{\land} out\@s{0.40} \.{\in} Seq ( Msg )}%
 \@x{\@s{56.14} \.{\land} buf \.{\in} [ 0 \.{\dotdot} ( N \.{-} 1 )
 \.{\rightarrow} Msg ]}%
\@x{\@s{56.14} \.{\land} p \.{\in} 0 \.{\dotdot} ( 2 \.{*} N \.{-} 1 )}%
 \@x{\@s{56.14} \.{\land} c\@s{0.57} \.{\in} 0 \.{\dotdot} ( 2 \.{*} N \.{-} 1
 )}%
\end{tlatex}
\midcol
\begin{verbatim}
TypeOK == /\ in \in ISeq(Msg)
          /\ out \in Seq(Msg)
          /\ buf \in [0..(N-1) -> Msg]
          /\ p \in 0..(2*N-1)
          /\ c \in 0..(2*N-1)
\end{verbatim}
\end{twocols}
Use TLC to check that $TypeOK$ is an invariant of the spec.  As with
the bounded channel spec, you will have to use a model that overrides
the definitions of $ISeq$ and $ITail$ and that uses a state constraint
to prevent TLC from reporting an error after all the elements of
$Input$ have been sent.


\subsection{The~Bounded~Buffer~Implements~the~Bounded~Channel\protect\hspace*{-10em}}

%try
\subsubsection{The Refinement Mapping} \xlabel{refinement-mapping}

\begin{sloppypar}
We now show that the $BoundedBuffer$ specification implements the
$BoundedChannel$ specification under a suitable refinement mapping.
Refinement mappings and implementation  were explained in 
  \rref{main}{\xlink{sec:refinement}}{Section~\xref{sec:refinement}}
and
\rref{main}{\xlink{main:tl-refinement}}{Section~\xref{main:tl-refinement}}.
You may want to review those sections now.
\end{sloppypar}

A refinement mapping from $BoundedBuffer$ to $BoundedChannel$ consists
of definitions of state functions \ov{in}, \ov{out}, and \ov{ch} in
terms of the variables of $BoundedBuffer$.  Recall that for any
formula $F$ of $BoundedChannel$, we define \ovs{F} to be the formula
obtained from $F$ by substituting the expressions \ov{in}, \ov{out},
and \ov{ch} for $in$, $out$, and $ch$, respectively.
(The variables of \ovs{F} are variables of $BoundedBuffer$.) 

Let $Spec_{C}$ be formula $Spec$ of module $BoundedChannel$ and let
$Spec_{B}$ be formula $Spec$ of module $BoundedBuffer$, so $Spec_{C}$
is the specification of the bounded channel and $Spec_{B}$ the
specification of the bounded buffer.  We say that $Spec_{B}$
implements $Spec_{C}$ under the refinement mapping iff the following
condition is satisfied: For every behavior $s_{1}->s_{2}->\cdots$
satisfying formula $Spec_{B}$, the state sequence
$\ov{s_{1}}->\ov{s_{2}}->\cdots$ is a behavior satisfying formula
$Spec_{C}$, where each $\ov{s_{i}}$ is the state that assigns to the
variables $in$, $out$, and $ch$ of $BoundedChannel$ the values of the
state functions \ov{in}, \ov{out}, and \ov{ch}, respectively, in the
state $s_{i}$.%
 \marginpar{\popref{overbar}{A more precise definition of $\ov{s_{i}}$\,.}}
This condition is equivalent to the assertion that $Spec_{B} =>
\ov{Spec_{C}}$ is a theorem---that is, a formula that is true for all
behaviors.

As explained in \lref{\xlink{impl-bchan}}{Section~\xref{impl-bchan}},
we want the refinement mapping to be the identity on $in$ and $out$,
so $\ov{in}=in$ and $\ov{out}=out$.  This means that the
behavior $s_{1}->s_{2}->\cdots$ of $BoundedBuffer$ and the
corresponding behavior $\ov{s_{1}}->\ov{s_{2}}->\cdots$ have the same
values of $in$ and $out$, so they represent the same sending and
receipt of messages.  We consider $in$ and $out$ to be the only
observable variables, and if we look only at the observable variables
$in$ and $out$, then $s_{1}->s_{2}->\cdots$ and
$\ov{s_{1}}->\ov{s_{2}}->\cdots$ are the same behavior (where two
behaviors that differ only in stuttering steps are considered to be
the same).  Let $VSpec_{C}$ be specification $Spec_{C}$ with the
internal variable $ch$ \popref{variable-hiding}{hidden}.  Then
$Spec_{B}$ implements $Spec_{C}$ under the refinement mapping iff
every behavior that satisfies $Spec_{B}$ also satisfes
$VSpec_{C}$---in other words, iff $Spec_{B}=>VSpec_{C}$ is a theorem.
We write $VSpec_{C}$ informally as \,$\EE ch:Spec_{C}$.

The interesting part of the refinement mapping is the definition of
\ov{ch}.  Recall that the sequence of messages in the channel $ch$ is
represented by the sequence of elements\target{main-ovch}
 \[ <<\,buf[c\,\%\,N],\; buf[(c\oplus1)\,\%\,N],\; \ldots\,, \;
       buf[(p\ominus1)\,\%\,N]\,>>
 \]
We define \ov{ch} to equal this sequence of messages.  For example,
\popref{modular-arithmetic-fig-3}{in this picture}, \ov{ch} equals
%
 \[ <<\, buf[N-2],\; buf[N-1],\; buf[0],\; buf[1],\; buf[2]\,>> \]
%
To define \ov{ch} precisely, recall that the number of messages
in the buffer is $p\ominus c$.  From this and the fact that the
first message in the buffer (if there is one) is $buf[c\,\%\,N]$,
the definition is straightforward.  Since \ov{ch} isn't a \tlaplus\
identifier, we call it $chBar$:
\begin{twocols}[.4]
\begin{notla}
chBar  ==  [i \in 1..(p (-) c)  |-> 
            buf[(c (+) (i - 1)) % N]]
\end{notla}
\begin{tlatex}
 \@x{ chBar\@s{4.1} \.{\defeq}\@s{4.1} [ i \.{\in} 1 \.{\dotdot} ( p
 \.{\ominus} c )\@s{4.1} \.{\mapsto}}%
\@x{\@s{67.02} buf [ ( c \.{\oplus} ( i \.{-} 1 ) ) \.{\%} N ] ]}%
\end{tlatex}
\midcol
\begin{verbatim}
chBar  ==  [i \in 1..(p (-) c)  |-> 
              buf[(c (+) (i - 1)) % N]]
\end{verbatim}
\end{twocols}
Add this definition to module $BoundedBuffer$.  To check it, create an
error trace by having TLC check an incorrect invariant---for example,
$Len(out)#4$.  Run the Trace Explorer (\popref{trace-explorer}{as you
did before}), using it to display the value of $chBar$ in each state
of the trace.  

\begin{sloppypar}
The following statement imports module $BoundedChannel$ into module
$BoundedBuffer$ so that $C!Spec$ equals \ovs{Spec_{C}}:
\end{sloppypar}
\begin{widedisplay}
$C == \INSTANCE BoundedChannel \WITH 
      \begin{noj}
       ch <- chBar,\; in <- in,\; out <- out,\; \\ N <- N,\; Msg <- Msg,\; Input <- Input
            \end{noj}$
\end{widedisplay}
\tlaplus\ allows us to omit any substitution of the form $id <- id$
from the \textsc{with} clause, so we can write this statement as%
\ascii[-1.85]{ascii-instance-boundedchannel}
\begin{widedisplay}
$C == \INSTANCE BoundedChannel 
      \WITH ch <- chBar$
\end{widedisplay}
\begin{sloppypar}
In fact we could have used the identifier $ch$ instead of $chBar$ in
module $BoundedBuffer$ and eliminated the entire \textsc{with} clause.
\end{sloppypar}

Add the \textsc{instance} statement to module $BoundedBuffer$.  You
can now have TLC check that $Spec_{B}=>\ov{Spec_{C}}$ is a theorem by
having it check the property $C!Spec$.  (Add $C!Spec$ to the
\textsf{Properities} subsection of the \textsf{What to check?} part of
the Model Overview page.)  If you followed the instructions in
\lref{\xlink{bchan-liveness}}{Section~\xref{bchan-liveness}} and added
a fairness condition to the bounded channel spec, then TLC should report
the error
\begin{display}
\tt Temporal properties were violated.
\end{display}
Since we haven't yet added any fairness condition to the bounded
buffer algorithm, $Spec_{B}$ is satisfied by behaviors
$s_{1}->s_{2}->\cdots$ for which $\ov{s_{1}}->\ov{s_{2}}->\cdots$
doesn't satisfy the weak fairness property of $Spec_{C}$.  If you
remove that fairness condition (by deleting the \textbf{fair} keyword
and running the translator), TLC should find no error.


%try

\newcommand{\ovsig}{\ensuremath{\ov{\sigma}}}


\subsubsection{Showing Implementation} \xlabel{main:bbuf-impl-bchan}

Since TLC finds no counterexample, we can try to prove
$Spec_{B}=>\ov{Spec_{C}}$.  Let's drop the subscripts and write
our proof as it would appear inside module $BoundedBuffer$.
Remember that $C!Id$ means $\ov{Id}$ for any identifier $Id$
defined in $BoundedChannel$.  Any other identifier has the meaning
it has in $BoundedBuffer$.  Thus, we have to prove
$Spec => C!Spec$.
We saw in 
  \rref{main}{\xlink{main:tl-refinement}}{Section~\xref{main:tl-refinement}}
that to prove $Spec=>C!Spec$, we have to prove two things:
\begin{enumerate}
\item[R1.] $Init=>C!Init$

\item[R2.] $Inv /\ Inv' /\ Next => [C!Next]_{C!vars}$
\end{enumerate}
for some invariant $Inv$ of the bounded buffer.  Let's start with R1.

Looking at the translations of the two PlusCal algorithms, and
remembering that $\ov{ch}= chBar$, $\ov{in}=in$ and $\ov{out}=out$, we
see that:
%try
\begin{twocols}[.45]
\s{2}$
Init = \begin{conj}
         in = Input
         \\ out = << >>
         \\ buf \in [0\dd(N-1) -> Msg]
         \\ p = 0
         \\ c = 0
         \end{conj}
$
\midcol
$
C!Init = \begin{conj}
         in = Input
         \\ out = << >>
         \\ \ensuremath{chBar} = << >>
         \end{conj}
$
\end{twocols}  
%try
Obviously, $Init$ implies the first two conjuncts of
$C!Init$.  To see that it also implies $\ensuremath{chBar}=<<>>$,
% remember that if we picture the elements $buf[0]$, $buf[1]$,
% \ldots\,, $buf[2N-1]$ arranged in a circle, then 
% the $\ensuremath{chBar}$ is the sequence of elements starting from 
% $buf[c\%N]$ and going clockwise around the circle up to but
% excluding $buf[p\%N]$---for example, the sequence
%  \[ << buf[N-2],\; buf[N-1],\; buf[0],\; buf[1],\; buf[2]>> \]
% \popref{modular-arithmetic-fig-3}{in this picture}.  
recall that \ensuremath{chBar} is the sequence
  \[ <<\,buf[c\,\%\,N],\; buf[(c\oplus1)\,\%\,N],\; \ldots\,, \;
       buf[(p\ominus1)\,\%\,N]\,>>
 \]
of length $p\ominus c$.  Since $p=c$ implies $p\ominus c = 0$,
$Init$ implies $\ensuremath{chBar}=<<>>$, proving R1.  (A rigorous proof uses
the third conjunct of $Init$, which implies that $buf$
is a function with domain $0\dd(N-1)$.)

Let's now prove R2.  We expect that $Inv$ should imply
$TypeOK$.  We have defined \ensuremath{chBar} to be a sequence of length
$p\ominus c$.  Since $Spec$ implies that $ch$ is always a sequence
of length at most $N$, to prove $Spec$ we must be able to prove
that $p\ominus c$ is at most $N$.  Hence $Inv$ must imply 
$p\ominus c\leq N$.  It turns out that this is the only additional
property we need to prove R2, so we can define:
 \[ Inv == TypeOK\, /\ \, (p\ominus c\leq N)\]
Note that by definition of $\ominus$ and $TypeOK$, this implies
$p\ominus c \in 0\dd N$.

From the specifications, we see that
 \[\begin{noj3}
    C!Next &\;=\;&C!Send\, \/ \, C!Rcv \V{.4}
    Next &\;=\;& Producer \, \/ \, Consumer
  \end{noj3}\]
We expect a $Producer$ step of the bounded buffer to implement a
$Send$ step of the bounded channel, and a $Consumer$ step of
the bounded buffer to implement a $Rcv$ step of the bounded
channel.  To prove R2, we therefore prove
\begin{enumerate}
\item $Inv /\ Inv' /\ Producer \implies C!Send$

\item $Inv /\ Inv' /\ Consumer \implies C!Rcv$
\end{enumerate}
% 
% \step{1}{}
% 
% \vspace{.5\baselineskip}%
% \step{2}{}
% 
% \vspace{.5\baselineskip}%
% \qedstep
% \vspace{.2\baselineskip}%
% \begin{proof}
% \pf\ By \stepref{1}, \stepref{2}, and the definitions of $Next$
% and $Next$.
% \end{proof}
% \end{proof}
% \end{display}
\popref{bbuf-r2}{Here is a partial proof of R2} containing
the proof of property~$1$.  It uses these definitions:
  \[\begin{noj3}
    C!Send & \;\deq\; &
  \begin{conj}
  Len(\ensuremath{chBar}) # N \\
   \ensuremath{chBar}' = Append(\ensuremath{chBar}, IHead(in)) \\
    in' = ITail (in) \\
    out' = out\vs{.3}
   \end{conj}\\
 Producer & \;\deq\; &
    \begin{conj}
    p \ominus c # N \\
   buf' = [buf \EXCEPT ![p \% N] = IHead(in)] \\
   in' = ITail (in) \\
    p' = p \oplus 1 \\
   \UNCHANGED << out, c >>
    \end{conj}
    \end{noj3}\]
The proof of property~2 is left as an exercise, as is the proof of
invariance of $Inv$.
\begin{question}
Complete the proof of R2 and show that $Inv$ is an 
inductive invariant of $Spec$.
\end{question}



\subsubsection{Liveness} 

Our liveness requirement for the bounded channel is weak fairness of
the receiver's action.  The corresponding requirement for the bounded
buffer is weak fairness of the consumer's action, which we assert by
adding the keyword \textbf{fair} before the producer's
\textbf{process} declaration.  Do that and rerun the translator.  The
specification $Spec$ now becomes
 \[ Init \, /\ \, [][Next]_{vars} \, /\ \, \WF_{vars}(Consumer)
 \]
%
We expect that the fairness requirement of the bounded buffer should
implement the fairness requirement of the bounded channel, under the
refinement mapping we have been using.  More precisely let's once
again add to the specification $Spec$ of module $BoundedChannel$ the
fairness conjunct $\WF_{vars}(Rcv)$ (by putting \textbf{fair} before
its \textbf{process} declaration and running the translator).  We
expect $Spec=>C!Spec$ to still be a theorem.  Use TLC to check that it
is.  We now prove that it's a theorem.

The fairness condition of the bounded channel spec gives $C!Spec$ the
conjunct%
  \marginpar{Any symbol appearing under a bar comes
             from module $BoundedChannel$.}
$\ov{\WF_{vars}(Rcv)}$, the formula obtained from
$\WF_{vars}(Rcv)$ by substituting $chBar$ for $ch$.  We can't write
this formula in \tlaplus.  \popref{wfbar}{It does not equal
$\WF_{\ov{vars}}(\ov{Rcv})$}, which we can write as the \tlaplus\
formula $\WF_{C!vars}(C!Rcv)$.  We know that
$\ov{\WF_{vars}(Rcv)}$ equals
  \[ []<>\,~\ov{\ENABLED <<Rcv>>_{vars}} \;\/\; []<><<C!Rcv>>_{C!vars}
 \]
but we can't write $\ov{\ENABLED <<Rcv>>_{vars}}$ in \tlaplus.  Even
though we can't write this formula in \tlaplus, it is mathematically
well defined and we can use it in our informal proof.

We've already proved the
safety part of $Spec=>C!Spec$---namely, the formula:
 \[ Init /\ [][Next]_{vars} \;=>\; \ov{Init_{C} /\ [][Next_{C}]_{vars_{C}}}
 \]
We therefore just have to prove 
 $Spec=>\ov{\WF_{vars_{C}}(Rcv_{C})}$.  
Before we do this, you should read (or re-read)
  \rref{math}{\xlink{proving-fairness}}{Section~\xref{proving-fairness}}
on proving liveness properties.

In proving the safety part, we showed that a consumer step implements
a receiver step---that is, we proved that $Consumer$ implies $C!Rcv$.
This suggests that we should be able to use the simplest proof
rule from Section~\xref{proving-fairness}:
 \[ \tlrule{
      <<A>>_{v} /\ \overline{\strut\ENABLED <<B>>_{w}}
          \;=>\; <<\overline{B}>>_{\overline{w}} \V{.45}
      \overline{\strut\ENABLED <<B>>_{w}} \;=>\; \ENABLED <<A>>_{v}
     }
    {\rule{0pt}{1.35em}\WF_{v}(A) \;=>\;\overline{\WF_{w}(B)}}     
 \] 
with the substitutions:
 \[ A <- Consumer \s{2} v <- vars \s{2} B <- Rcv_{C} \s{2} w <- vars_{C}
 \]
Actually, we can't expect to prove either of the hypotheses without an
invariant, so we extend the proof rule to make use of an invariant $I$
of the bounded buffer spec:
 \[ \mbox{WF2s.}\ \ \tlrule{
     I /\ I' /\ <<A>>_{v} /\ \overline{\strut\ENABLED <<B>>_{w}}
     \;=>\; <<\overline{B}>>_{\overline{w}} \V{.45}
      I /\ \overline{\strut\ENABLED <<B>>_{w}} \;=>\; \ENABLED <<A>>_{v}
     }
    {\rule{0pt}{1.35em}[]I /\ \WF_{v}(A) \;=>\;\overline{\WF_{w}(B)}}     
 \] 
We will determine below what invariant to substitute for $I$.
\begin{aquestion}{wf2s}
Derive rule WF2s from \rref{math}{rule-wf2a}{rule WF2a}.
\end{aquestion}
Proving the safety part required proving
 $Inv /\ Inv' /\ Consumer => C!Rcv$.
Since a $Consumer$ step modifies $c$ and $out$, it's easy to prove
 \[ TypeOK => (Consumer => (vars' # vars)) \]
Hence, $Inv /\ Inv'$  (which implies $TypeOK$) implies 
  $Consumer \equiv <<Consumer>>_{vars}$.
Thus, the first hypothesis of WF2s follows from what we have already
proved if $I$ implies $Inv$.  (We don't need the
$\overline{\strut\ENABLED <<B>>_{w}}$ on the left of the implication
to prove the first hypothesis.)

When we turn to the second hypothesis of WF2s, we face a problem:
It requires reasoning about the formula 
  $\ov{\ENABLED <<Rcv_{C}>>_{vars_{C}}}$
that we can't even write in \tlaplus.  It's actually easy to write this
formula in \tlaplus; we just add the definition
  \[ RcvEnabled == \ENABLED <<Rcv>>_{vars}\]
to module $BoundedChannel$, so $\ov{\ENABLED <<Rcv>>_{vars}}$ equals
$C!RcvEnabled$.  This doesn't help because we can't expand
the definition of $C!RcvEnabled$ as a \tlaplus\ formula, but it
suggests the following approach: We
define $RcvEnabled$ to be a formula that's equivalent to
$\ENABLED<<Rcv>>_{vars}$ such that $C!RcvEnabled$ can be written in
\tlaplus.  More precisely, we prove (in module $BoundedChannel$) that
$RcvEnabled$ is equivalent to $\ENABLED<<Rcv>>_{vars}$.  The obvious
definition is
  \[ RcvEnabled == Len(ch) # 0
  \]
In the context of module $BoundedChannel$, we must prove:
 \[ \THEOREM RcvEnabledThm ==
      TypeOK => (RcvEnabled \equiv \ENABLED<<Rcv>>_{vars})\s{-10}\]
(Here, $TypeOK$ is the formula of that name defined in
$BoundedChannel$.)  Since substituting state functions for
variables (and constant expressions for constants) in a 
valid formula produces a valid formula, $C!RcvEnabledThm$ is a valid
theorem.  It asserts:
   \[ C!TypeOK => (C!RcvEnabled \equiv \ov{\ENABLED<<Rcv>>_{vars}})
   \]
Thus, if $I$ implies $C!TypeOK$, then (after expanding the definition
of $C!RcvEnabled$) the second hypothesis of WF2s becomes 
 \[ I /\ (Len(chBar) # 0) => \ENABLED <<Consumer>>_{vars}
 \]
There was no need to define $RcvEnabled$.  We could simply replace
it with its definition, $Len(ch)#0$, in $RcvEnabledThm$.


Let $I$ equal $Inv /\ C!TypeOK$.  We have reduced the proof of
 $Spec => \ov{\WF_{vars_{C}}(Rcv_{C})}$ 
to proving three things:
\begin{enumerate}
\item Theorem $RcvEnabledThm$.

\item $Inv /\ (Len(chBar) # 0) => \ENABLED <<Consumer>>_{vars}$

\item $Spec => [](Inv /\ C!TypeOK)$.
\end{enumerate}
\begin{sloppypar}
The proofs of 1 and 2 use 
 \rref{math}{enabled-rules}{rules E1--E7} of Section~\xref{sec-enabled}.
For 1, observe that $TypeOK$ (of module $BoundedChannel$) implies that
a $Rcv$ action changes $ch$ and $out$, so $<<Rcv>>_{vars}$ 
is equivalent to $Rcv$ and E7 implies 
  $\ENABLED<<Rcv>>_{vars}\equiv \ENABLED Rcv$.
We then use E1, E4, and E5 to show 
  $\ENABLED Rcv \equiv Len(ch)#0$, 
proving~1.  The proof of~2 is similar (except in the context
of module $BoundedBuffer$).
\end{sloppypar}

To prove 3, first observe that in proving safety, we proved
$Spec => []Inv$.  Hence, we just have to prove $Spec => []C!TypeOK$.
In proving safety, we also proved
  \[ Spec => C!Init /\ [][C!Next]_{C!vars}
  \]
Hence we just have to prove
  \[ C!Init /\ [][C!Next]_{C!vars} => C!TypeOK\]
Since substitution (barring) preserves truth of a formula, it suffices to
prove the following theorem in module $BoundedChannel$:
  \[ Init /\ [][Next]_{vars} => TypeOK
  \]
This is a straightforward invariance proof.





\subsection{A Finer-Grained Bounded Buffer} 

We have written the bounded buffer algorithm so each of its steps
implements one step of the bounded channel.  Thus, in one step, the
producer (1)~evaluates the test $p\ominus c # N$, (2)~assigns a value
to $buf[p\,\*\%\,N]$, and (3)~increments $p$ modulo $2N$.  
As explained in 
  \lref{\xlink{atom-grain}}{Section~\xref{atom-grain}},
such an algorithm is not considered to be a satisfactory
implementation because it doesn't satisfy the
\lref{single-access}{Single Access Rule}.

We get a finer-grained implementation of the bounded channel by adding
labels to the bounded buffer algorithm $BBuf$.  That algorithm's
shared variables are $buf$, $p$, and $c$.  (Variable $in$ is accessed
only by the producer; variable $out$ is accessed only by the
consumer.)  Moreover, $p$ is written only by the producer and $c$ is
written only by the consumer.  We get a finer-grained version that
satisfies the Single Access Rule by adding labels
\popref{pcal-fgbbuffer}{as shown here.}

\popref{PCalFGBoundedBuffer}{Here is the \textsc{ascii} text} of a new
module $FGBoundedBuffer$ that's the same as the beginning of the
$BoundedBuffer$ module, except with the additional labels in the
algorithm and the algorithm renamed $FGBBuf$.  Open it in the Toolbox
and run the translator.  Create the same kind of model for it that you
used for the original bounded buffer spec, and check that the algorithm
satisfies the same type invariant $TypeOK$.

The \tlaplus\ translation of $FGBuf$ introduces the additional
variable $pc$, which satisfies this type-correctness invariant, where
$\STRING$ is the set of all strings:
\begin{widedisplay}
\begin{twocols}[.35]
\begin{notla}
pc \in [{"P", "C"} -> STRING] 
\end{notla}
\begin{tlatex}
 \@x{ pc \.{\in} [ \{\@w{P} ,\,\@w{C} \} \.{\rightarrow} {\STRING}
 ]}%
\end{tlatex}
\midcol
\begin{verbatim}
pc \in [{"P", "C"} -> STRING]
\end{verbatim}
\end{twocols}
\end{widedisplay}
Add it as an additional conjunct to $TypeOK$.  We can make this condition
more precise by adding the following two conjuncts as well:
\begin{widedisplay}
\begin{twocols}[.35]
\begin{notla}
/\ pc["P"] \in {"p1", "p2", "p3"}
/\ pc["C"] \in {"c1", "c2", "c3"}
\end{notla}
\begin{tlatex}
\@x{ \.{\land} pc [\@w{P} ] \.{\in} \{\@w{p1} ,\,\@w{p2} ,\,\@w{p3} \}}%
\@x{ \.{\land} pc [\@w{C} ] \.{\in} \{\@w{c1} ,\,\@w{c2} ,\,\@w{c3} \}}%
\end{tlatex}
\midcol
\begin{verbatim}
/\ pc["P"] \in {"p1", "p2", "p3"}
/\ pc["C"] \in {"c1", "c2", "c3"}
\end{verbatim}
\end{twocols}
\end{widedisplay}
Have TLC check that the resulting formula $TypeOK$ is invariant of
$FGBBuf$.
%
\begin{aquestion}{fgbuf-refine}
We might expect algorithm $FGBBuf$ to implement the bounded channel
algorithm $BChan$ under the same refinement mapping as algorithm
$BBuf$.  Use TLC to see why it doesn't.
\end{aquestion}
%
Instead of showing directly that $FGBBuf$ implements $BChan$, we show
that it implements $BBuf$ under a refinement mapping
\[ 
   buf <- \ovr{buf}\s{2} p <- \ovr{p} \s{2} c <- \ovr{c}\s{2}
   in <- \ovr{in}\s{2} out <- \ovr{out} 
\]
where we use {\red red} overbars to distinguish this refinement mapping
from the refinement mapping
 \[ch <- \ov{ch}\s{2} in <- \ov{in}\s{2} out <- \ov{out}\]
under which $BBuf$ implements $BChan$.  We know that $BBuf$ implements
$BChan$ under the ``black'' refinement mapping.  If $FGBuf$ implements
$BBuf$ under the ``red'' refinment mapping, then we can conclude that
$FGBuf$ implements $BChan$ under refinement mapping
 \[ ch <- \ovr{\ov{ch}}\s{2} in <- \ovr{\ov{in}}\s{2} out <- \ovr{\ov{out}}
 \]
For any expression $e$ in the variables $ch$, $in$, and $out$ of $BChan$, 
the expression $\ovr{\ov{e}}$ is obtained as follows.
\begin{enumerate}
\item Perform the
black substitutions for the variables 
of $BChan$ to obtain
the expression \ov{e} in the variables $buf$, $p$, $c$, $in$, and $out$
of $BBuf$.

\item Perform the red substitutions for the variables 
of $BBuf$ 
to obtain \ovr{\ov{e}}, which is an expression
in the variables $buf$, $p$, $c$, $in$, $out$, and $pc$ of $FGBBuf$.
\end{enumerate}
%
As explained in \lref{\xlink{impl-bchan}}{Section~\xref{impl-bchan}},
we are letting both refinement mappings be the identity on $in$ and
$out$, so $\ovr{\ov{in}}=in$ and $\ovr{\ov{out}}=out$.

Since $\ovr{in}=in$, a $Producer$ step of $BBuf$ must be simulated by
a $p2$ step of $FGBuf$.  Therefore, a $p2$ step must increment \ovr{p}
and a $p1$ or $p3$ step must leave \ovr{p} unchanged.  This is accomplished
by letting
\begin{display}
\begin{notla}
p  ==  IF pc["P"] = "p3" THEN p (+) 1 ELSE p 
\end{notla}
\begin{tlatex}
 \@x{ \ovr{p}\@s{4.1} \.{\defeq}\@s{4.1} {\IF} pc [\@w{P} ] \.{=}\@w{p3} \.{\THEN} p
 \.{\oplus} 1 \.{\ELSE} p}%
\end{tlatex}
\end{display}
Similar reasoning leads to the analogous definition of \ovr{c}.
Therefore, add the following to module $FGBoundedBuffer$.
\begin{display}
\begin{notla}
pBar == IF pc["P"] = "p3" THEN p (+) 1 ELSE p 
cBar == IF pc["C"] = "c3" THEN c (+) 1 ELSE c
B == INSTANCE NewBoundedBuffer WITH p <- pBar, c <- cBar
\end{notla}
\begin{tlatex}
 \@x{ pBar \.{\defeq} {\IF} pc [\@w{P} ] \.{=}\@w{p3} \.{\THEN} p \.{\oplus} 1
 \.{\ELSE} p\vs{.4}}\ascii{pbar-cbar}%
 \@x{ cBar\@s{0.51} \.{\defeq} {\IF} pc [\@w{C} ] \.{=}\@w{c3}\@s{0.72}
 \.{\THEN} c\@s{0.57} \.{\oplus} 1 \.{\ELSE} c\vs{.4}}%
 \@x{ B \.{\defeq} {\INSTANCE} NewBoundedBuffer {\WITH} p \.{\leftarrow} pBar
 ,\, c \.{\leftarrow} cBar}%
\end{tlatex}
\end{display}
Let TLC check if $FGBBuf$ implements $BBuf$ under this refinement
mapping by having it check the temporal propertyh $B!Spec$.  TLC will
report that temporal properties are violated, which means that
$FGBBuf$ doesn't implement the fairness properties of $BBuf$ under
this refinement mapping.  The error trace is one in which the producer
executes actions $p1$ and $p2$, and then the execution halts (stutters
forever).  In this last state, $p=c=0$, so a consumer action is not
enabled.  The only enabled action is the producer's $p3$ action.
Since there is no fairness condition on the producer, that step need
not be taken, so the execution can halt.

We don't want to require that the producer keeps performing observable
steps---$p2$ steps that remove an element from $in$.  However, if it
does perform such a step, then it must complete the operation and
perform a $p3$ step.  Therefore, we want to require fairness of the
$p3$ action but not of the $p2$ action.  We express this in PlusCal
by making the producer a \textbf{fair} process, but change the $p2$
label to \verb|p2:-|\,.  Since a $p1$ step changes no variable except
$pc$, it doesn't matter whether we require fairness of $p1$ or
not require it by adding a \verb|-| after its label.  I find it more
natural not to require it.

Make the necessary change to the PlusCal code, rerun the translator,
and have TLC check that $FGBBuf$ now implements $BBuf$ under the
refinement mapping.  Check it without fairness of $p1$.  Since adding
fairness strengthens the spec, so $FGBBuf$ still satisfies any
properties that it did without fairness of $p1$, it will also
implement $BBuf$ with the fairness property.
%
\begin{question}
Write the refinement mapping under which $FGBBuf$ implements
the bounded channel specifiction $BChan$, and have TLC check that
it's correct.
\end{question}

\subsection{Further Refinement}

When the producer is at $p2$, it is about to access buffer element
$p\,\%\,N$.  When the consumer is at $c2$, it is about to access
buffer element $c\,\%\,N$.  The following state predicate asserts
that if both processes are about to access buffer elements, then
they are about to access different elements:
 \[ BufMutex == 
  (pc["P"]="p2") \, /\ \, (pc["C"]="c2") \;=>\; (p\,\%\,N # c\,\%\,N) \s{-10}
 \]
Have TLC check that $BufMutex$ is an invariant of algorithm
$FGBBuf$.  

Formula $BufMutex$ asserts a sort of mutual exclusion property.  We
can think of each of the two processes having $N$ separate critical
sections, numbered from 0 to $N-1$.  The producer is in its $i$\tth\
critical section when $pc["P"]$ equals $"p2"$ and $p\,\%\,N$ equals
$i$; and likewise, the consumer is in its $i$\tth\ critical section
when $pc["C"]$ equals $"c2"$ and $c\,\%\,N$ equals $i$.  The state
predicate $BufMutex$ asserts that the two processes cannot be in their
$i$\tth\ critical sections at the same time, for each $i$ in
$0\dd(N-1)$.  If we can consider $buf[i]$ and $buf[j]$ 
  \marginpar{\popref{separate-vars}{Are $buf[0]$ and $buf[1]$ separate
   variables?}}
to be separate
variables if $i#j$, then the discussion in
 \lref{\xlink{modern-mutex}}{Section~\xref{modern-mutex}} 
shows that we can implement statements $p2$ and $c2$ with non-atomic
actions.  

As a very simple example of refining the grain of atomicity of the
$p2$ and $c2$ steps, let's just refine $p2$ into two separate atomic
actions.  Create a new specification by copying the beginning of
module $FGBoundedBuffer$ through the algorithm declaration, and
changing the algorithm by replacing the two-line statement $p2$ with
\begin{display}
\begin{twocols}[.4]
\begin{nopcal}
p2a:-  buf[p % N] := IHead(in);
p2b:   in := ITail(in) ;
\end{nopcal}
\begin{tlatex}
 \@x{ p2a\@s{.5}\textrm{:-}\@s{3}\@s{4.1} buf [ p \.{\%} N ] \.{:=} IHead ( in
 ) {\p@semicolon}}%
 \@x{ p2b\@s{.5}\textrm{:}\@s{3}\@s{8.08} in \.{:=} ITail ( in )
 {\p@semicolon}}%
\end{tlatex}
\midcol
\begin{verbatim}
p2a:-  buf[p % N] := IHead(in);
p2b:   in := ITail(in) ;
\end{verbatim}
\end{twocols}
\end{display}
This algorithm implements $FGBBuf$ under a refinement mapping for
which \ov{buf} and \ov{out} are changed by $p2a$.  They are defined as
follows:
\begin{display}
\begin{nopcal}
in  ==  IF pc["P"] = "p2b" THEN ITail(in)
                           ELSE in
pc  ==  [i \in {"P", "C"} |->
            CASE i = "P" -> CASE pc["P"] = "p2a" -> "p2"
                              [] pc["P"] = "p2b" -> "p3"
                              [] OTHER -> pc["P"]
              [] i = "C" -> pc["C"]    ]
\end{nopcal}
\begin{tlatex}
 \@x{ \ov{in}\@s{4.40} \.{\defeq}\@s{4.1} {\IF} pc [\@w{P} ] \.{=}\@w{p2b}
 \.{\THEN} ITail ( in )}\ascii{in-pc}%
\@x{\@s{119.38} \.{\ELSE} in\vs{.3}}%
 \@x{ \ov{pc}\@s{4.10} \.{\defeq}\@s{4.10} [ i \.{\in} \{\@w{P} ,\,\@w{C} \}
 \.{\mapsto}}%
 \@x{\@s{47.81} {\CASE} i \.{=}\@w{P} \.{\rightarrow} {\CASE} pc [\@w{P} ]
 \.{=}\@w{p2a}\@s{0.36} \.{\rightarrow}\@w{p2}}%
 \@x{\@s{131.35} {\Box}\@s{10.30} pc [\@w{P} ] \.{=}\@w{p2b}
 \.{\rightarrow}\@w{p3}}%
\@x{\@s{131.35} {\Box}\@s{10.30} {\OTHER} \.{\rightarrow} pc [\@w{P} ]}%
 \@x{\@s{56.01} {\Box}\@s{10.30} i \.{=}\@w{C} \.{\rightarrow} pc [\@w{C}
 ]\@s{12.29} ]}%
\end{tlatex}
\end{display}
The refinement mapping is the identity on $out$, $buf$, $p$, and $c$.
Use TLC to check that the new algorithm implements $FGBBuf$ under this
refinement mapping.
%
\begin{aquestion}{xfgbuf-refine}
Why do we want a ``\verb|-|'' after the label $p2a$ but not after the
label $p2b$.
\end{aquestion}
%
This refinement mapping is not the identity on $in$.  The new
algorithm also refines $FGBBuf$ under a refinement mapping that is the
identity on $in$ (as well as $out$)---a mapping under which a $p2$
step of $FGBBuf$ is implemented by a $p2b$ step.  To define that
refinement mapping, we must add a history variable that records the
value of $buf[p\,\%\,N]$---the value that is overwritten by step
$p2a$.  History variables are explained in
\rref{topics}{\xlink{hide-variables}}{Section~\xref{hide-variables}}.
\begin{question}
Add the necessary history variable to the new algorithm and define the
refinement mapping that is the identity on $in$ and $out$ under which
the algorithm implements $FGBBuf$.
\end{question}
 

  \tindex{1}{process}%
  \vspace{-1.5\baselineskip}%
\subsection{What is a Process?}

It seems obvious that the bounded channel and the bounded buffer
are two-process systems.  It also seems obvious that sequential
systems like the one-bit clock and Euclid's algorithm have just a
single process.  What is obvious is not always true.

% \begin{tabbing}
% \algorithm\ $Clock$ \{ \V{.3} 
% \s{1}\variable\ $b \in \{\,\}$;\V{.3}
% \s{1}\process\ $(Tick = "tick")$\\
% \s{2}\{ \=$i$: \=\+\pwhile\ $(\TRUE)$\+\\
% \s{.5}\= \{ \= \await\ $b=0$ ; \\
% \>\>            $b := 1$\\
% \>        \} \-\-\\
% \s{2}\} \V{.5}
% \s{1}\process\ $(Tock = "tock")$\\
% \s{2}\{ \=
% $o$: \>\+ \pwhile\ $(\TRUE)$ \\
% \> \{ \> \await\ $b=1$ ; \\
% \>\>             $ := 0$\\
% \>        \}\-\\
% \s{2}\} \\
% \s{.5}\}
% \end{tabbing}
% \begin{twocols}
% \begin{tabbing}
% \algorithm\ $Clock$ \{ \V{.3} 
% \s{1}\variable\ $b \in \{\,\}$;\V{.3}
% \s{1}\process\ $(Tick = "tick")$\\
% \s{2}\{ \=$i$: \=\pwhile\ $(\TRUE)$ \= \{ \= \await\ $b=0$ ; \s{5}\\
%         \>      \>                  \>    \> $b := 1$\\
%         \>      \>                  \>  \} \\
% \s{2}\} \V{.5}
% \s{1}\process\ $(Tock = "tock")$\\
% \s{2}\{ \> $o$: \>\pwhile\ $(\TRUE)$ \> \{ \> \await\ $b=1$ ; \\
%         \>      \>                   \>    \>  $ b := 0$\\
%         \>      \>                   \>  \}\\
% \s{2}\} \\
% \s{.5}\}
% \end{tabbing}
% \midcol
% \begin{verbatim*}
% --algorithm Clock {
%   variable b \in {0, 1} ;
%   process (Tick = "tick") 
%     { i: while (TRUE) { await b = 0;
%                         b := 1;
%                       }
%     }
%   process (Tock = "tick") 
%     { o: while (TRUE) { await b = 1;
%                         b := 0;
%                       }
%     }
% }
% \end{verbatim*}
% \end{twocols}

Consider \popref{TwoProcessClock}{this PlusCal algorithm}.  
It is
a two-process algorithm whose basic structure is identical to that
of 
\popref{pcal-channel}{the bounded
       channel algorithm} (without fairness).
Algorithm $Clock$ describes a one-bit clock, the $Tick$ process waiting
until $b$ equals 0 and setting $b$ to 1, the $Tock$ process does the
inverse.  In the Toolbox, create a new specification containing this
algorithm (the module needs nothing else), and run the PlusCal
translator.  The translation defines the initial predicate $Init$ and
next-state action $Next$ by:
\begin{display}
\begin{tlatex}
\@x{ Init\@s{4.44} \.{\defeq} b \.{\in} \{ 0 ,\, 1 \}}%
\par\vspace{8.0pt}%
\@x{ Next\@s{0.32} \.{\defeq} Tick \.{\lor} Tock}%
\end{tlatex}
\end{display}
where $Tick$ and $Tock$ are defined by:
\begin{display}
\begin{tlatex}
\@x{ Tick\@s{0.76} \.{\defeq} \.{\land} b \.{=} 0}%
\@x{\@s{40.15} \.{\land} b \.{'} \.{=} 1}%
\par\vspace{8.0pt}%
\@x{ Tock \.{\defeq} \.{\land} b \.{=} 1}%
\@x{\@s{40.15} \.{\land} b \.{'} \.{=} 0}%
\end{tlatex}
\end{display}
These formulas $Init$ and $Next$ are equivalent to the formulas
   \rref{main}{init1-next1-clock}{$Init1$ and $Next1$} 
that were the initial predicate and next-state formulas of our first
specification of the one-bit clock.  In other words, the specification
defined by this two-process algorithm is the same as our original
specification of the one-bit clock.  This is the same one-bit clock
that we also specified in
   \rref{main}{\xlink{sec:pcal-clock}}{Section~\xref{sec:pcal-clock}}
as a one-process (sequential) PlusCal algorithm.  Expressing this more
mathematically, the specification $Spec$ defined by the translation of
the two-process one-bit clock algorithm is equivalent to the
specification $Spec$ defined by the translation of our original
PlusCal specification of the one-bit clock.

If we look at the \tlaplus\ specifications that represent what we
think of as describing two processes, we see that the next-state
action is the disjunction of two formulas, each describing the steps
taken by one of the processes.  In fact, one reasonable definition of
a process is a disjunct of the next-state action.  However, as we saw
in our several specifications of the one-bit clock, there can be many
different ways to write equivalent specifications.  Their next-state
actions need not have the same disjuncts---or even the same number of
disjuncts.

We usually view a concurrent system as a collection of processes, and
we tend to find that view so natural that we think that the process
structure is inherent in the system.  It isn't.  The decomposition of
a system into a particular collection of processes is just a way of
viewing the system; there are often other ways of viewing it.  For a
number of years, it seemed completely obvious that in a multi-computer
system, a process was something that was executed on a single
computer.  The invention of remote procedure calls made it clear that
one can also describe a multi-computer system with processes whose
execution moves from one computer to another.

Processes provide a way of viewing a system. They are not an innate
part of the system.
\begin{question}
Write a two-process PlusCal version of Euclid's algorithm whose translation
produces a specification equivalent to the one we wrote
in \rref{main}{\xlink{main:euclid-alg}}{Section~\xref{main:euclid-alg}}
in module $Euclid$.
\end{question}
%
We have been viewing the bounded buffer algorithm $BBuf$ and its
refinements as two-process algorithms.  However, they can also quite
naturally be viewed as $N$-process algorithms, the $i$\tth\ process
being responsible for reading and writing from buffer element
$buf[i]$, for each $i$ in $0\dd (N-1)$.  Here is
\popref{pcal-nproc-bbuf}{algorithm $NProcBBuf$}, an $N$-process
version of algorithm $BBuf$.  Compare it with
\popref{pcal-bbuffer}{algorithm $BBuf$}.  We show that if we ignore
the value of the variable $pc$ of algorithm $NProcBBuf$, the two
algorithms have the same behaviors.  (The \tlaplus\ translation of
$NProcBBuf$ has a variable $pc$, but the translation of $BBuf$ does
not.)  To state this more precisely, let $Spec_{2}$ be the \tlaplus\
formula $Spec$ in the translation of $BBuf$---the formula that is the
specification of algorithm $BBuf$.  Let $Spec_{N}$ be the
corresponding formula for algorithm $NProcBBuf$.  We show that
$Spec_{2}$ is equivalent to $\EE pc\midcolon Spec_{N}$, the formula
obtained by \rref{topics}{hiding-variables}{hiding the variable} $pc$
in $Spec_{N}$.

Here is \popref{PCalNProcBoundedBuffer}{the \textsc{ascii} text} of
the algorithm and its enclosing module.  First show that $NProcBBuf$
implements $BBuf$ under the 
  \tindex{1}{identity refinement mapping}%
  \ctindex{1}{refinement mapping!identity}{identity}%
identity refinement mapping---one that
defines $\ov{v}=v$ for every variable $v$ of $BBuf$.  This shows that
every behavior of $NProcBBuf$ is a behavior of $BBuf$, so 
 $\EE pc\midcolon Spec_{N}$ 
implies $Spec_{2}$.  We now want show that 
$Spec_{2}$ implies $\EE pc\midcolon Spec_{N}$.  For this, we must
show that $BBuf$ implements $NProcBBuf$ under a refinement mapping
that is the identity on all variables of $NProcBBuf$ except $pc$.
You can do this in:
\begin{aquestion}{nproc-bbuf-impl}
Find an invariant of algorithm $NProcBBuf$ of the form $pc = expr$
that expresses the value of $pc$ in terms of the values of the other
variables.  Use TLC to check that $BBuf$ implements $NProcBBuf$
under the refinement mapping with $\ov{pc}=expr$ that is the identity
on all other variables of $NProcBBuf$.
\end{aquestion}


\end{document}


XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

WHO KNOWS WHAT GARBAGE LURKS BELOW?

XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
\subsection{Choosing the Grain of Atomicity} 
\xlabel{main:grain-of-atomicity}

What is the right grain of atomicity for the bounded buffer algorithm?
Should we use the coarse-grained algorithm $BBuf$ of module
$BoundedBuffer$ or the finer-grained
  \popref{pcal-fgbbuffer}{algorithm $FGBBuf$}
of module $FGBoundedBuffer$?  Or should we use a still finer-grained
algorithm?

We are not interested in specifications for their own sake.  A
specification is interesting because it is an abstract description of
a concrete system.  That system might be a computer program or a
hardware component that we intend to build.  We want our specification
to be as simple as possible, and coarser specifications are simpler
than finer-grained ones.  However, we also want our specification to
be a sufficiently accurate representation of the system, and a
finer-grained specification more accurately describes the concrete
system.  Our specification should be fine enough to describe all the
aspects of the concrete system that are important to us, but no finer.

Before we can begin writing a specification of a system, we must
choose the variables that represent the system's state.  When doing
that, we also decide on approximately what the grain of atomicity
should be.  I chose integer-valued variables $p$ and $c$ because I
decided that reading or writing the value of each of those variables
would occur in a single 
  \sref{main}{main:atomic-action}{atomic action}.  
Had I wanted reading or writing a single bit of those values to be a
separate atomic action, I might have made them bit-valued
arrays---that is, I might have let their values be functions from a
set of bit locations to $\{0,\,1\}$.

When specifying a system, it's a good idea to start with the
coarsest-grained specification that makes sense.  There's no point
writing a more complicated, finer-grained specification if a
coarser-grained one will reveal errors.  The coarser-grained
specification is easier to write and faster to check with TLC\@.  It
is usually very easy to modify a PlusCal algorithm to make it
finer-grained: you just add more labels and perhaps add some
  \ctindex{9}{variable!process-local}{variable-process-local}%
  \ctindex{9}{process!variable local to}{process-variable-local}%
process-local variables.  For example, suppose we want to turn the
single atomic action
\begin{display}
$p3$: $p := p \oplus 1$
\end{display}
of $FGBBuf$ into three actions: the first reading the value of $p$,
the second applying the $\oplus 1$ operation, and the third assigning
the value to $p$.  We just replace this statement by
\begin{display}
\begin{tabbing}
$p3a$: \= \kill
$p3$: \> $t := p$ ; \target{p3a-p3c}\\*
$p3a$: \> $t := t\oplus1$ ;\\*
$p3b$: \> $p := t$
\end{tabbing}
\end{display}
where $t$ is a variable local to the process (not accessible by any other
process).  Process-local variables are declared right before the
process's code---in this case, as follows:
\begin{display}
\begin{tabbing}
\process\ $(Process = "P")$\\*
\s{1}\variable\ $t$ ;\\*
\s{1}\{ $p1$: \pwhile\ $(\TRUE)$ \ldots
\end{tabbing}
\end{display}
Let's call this new algorithm \MF.

Refining the grain of atomicity in a specification written directly in
\tlaplus\ is not as easy, but it is still easy enough.  The hard part
of writing a specification is understanding 
  \marginpop{understanding}{How do you know if you understand something?}%
what it should say.  Once you get used to the language, expressing it
in \tlaplus\ or PlusCal is straightforward.


Should we check the finer-grained bounded buffer algorithm \MF\
obtained by splitting the single atomic statement $p3$ into the three
separate statements $p3$, $p3a$, and $p3b$?  This algorithm is a more
accurate representation of an eventual implementation of the algorithm
by a multi-threaded program.  However, having checked the
coarser-grained algorithm $FGBBuf$, do we have to check \MF? The
answer is no, because correctness of $FGBBuf$ implies the correctness
of \MF. The following is a very informal proof of this claim;
don't take it too seriously.  The rigorous way to prove 
the claim is described in 
  \rref{topics}{\xlink{reduction-section}}{Section~\xref{reduction-section}}.

To understand the proof, recall that correctness of an algorithm means
that each of its behaviors is correct---that is, satisfies the
algorithm's correctness property.  For $FGBBuf$, the correctness
property is $C!Spec$ of module $FGBoundedBuffer$, which asserts of a
behavior $\tau$ that it is
  \lref{main-refinement}{mapped by the refinement mapping} 
$ch <- chBar$ to a behavior \ovs{\tau} that satisfies the bounded
channel specification.

\begin{proof}
\step{1}{Let \rd{\MF} be the algorithm obtained from \MF\ by combining the
three separate statements into the single statement:
\begin{display}
$\red p3$: $t := p$ ; $t := t\oplus1$ ; $p := t$%
\marginpar{I write the statement $\red p3$ of \rd{\MF} in red to distinguish it
from the statement $p3$ of \MF.}
\end{display}}

\vspace{.5\baselineskip}%

\step{2}{Correctness of algorithm $FGBBuf$ implies correctness
 of algorithm \rd{\MF}.}
\vspace{.2\baselineskip}%
\begin{proof}
\pf\ Algorithm \rd{\MF} is the same as except that it also specifies
the values of the variable $t$, so a behavior of \rd{\MF} is a
behavior of $FGBBuf$.  Hence, correctness of every behavior of
$FGBBuf$ implies correctness of every behavior of \rd{\MF}.
\end{proof}

\vspace{.5\baselineskip}%

\step{3}{Correctness of \rd{\MF} implies correctness of \MF.}
\vspace{.2\baselineskip}%
\begin{proof}
\step{3.1}{It suffices to assume $\sigma$ is a behavior of
\MF\ and show that there exists a behavior \rd{\sigma} of
\rd{\MF} such that correctness of \rd{\sigma} implies 
correctness of $\sigma$.}
\vspace{.2\baselineskip}%
\begin{proof}
\pf\ By definition of correctness of an algorithm.
\end{proof}
\vspace{.3\baselineskip}%

\step{3.2}{Define \rd{\sigma} to be obtained by executing the same sequence
of actions as in $\sigma$ except with each $p3$ and $p3a$ step replaced
by a stuttering step and each execution of $p3b$ replaced by an 
execution of $\red p3$.\marginpar{$\red p3$ is the action of \rd{\MF}
defined in \stepref{1}.}}
\vspace{.2\baselineskip}%
\begin{proof}
\pf\ Such a behavior \rd{\sigma} exists because the producer actions
$p3$ and $p3a$ of \MF\ write only the value of $t$, which is never
accessed by the consumer, and they read only the values of $t$ and
$p$, which are never written by the consumer.  Hence, these actions do
not interact with any consumer actions---that is, they neither affect
nor are affected by any consumer actions.  It is therefore possible to
defer executions of $p3$ and $p3a$ actions and combine them with the
execution of the next $p3b$ action.
\end{proof}

\vspace{.3\baselineskip}%

\step{3.3}{\rd{\sigma} is a behavior of \rd{\MF}}
\vspace{.2\baselineskip}%
\begin{proof}
\pf\ Each step of \rd{\sigma} either satisfies an action that is
the same in both \MF\ and \rd{\MF}, is a $\red p3$ step, or is a
stuttering step.
\end{proof}

\vspace{.3\baselineskip}%

\step{3.4}{$\ov{\rd{\sigma}}=\ov{\sigma}$, where \rd{\sigma} and
$\sigma$ are mapped to \ov{\rd{\sigma}} and \ov{\sigma}, respectively,
by the refinement mapping $ch<-chBar$.}
\vspace{.2\baselineskip}%
\begin{proof}
\pf\ The value of
$chBar$ depends only on the values of the variables $p$, $c$, and
$buf$.  The actions $p3$ and $p3a$ of \MF\ leave those variable
unchanged, and action $\red p3$ of \rd{\MF} changes them the same way
as the corresponding action $p3b$ of \MF\ does (incrementing $p$ and
leaving $c$ and $buf$ unchanged).  Therefore, in each state of $\sigma$,
the value of each of these three variables is the same as its value in the
corresponding state of \rd{\sigma}.  Hence, $\sigma$ and \rd{\sigma}
are mapped to the same behavior by the refinement mapping.
\end{proof}

\vspace{.3\baselineskip}%

\qedstep
\vspace{.2\baselineskip}%
\begin{proof}
\pf\ By \stepref{3.1}, \stepref{3.3}, and \stepref{3.4}, since correctness
of a behavior means that it is mapped by the refinement mapping 
$ch<-chBar$ to a behavior of the bounded channel.
\end{proof}
\end{proof}
\vspace{.5\baselineskip}%

\qedstep
\vspace{.2\baselineskip}%
\begin{proof}
By \stepref{2} and \stepref{3}.
\end{proof}
\end{proof}
%
\noindent 
%
This argument is quite informal.  Making it more rigorous requires
defining precisely what it means for two actions not to interact
with one another.  We could make a simple syntactic definition for
PlusCal algorithms in terms of the variables that appear in both
actions.  However, such a definition would be too strong.  For example,
it would assert that
\begin{display}
$a$: $x[i] := 1$ \ and \ $b$: $x[j] := 2$
\end{display}
interact because they both write the variable $x$.  However, these
actions do not really interact if $i$ is unequal to $j$.  A more
precise definition is: \marginpar{Remember that action $A$ is enabled
           in state $s$
           iff there is a state $t$ such that $s\rightarrow t$ is
           an $A$ step.}
\begin{display}
\textbf{Definition } Two actions 
  \tindex{1}{interact, do not}%
\emph{do not interact} iff
(i)~executing them in either order produces the same result and
(ii)~executing either of them cannot 
enable or disable the other.
\end{display}
%
The procedure of deducing properties of a finer-grained algorithm
from properties of a coarser-grained one is called 
  \tindex{1}{reduction}%
  \tindex{1}{reducing}%
\emph{reduction}.
We say that we obtain \rd{\MF} by \emph{reducing} \MF.

I now generalize the process of reduction from the bounded buffer
example to other PlusCal algorithms.  Let \MF\ be a multiprocess
PlusCal algorithm with a process $\Pi$ containing a sequence of
consecutive statements
\begin{display}
$r_{1}$: $R_{1}$ ; \ $r_{2}$: $R_{2}$ ; \ \ldots\,\  $r_{n}$: $R_{n}$
\end{display}
where each $R_{i}$ is a statement or sequence of statements with no
labels.  Define \rd{\MF} to be the PlusCal algorithm obtained from
\MF\ by replacing this sequence of statements with
\begin{display}
$\red r_{1}$: $R_{1}$ ; \ $R_{2}$ ; \ \ldots\,\ $R_{n}$
\end{display}
In the example above, $n$ equals 3, step $r_{1}$ is $p3$, step $r_{2}$
is $p3a$, and step $r_{3}$ is $p3b$.

Assume that \rd{\MF} is a legal PlusCal algorithm.  The PlusCal
language contains a 
      \ctindex{1}{goto (PlusCal statement)@\icmd{textbf}{goto} (PlusCal statement)}{goto}%
\textbf{goto} statement.  For \rd{\MF} to be a
PlusCal algorithm, \MF\ must contain no \textbf{goto}~$r_{i}$
statement for $i#1$.  Also, PlusCal requires a \textbf{while}
statement to be labeled, so no $R_{i}$ can contain a \pwhile---except
that $R_{1}$ can be a \pwhile\ statement.

To construct a mapping from behaviors of \MF\ to behaviors of
\rd{\MF}, we assume:
\begin{describe}{\textbf{Red1}}
\item[\textbf{Red1}] There is a $k$ in $1\dd n$ such that for each
$i#k$, action $r_{i}$ does not interact with any action of any process
other than $\Pi$.
\end{describe}
For each behavior $\sigma$ of \MF, we define a behavior \rd{\sigma} by
(a)~for each $i#k$, replacing every execution of $r_{i}$ in $\sigma$
with a stuttering step, and (b)~replacing every execution of $r_{k}$
by an execution of action $\red r_{1}$ of algorithm \rd{\MF}.
In our example, $k$ equals $3$, so $r_{k}$ is the action $p3b$.
The non-interactivity assumption of $p3$ and $p3a$ were necessary
but not sufficient to imply the existence of the behavior \rd{\sigma}
for any behavior $\sigma$.

However,
examining the proof reveals that this was true only because $k$
equaled $n$ in this example.  If $\sigma$ contains an execution in
which an $r_{k}$ is not followed by an execution of the following
action $r_{k+1}$, \ldots, $r_{n}$, then we need an additional
assumption to ensure that it is possible to replace the execution of
$r_{k}$ by an execution of $\red r_{1}$.  A sufficient assumption
is: 
\begin{describe}{\textbf{Red2}}
\item[\textbf{Red2}] For every $i$ in $(k+1)\dd n$, action $r_{i}$ is
enabled whenever control in process $\Pi$ is at $r_{i}$.
\end{describe}
To check condition Red2, note that a PlusCal action can be disabled
when control is at the action only if the action contains one of the
following two kinds of statements:
\begin{itemize}
\item \textbf{await}~$P$ \ \ with $P$ false

\item \textbf{with}~$(u\in S)$ \ \ with $S$ the empty set
\end{itemize}
Conditions Red1 and Red2 ensure that if $\sigma$ is any behavior
satisfying the safety property of \MF\ (its initial predicate and
next-state action) then \rd{\sigma} satisfies the safety property of
\rd{\MF}.  We must show that if $\sigma$ also satisfies the fairness
property of \MF, then \rd{\sigma} satisfies the fairness property of
\rd{\MF}.  But first, we must state what the fairness property of
\rd{\MF} is.

In
\sref{main}{\xlink{adding-fairness}}{Section~\xref{adding-fairness}},
we introduced the \textbf{fair~process} construct, which asserts weak
fairness of the process's next-state action.  As we saw in
\lref{\xlink{main:proc-wf}}{Question~\xref{main:proc-wf}}, weak
fairness of a process is equivalent to weak fairness of each of its
actions.  In PlusCal, it is possible to specify different fairness
conditions---weak fairness, \popref{strong-fairness}{strong fairness},
or no fairness---for different actions in a process.  To ensure that
\rd{\sigma} satisfies the fairness property of \rd{\MF} when $\sigma$
satisfies the fairness property of \MF, we require that all the
actions $r_{i}$ of \MF\ have the same fairness property, and that
action $\red r_{1}$ of \rd{\MF} has this fairness property.  Of
course, all the other actions of \rd{\MF} must have the same fairness
property as the corresponding actions of \MF.

Giving the actions of \rd{\MF} the same fairness properties as those
of \MF\ is not enough to ensure that \rd{\sigma} satisfies the
fairness properties of \rd{\MF} if $\sigma$ satisfies the fairness
properties of \MF. Consider a single-process PlusCal algorithm \MF\
satisfying weak fairness and containing the following statements,
where $t$ is a variable:
\begin{display}
$r_{1}$: \with\ $(u \in {1, 2})$ \{ $t := u$ \}; \V{.2}
$r_{2}$: \await\ $t = 2$
\end{display}
In the reduced algorithm \rd{\MF}, these two actions are replaced
by the single action:
\begin{display}
\begin{tabbing}
$\red r_{1}$: \= \with\  $(u \in {1, 2})$ \{ $t := u$ \}; \V{.2}
         \> \await\ $t = 2$
\end{tabbing}
\end{display}
The \tlaplus\ translation of this action is
 \[ {\red r_{1}} == \begin{conj}
                    pc  = "r_{1}" \\
                    \E u \in \{1,2\} : t' = u; \\
                    t' = 2 \\
                    pc' = \ldots
                    \end{conj}
 \]
The formula
 \[ \begin{conj}
    \E u \in \{1,2\} : t' = u; \\
                    t' = 2
    \end{conj}
 \]
is equivalent to $t'=2$, which shows that the statement $\red r_{1}$
is equivalent to the simple assignment ${\red r_{1}}\!\!\!: t := 2$.

Algorithm \MF\ allows a behavior $\sigma$ in which statement $r_{1}$
sets $t$ to $1$ and then halts.  This behavior satisfies weak fairness
of the actions, since it halts with $pc$ equal to $"r_{2}"$ and the
$r_{2}$ action not enabled.  However, the corresponding behavior
\rd{\sigma} halts with $pc$ equal to $"r_{1}"$ and the $r_{1}$ action
enabled, which does not satisfy weak fairness for \rd{\MF}.
To ensure that \rd{\sigma} satisfies the fairness condition of
\rd{\WF}, we need an additional condition.  The following one suffices.
\begin{describe}{\textbf{Red3}}
\item[\textbf{Red3}] For any state in which the atomic statement
\begin{display}
 $\red r_{1}$: $R_{1}$ ; \ $R_{2}$ ; \ \ldots\,\ $R_{k}$
\end{display}
is enabled, every execution of the sequence
\begin{display}
  $r_{1}$: $R_{1}$ ; \ $r_{2}$: $R_{2}$ ; \ \ldots\,\ $r_{k-1}$: $R_{k-1}$
\end{display}
of statements starting in that state leaves $r_{k}$:~$R_{k}$ enabled.
\end{describe}
Condition Red3 is vacuously true if $k=1$.

\medskip
We also want to ensure that correctness of \rd{\MF} implies
correctness of \MF. The generalization of the result for the bounded
buffer algorithm is straightforward.  Assume a refinement mapping
$x_{1}<-\ov{x_{1}}$, \ldots, $x_{m}<-\ov{x_{m}}$ under which the
behaviors $\sigma$ and \rd{\sigma} are mapped to \ovs{\sigma} and
\ov{\rd{\sigma}}, respectively.  The following additional condition
implies that $\ovs{\sigma}=\ov{\rd{\sigma}}$.
\begin{describe}{\textbf{Red4}}
\item[\textbf{Red4}] For each $i#k$ and each $j$, action $r_{i}$
leaves \ovs{x_{j}} unchanged.
\end{describe}
This condition implies that, if \rd{\MF} implements some specification
under this refinement mapping, then so does \MF. We saw in
   \sref{main}{main:invariance-as-refinement}{Question~\ref{invariance-as-refinement}}
that invariance is a special case of implementation under a refinement
mapping.  Thus, if each $r_{i}$ with $i#k$ leaves a predicate $Inv$
unchanged, then $Inv$ an invariant of \rd{\MF} implies that it is also
an invariant of \MF.  

I will restate these results as the following informal theorem.  The
theorem is informal mostly because our construction of \rd{\sigma}
from $\sigma$ is informal.  It involves replacing in $\sigma$
executions of one action by another, whereas a behavior consists of a
sequence of states, not executions.  
\begin{display}
\textbf{Simple PlusCal Reduction Theorem } Let \MF\ be a PlusCal algorithm
with a process $\Pi$  containing the consecutive statements
\begin{display}
$r_{1}$: $R_{1}$ ; \ $r_{2}$: $R_{2}$ ; \ \ldots\,\  $r_{n}$: $R_{n}$
\end{display}
where each $R_{i}$ has no labels, and assume that replacing these
statements with
\begin{display}
$\red r_{1}$: $R_{1}$ ; \ $R_{2}$ ; \ \ldots\,\ $R_{n}$
\end{display}
produces a legal PlusCal algorithm \rd{\MF}.  Assume all the actions
$r_{i}$ of \MF\ have the same fairness condition, and that each action
of \rd{\MF} has the same fairness condition as the corresponding
action of \MF, where action $\red r_{1}$ of \rd{\MF} has the
same fairness condition as the actions $r_{i}$ of \MF. If Red1--Red3
hold, then for every behavior $\sigma$ of \MF\ there is a
behavior \rd{\sigma} of \rd{\MF} that is obtained from $\sigma$ by
replacing each execution of $r_{i}$ by a stuttering step, for $i#k$,
and replacing each execution of $r_{k}$ by an execution of action
$\red r_{1}$ of \rd{\MF}.  Moreover, for any refinement mapping
$x_{1}<-\ov{x_{1}}$, \ldots, $x_{m}<-\ov{x_{m}}$, if Red4 holds, then
$\sigma$ and \rd{\sigma} are mapped to the same behavior under this
refinement mapping.
\end{display}
We use the reduction theorem to show that correctness of a
coarser-grained algorithm implies the correctness of a finer-grained
one.  We start with an algorithm \MG\ and split one of its
actions to obtain an algorithm \MF\ such that \MG\ equals \rd{\MF}.
We can continue this process by splitting another action in \MG\
that was copied intact into \MF, obtaining a finer-grained algorithm
$\mathcal{E}$ such that \MF\ equals \rd{\mathcal{E}}; and so on.

We can apply multiple reductions to a finer-grained bounded buffer
algorithm in which each of the five actions of
  \popref{pcal-fgbbuffer}{algorithm $FGBBuf$} 
are split.  It is not obvious how the atomic actions $p1$ and $c1$ can
be split into a sequence of statements.  To split them, 
we first rewrite $FGBBuf$ by
using \textbf{goto} statements to eliminate the \textbf{while} loops.
For example, the body of the consumer process can be written as follows:
\begin{display}
\begin{tabbing}
$c1$: \= \await\ $p # c$; \\
$c3$: \> $c := c \oplus 1$; \\
      \> \goto\ $c1$
\end{tabbing}
\end{display}
You should check that the rewritten algorithm has the same
\tlaplus\ translation as the original, so it is obviously the same
algorithm.  To split the \await\ statement, observe that it can be
rewritten as:
\begin{display}
$c1$: \pif\ $(p = c)$ \goto\ $c1$ 
\end{display}
Naively, this statement seems to be different from the original
\await\ statement because, when $p$ equals $c$, it performs ``busy
waiting'' steps instead of waiting.  However, those steps change none
of the algorithms variables, so they are just stuttering steps that
are also allowed by the algorithm with the \await\ statement.  (The
consumer can loop forever at $c1$ iff it can wait forever at the
\await\ statement in a behavior that is the same as the looping
behavior except for stuttering steps.)  Thus, we can split the
consumer process's body into finer-grained actions as follows, where
$u$ is a variable local to the consumer process:
\begin{display}
\begin{tabbing}
$c1a$: \= \kill
$c1$: \> $u := p$ ; \\
$c1a$: \> \pif\ $(u = c)$ \goto\ $c1$ ; \\
$c3$: \> $u := c$ ; \\
$c3a$:   \> $u := u \oplus 1$; \\
$c3b$:   \> $c := u$; \\
         \> \goto\ $c1$
\end{tabbing}
\end{display}
In the reduction that combines $c1$ and $c1a$ into a single action,
action $c1$ is the action $r_{k}$ of the reduction theorem (in other
words, $k$ equals~1).

The splitting of the consumer actions $p1$ and $p3$ are similar.  It
is not clear how to split the action $p2$ that assigns a value to
$buf[p\,\%\,N]$.  In an application, a message might be a complex data
structure, and assigning a value to $buf[p\,\%\,N]$ might consist of
multiple separate writes, the last one setting it to the desired
value.  Just to have a definite example, let's split the $p2$ action
into the following actions, where $t$ is the variable local to the
producer process that we introduced to split $p3$.
\begin{display}
\begin{tabbing}
$p2a$: \= \kill
$p2$: \> \with\ $(v \in Msg)$ \{ $t := v$ \} ; \\
$p2a$: \> $buf[p\,\%\,N] := 42$ ;\\
$p2b$: \> $buf[p\,\%\,N] := t$ 
\end{tabbing}
\end{display}
Each of these three actions does not interact with any consumer action.
In the reduction that combines these three actions into one, we can
let $r_{k}$ be any of the actions.  

Let \MF\ now be the algorithm obtained by splitting the five actions
of $FGBBuf$ in this way.  Five reductions lead from algorithm \MF\ to
an algorithm \MG\ that is the same as $FGBBuf$ except for the
introduction of the process-local variables $t$ and $u$.  These
reductions can be performed in any order, and they all satisfy
Red1--Red4.  The only one of these fifteen conditions that is not
obvious is Red4 for the reduction that ``reassembles'' the $p2$
action.  It is not immediately clear that the assignments to
$buf[p\,\%\,N]$ leave $chBar$ unchanged.  To see that they do, recall
that $chBar$ is defined to equal the sequence
    \[ <<\,buf[c\,\%\,N],\; buf[(c\oplus1)\,\%\,N],\; \ldots\,, \;
       buf[(p\ominus1)\,\%\,N]\,>>
 \]
The invariance of $PCInv$, which asserts
  $p\ominus c \in 0\dd N$,
implies that $p\,\%\,N$ is not one of the function arguments
$c\,\%\,N$, \ldots, $(p\ominus1)\,\%\,N$, so changing the value of
$buf[p\,\%\,N]$ does not change the value of $chBar$.

Since $FGBBuf$ implements the bounded channel under the refinement
mapping $ch<-chBar$, it is obvious that \MG\ does too.  Five
applications of the reduction theorem then show that \MF\ does as
well.  The reduction theorem therefore allows us to deduce the
correctness of the very fine grained algorithm \MG\ from the
correctness of $FGBBuf$.

\pause\noindent
%
In many real examples---perhaps most examples---Red4 does not hold,
and an algorithm \MF\ does not implement the desired specification
under the same refinement mapping as its reduced version \rd{\MF}.
However, Red1--Red3 imply that \MF\ implements the same
specification as \rd{\MF} under a different refinement mapping that is
related to the original one.  This is often good enough to imply
correctness of \MF.
  \rref{topics}{\xlink{reduction-section}}{Section~\xref{reduction-section}}
will explain this refinement mapping and show how to formalize
everything done here.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

How to get two processes with arbitrary numbers.

Define an i, j configuration to be one with 
  i < j
  num[p] = i, and p has read num[q] and num[r]
  num[q] = j, and q has read num[r]
  num[r] = 0, and r in nc section

How to get to a 1, j configuration, for any j:

  Have two processes alternate, reaching a position
  in which q is setting its number and has read num[r] = j-1.

  Have process p enter, and read all numbers = 0.

  q sets num[q] to j and reads num[r].
  p sets num[p] to 1 and reads num[q] and num[r]

How to go from an i, j configuration to an i+1, j+1 
configuration:

num[1] = 44, has read 2
2 in nc
num[3] = 22, has read {2, 1}

2 enters, reads num[3] = 22

3 exits, in nc

1 reads 3, enters & exits cs

3 enters, reads num[1] = 44

1 sets num[1] = 0 and goes to nc

2 reads num[1] = 0 , sets num[2]= 22+1

3 reads num[1], sets num[3] = 44+1

2 reads 1&3 
3 reads 1

------------------------------------------------------------

Let's return now to \popref{tla-pf-2}{our informal liveness proof} for
the 2-process 1-bit algorithm and formalize it.  The theorem asserts that
the algorithm satisfies formula $DeadlockFree$, a theorem that is written
formally as
 $Spec => DeadlockFree$,
where $Spec$ is the algorithm's specification.  Define
 \[ Fairness == \A self \in \{0,1\} : \WF_{vars}((pc[self] # "ncs") /\ P(self))
 \]
so $Spec$ equals 
 $ Init /\ [][Next]_{vars} /\ Fairness$.

The usual proof of an implication like $Spec => DeadlockFree$ is to
assume $Spec$ and prove $DeadlockFree$, starting the proof with the
step:
\begin{display}
\begin{proof}
\step{1}{\sassume{$Spec$}\sprove{$DeadlockFree$}}
\end{proof}
\end{display}
However, formula $Spec$ contains the conjunct $Init$, which is an
assertion about the initial state of a behavior.  Therefore, $Spec$ is
not a $[]$ formula; it can be true of a behavior $\sigma$ without
being true of all suffixes of $\sigma$.  As observed above, assumptions
in a temporal proof should be $[]$ formulas; so we should not use
this \textsc{assume}/\textsc{prove} in a proof.


XXXXXXXXXXXXXXXXXXXX


\bigskip
\noindent
The liveness properties we want to prove about a system are generally
$[]$ formulas like $F~>G$ (which is defined to equal $[](F => <>G)$),
asserting that something is true throughout its execution.  A system
satisfies such a property not because of what was true in its initial
state, but because of what is true in all of its reachable
states---that is, because it satisfies an invariant.

Proving that a system satisfies a property $F$ means proving 
  $Spec => F$,
where the specification $Spec$ equals
 $Init /\ [][Next]_{vars} /\ Fair$ 
for some fairness property $Fair$.  The formulas $[][Next]_{vars}$ and
$Fair$ are $[]$ formulas. However, the formula $Init$ is an
assertion about only the initial state.  It cannot be used directly to
reason about what is true throughout the behavior.

Here is a possible structure for the proof of $Spec => F$ for a $[]$
formula $F$, where $Inv$ is a suitable invariant.
\begin{display}
\pflongindent
\pflongnumbers
\beforePfSpace{0pt}
\afterPfSpace{0em}
\interStepSpace{.5em}
\begin{proof}
\step{1}{$Spec => []Inv$}
\step{2}{$[]Inv /\ [][Next]_{vars} /\ Fair => F$}
\qedstep
\begin{proof}
\pf\ By steps \stepref{1} and \stepref{2} and the definition of $Spec$.
\end{proof}
\end{proof}
\end{display}
A more convenient structure is often:
\begin{display}
\pflongindent
\pflongnumbers
\beforePfSpace{0pt}
\afterPfSpace{0em}
\interStepSpace{.5em}
\begin{proof}
\step{1}{$Spec => []Inv$}
\step{2}{\sassume{$[]Inv /\ [][Next]_{vars} /\ Fair$} \sprove{$F$}}
\begin{proof}
\pf\ By step \stepref{1} and the definition of $Spec$.
\end{proof}
\ldots
\end{proof}
\end{display}
The assumption of the \textsc{assume} is a $[]$ formula, so everything
we prove using it is true for all suffixes of the behavior we are
reasoning about.  For example, assuming $[]Inv$ allows us to use
$Inv$ in proving the hypothesis of the rule
 \[ \proofrule{I /\ [N]_{v} => I'}%
    {I /\ [][N]_{v} => []I}
 \]

-------------------------------------------------------------

\subsubsection{Proving \protect\ensuremath{\protect\leadsto} Formulas}

One often wants to prove that a specification satisfies a property of
the form $F ~> G$.  I now explain how such a property is proved.

\paragraph{One-Step \protect\ensuremath{\protect\leadsto} Properties}
\mbox{}\V{.2} 
  \ctindex{1}{one-step \mmath{\icmd{leadsto}} property}{one-step}%
A one-step $~>$ property $F~>G$ is one that holds
because fairness of an action $A$ implies that whenever $F$ holds, a
step of $A$ must eventually occur that makes $G$ true.  For example,
consider this code from the one-bit protocol:
\begin{display}
\begin{tabbing}
$r:$ \= \pwhile (\TRUE) \+\V{.2}
  \s{1}\= \{ \= $e1$: \= \+ \kill
  \{ \> \> \ldots\+ \V{.2}
       $e1$: \> $x[self] := \TRUE$ ; \V{.2}
       $e2$: \> \pif\ $(\,~x[1\!-\!self]\,)$ \{ $cs$: critical section \} \- \\

  \}
\end{tabbing}
\end{display}
Weak fairness implies that if a process is ever at $e1$, then
it eventually reaches $e2$.  More precisely, for a process $i$, weak
fairness of the process means that the algorithm's specification
implies
  $(pc[i]="e1")~>(pc[i]="e2")$.
This is because the $pc[i]="e1"$ implies that the process's next-state
action is enabled, and it must remain enabled at least until the
action is executed.  Weak fairness then implies that the process's
next-state action must eventually be executed, making $pc[i]="e2"$
true.

Weak fairness does not imply 
  $(pc[i]="e2")~>(pc[i]="cs")$
since executing the $e2$ action when $x[1-i]]$ is true sets $pc[i]$ to
$"r"$.  In fact, weak fairness does not even imply
 \[ (pc[i]="e2") /\ ~x[1-i] \; ~>\;(pc[i]="cs")
 \]
because $(pc[i]="e2") /\ ~x[1-i]$ could be true, then $x[1-i]$ could
be set to \TRUE\ and remain forever equal to \TRUE. It would then be
impossible for $pc[i]$ ever to equal $"cs"$, so the $~>$ property is
false for such a behavior.  Even if $x[1-i]$ did not remain true
forever, if process $1-i$ repeatedly set $x[1-i]$ false (in the
``\ldots'' code) and repeatedly set it true, there would exist an
execution in which $e2$ was always executed when $x[1-i]$ was true, so
$pc[i]$ never equaled $"cs"$.  However, weak fairness does imply\target{boxx1i}
  \[ (pc[i]="e2") /\ []~x[1-i] \; ~>\;(pc[i]="cs") 
  \]
If $(pc[i]="e2") /\ []~x[1-i]$ ever becomes true, then $x[1-i]$ is
false and remains false forever.  Weak fairness then implies that
process $i$ must take an $e2$ step when $x[1-i]$ is false, making
$pc[i]="cs"$ true.  You will see later how, in the course of a proof,
we can deduce that  $(pc[i]="e2") /\ []~x[1-i]$ becomes true.

In the Principles track of this hyperbook, we will be content with
informal proofs of these one-step $~>$ properties.  They can be
deduced formally from weak fairness assumptions using a single TLA
proof rule.  If you are curious about this rule, you can
  \popref{rule-wf1}{read about it here}.


\paragraph{The Leads-To Induction Rule} \mbox{} \V{.2}
%
 \tindex{1}{leads-to induction rule}%
 \tindex{1}{induction, leads-to}%
One-step $~>$ properties, which follow directly from fairness
assumptions, assert that something happens in a single step---usually
a step of a process.  The heart of proving liveness properties is
combining one-step $~>$ properties to deduce properties $F~>G$ in
which it takes many steps to go from $F$ being true to $G$ becoming
true.  I now explain the rules for deducing $~>$ properties from
simpler $~>$ properties.

We can deduce a ``two-step'' $~>$ property from two one-step $~>$
properties using the following tautology, which asserts the
transitivity of $~>$\,:
%
%\begin{equation} {\NOTLA \label{eq:fgh}}
 \[ (F ~>G)\; /\ \; (G~>H)\; => \; (F ~> H) \]
%\end{equation}
%from (\ref{eq:fgh})
By induction, we can generalize this to 
% the 
%  \[ (F_{n} ~> F_{n-1} ~> \ldots ~> F_{0}) \; => \; (F_{n} ~> F_{0})
%  \]
% This is an abbreviation for 
  \[ (F_{n}~>F_{n-1}) \; /\ \; \ldots \; /\ \; (F_{1} ~> F_{0})
      \; => \; (F_{n} ~> F_{0})
 \]
We can further generalize this as follows.  Suppose we have a finite
directed graph with no cycles that contains a single sink node.  Let's
take it to be the following graph that has the sink $z$; we'll
generalize later.
% \begin{display}
% \begin{picture}(0,128)(-10,-10)
% %{\gray\graphpaper(0,0)(400,200)}
% \put(0,100){\circle{20}}
% \put(0,100){\makebox(0,0){$T$}}
% \put(0,50){\circle{20}}
% \put(0,50){\makebox(0,0){$U$}}
% \put(0,0){\circle{20}}
% \put(0,0){\makebox(0,0){$V$}}
% %
% \put(100,100){\circle{20}}
% \put(100,100){\makebox(0,0){$W$}}
% \put(100,50){\circle{20}}
% \put(100,50){\makebox(0,0){$X$}}
% \put(150,0){\circle{20}}
% \put(150,0){\makebox(0,0){$Y$}}
% \put(200,50){\circle{20}}
% \put(200,50){\makebox(0,0){$Z$}}
% %
% %\put(8.8,54.4){\circle{2}}
% \thicklines
% \put(10,100){\vector(1,0){80}}
% \put(10,50){\vector(1,0){80}}
% \put(10,0){\vector(1,0){130}}
% \put(110,50){\vector(1,0){80}}
% %
% \put(9,54.5){\vector(2,1){81.5}}
% \put(9,4.5){\vector(2,1){81.5}}
% \put(109,95.5){\vector(2,-1){81.5}}
% \put(9.6,46.8){\vector(3,-1){130.5}}
% \put(107.2,42.8){\vector(1,-1){35.6}}
% \put(157.2,7.2){\vector(1,1){35.6}}%
% \qbezier(9.9,103)(155,145)(192.4,64)
% \put(195,59){\vector(1,-2){0}}
% \end{picture}
% \end{display}
%
\begin{display}
\begin{picture}(0,128)(-10,-10)
%{\gray\graphpaper(0,0)(400,200)}
\put(0,100){\circle{20}}
\put(0,100){\makebox(0,0){$t$}}
\put(0,50){\circle{20}}
\put(0,50){\makebox(0,0){$u$}}
\put(0,0){\circle{20}}
\put(0,0){\makebox(0,0){$v$}}
%
\put(100,100){\circle{20}}
\put(100,100){\makebox(0,0){$w$}}
\put(100,50){\circle{20}}
\put(100,50){\makebox(0,0){$x$}}
\put(150,0){\circle{20}}
\put(150,0){\makebox(0,0){$y$}}
\put(200,50){\circle{20}}
\put(200,50){\makebox(0,0){$z$}}
%
%\put(8.8,54.4){\circle{2}}
\thicklines
\put(10,100){\vector(1,0){80}}
\put(10,50){\vector(1,0){80}}
\put(10,0){\vector(1,0){130}}
\put(110,50){\vector(1,0){80}}
%
\put(9,54.5){\vector(2,1){81.5}}
\put(9,4.5){\vector(2,1){81.5}}
\put(109,95.5){\vector(2,-1){81.5}}
\put(9.6,46.8){\vector(3,-1){130.5}}
\put(107.2,42.8){\vector(1,-1){35.6}}
\put(157.2,7.2){\vector(1,1){35.6}}%
\qbezier(9.9,103)(155,145)(192.4,64)
\put(195,59){\vector(1,-2){0}}
\end{picture}
\end{display}
%
Suppose that we start with a token on any of the nodes and move it
according to the following rule: if the token is not on the sink node,
then it must eventually move along one of the edges from its current
node to another node.  For example, if the token is on node $x$, it
must eventually move to node $y$ or node $z$.  Obviously, the token
must eventually end up on the sink node.

Now, let's assign to each node $n$ a formula $F_{n}$.  In the token
game, let's interpret the token being on node $n$ to mean that $F_{n}$
is true.  The rule about how tokens must move corresponds to the
assumption that if $F_{n}$ is ever true, then $F_{q}$ must eventually
become true for some node pointed to by an edge from $n$.  In other
words, we assume that $F_{n}$ leads to the disjunction of all
formulas $F_{q}$ for which there is an edge from $n$ to $q$.
The conjunction of all those assumptions is the formula:
 \[ (F_{t} ~> (F_{w} \/ F_{z})) \; /\ \; ( F_{u}~> (F_{w} \/ F_{x} \/ F_{y}))
      \; /\ \; \ldots \; /\ \; (F_{y} ~> F_{z})
 \]
We observed that if the token is placed on any node, then it
eventually reaches the sink node.  Therefore, if we start with at
least one formula $F_{t}$ true, then eventually $F_{z}$ must be true.
In other words, the formula we are assuming implies
 \[ (F_{t} \/ F_{u} \/ \ldots \/ F_{z}) \,~> \, F_{z}
 \]
To generalize all this, let's require that there is an edge from every
other node to the sink node.  This requirement weakens what we are
assuming.  In terms of the token game, our assumption is weaker
because having more nodes that the token can move to weakens the
assumption that it must move.  In terms of formulas, our assumption is
weaker because $G ~> H \/ K$ is weaker than (is implied by)
 $G ~> H$, for any formulas $G$, $H$, and $K$.

%\newcommand{\N}{\mathcal{N}}
We now generalize to a set $\N$ of nodes.  Let's define the relation
$\succ$ on $\N$ by letting $m\succ n$ be true iff there is an edge from
$m$ to $n$, for any $m$ and $n$ in $\N$.  The absence of cycles in the
graph is equivalent to the assumption that there is no ``infinite
chain''
 \[ n_{1} \succ n_{2} \succ n_{3} \succ \ldots
 \]
of elements in $\N$.  The relation $\succ$ is said to be
  \tindex{4}{well-founded}%
  \ctindex{4}{relation!well-founded}{rel-well-founded}%
\emph{well-founded} on $\N$ iff this condition holds.  

Since we're requiring there to be an edge from every other node to the
sink, a node $z$ is a sink iff $n\succ z$ holds for every other node
$n$ of $\N$.  In other words, our requirement that the graph has no
cycles and has a single sink $z$ can be expressed as: $\succ$ is a
well-founded relation on $\N$ with minimum element $z$.

For any element $n$ of $\N$, define $\N\!_{n\,\succ}$ to be the
set of all elements $m$ of $\N$ such that $n\succ m$.  Our token-game
assumption is that, from any non-sink node $n$, the token eventually
moves to some node in $\N\!_{n\,\succ}$.  The corresponding temporal
property for node $n$ is 
   $F_{n}~>(\E m \in \N\!_{n\,\succ} : F_{m})$.
Our general rule states that, if this formula is true for all
nodes other than the sink node, then: if there exists some node
$n$ with $F_{n}$ true, then eventually $F_{z}$ is true:
\begin{display}
\textbf{Leads-To Induction Rule } If $\succ$ is a well-founded
relation on a set $\N$ with minimum element $z$, then:
 \[ \begin{noj}
    (\A \,n \in \N \,:\:\, \{z\} : 
           F_{n}~>(\E\, m \in \N\!_{n\,\succ} : F_{m})) \\
    \s{2}=> \\
    ((\E \,n \in \N : F_{n}) ~> F_{z})
    \end{noj}
 \]
\end{display}
The graph has disappeared from the rule, being replaced by a
well-founded relation with minimum element.  Also gone is the
assumption that the graph is finite.  The rule is valid for infinite
sets $\N$ as well.  The argument about the token game does not depend
on having a finite number of nodes, but only on there not being an
infinite path having a first node.

The most common example of a well-founded relation on an infinite set
$\N$ with minimum element is the relation $>$ on the set $Nat$ of
natural numbers, which has minimum element~0.  Another useful
well-founded relation on an infinite set is lexicographical ordering
on the set of $k$-tuples of natural numbers.  This ordering is defined
by letting $<<a_{1}, \ldots \, a_{k}>> \succ <<b_{1}, \ldots \, b_{k}>>$ 
be true iff there is some $i$ in $1\dd k$ such that $a_{i}> b_{i}$
and $a_{j} = b_{j}$ for all $j$ in $1\dd(i-1)$.  This is a well-founded
ordering with minimal element $<<0, \ldots, 0>>$.

\medskip

When explaining a use of the Leads-To Induction Rule in a proof, it
usually helps to draw the directed graph of the relation $\succ$ with
the actual formulas $F_{n}$ as the nodes.  For example, here is the graph
used in a proof of $T1 ~> \FALSE$.
\begin{display}
\begin{picture}(0,70)(0,0)
%      {\gray\graphpaper(0,0)(300,200)}
      \put(0,30){\makebox(0,0)[l]{$T1$}}
      \put(40,30){\makebox(0,0)[l]{$\Box T1$}}
      \put(160,60){\makebox(0,0)[t]{$T0$}}
      \put(85,0){\makebox(0,0)[lb]{$\Box (T1 \land \lnot T1)$}}
      \put(175,0){\makebox(0,0)[lb]{$\Box (T1 \land \lnot x[0])$}}
      \put(257,30){\makebox(0,0)[l]{$\FALSE$}}
      \thicklines
      \put(18,30){\vector(1,0){17}}
      \put(62,25){\vector(3,-2){20}}
      \put(64,34){\vector(4,1){87}}
      \put(150,6){\vector(1,0){20}}
      \put(240,10){\vector(1,1){15}}
      \put(170,55){\vector(4,-1){85}}
      \end{picture}
\end{display}
I will call such a graph a \emph{proof graph}.
Note that the proof is also using the observation that
 $(\E \,n \in \N : F_{n}) ~> F_{z}$
implies $F_{n} ~> F_{z}$, for any $n$ in $\N$.  This observation
follows from the proof rule $(H=>F) |- ((F~>G) => (H~>G))$.

\medskip

The Leads-To Induction Rule was originally called the \emph{Lattice
Rule}, which was a misleading name because the rule has nothing to do
with what mathematicians call lattices.  The following question
explains why I prefer to call it Leads-To Induction.
\begin{question}
The validity of the Leads-To Induction Rule depends only on the
transitivity of $~>$.  Ordinary implication is also transitive.
Therefore, the rule obtained from Leads-To Induction by replacing $~>$
with $=>$ is also valid.  Show that the following substitutions then
produce the rule for ordinary mathematical induction:
 \[ F_{n} \;<-\; ~F_{n} \s{2} \N \;<-\; Nat \s{2} \succ \;\; <- \;\; > 
   \s{2} z \;<-\; 0
 \]
\end{question}

\begin{aquestion}{leads -to-induction}
\sloppy
Define a \tlaplus\ operator $LeadsToInduction$ so that
 \[ LeadsToInduction(F,\, \N, \, \succ,\, z) \] 
expresses the Leads-To Induction Rule, writing $F(n)$ instead of
$F_{n}$ and $LTSet(\N,\,\succ)$ instead of $\N\!_{n\,\succ}$.  You
should include the definition of $LTSet$ and of a well-founded
relation with minimum element.
\end{aquestion}

\paragraph{\protect\ensuremath{\implies} Implies 
     \protect\ensuremath{\leadsto}} \mbox{}\V{.2}
%
Because $G=><>G$ is a tautology, it follows that 
  \[ [](F => G) => (F~>G)
  \]
is also a tautology.  Hence, we can deduce $F~>G$ from $[](F => G)$.
For example, $P => (P /\ Q) \/ (P /\ ~Q)$ is a tautology.  Therefore, by the
temporal proof rule $(F=>G)|-[](F=>G)$ it implies 
 $[](P => (P /\ Q) \/ (P /\ ~Q))$ and hence $P ~> (P /\ Q) \/ (P /\ ~Q))$.
This is often used to justify a subgraph
\begin{display}
%\setlength{\unitlength}{.6pt}
\begin{picture}(0,70)(-10,-10)
\put(50,50){\circle{20}}
\put(50,50){\makebox(0,0){$b$}}
\put(0,25){\circle{20}}
\put(0,25){\makebox(0,0){$a$}}
\put(50,0){\circle{20}}
\put(50,0){\makebox(0,0){$c$}}
\thicklines
\put(7.2,17.8){\vector(2,-1){32.6}}
\put(7.2,32.2){\vector(2,1){32.6}}%
\end{picture}
\end{display}
in applying the Leads-To Induction Rule, with $F_{a}=P$, $F_{b}=P /\ Q$,
and $F_{c} = P /\ ~Q$

In a proof in which only $[]$ formulas appear in \textsc{assume}s, if
we prove $F=>G$ then we can apply the rule $(F=>G)|-[](F=>G)$ to deduce
$[](F=>G)$ and hence $F~>G$.  Therefore, in such a proof, we can prove
$F~>G$ by proving $F=>G$.

A common use of this approach is to prove $P ~> []P$ by proving
$P=>[]P$, for a state predicate $P$.  To prove $P => []P$, we
use the invariance proof rule:
 \[ \proofrule{I /\ [N]_{v} => I'}%
    {I /\ [][N]_{v} => []I}
 \]
Remember that in a proof with only $[]$ formulas as assumptions, the
assumption $[]Inv$ allows us to use $Inv$ to prove the hypothesis of
this rule.

% When proving $~>$ formulas, $[]$ formulas are nice because 
% ``they are true forever''.  More precisely, we can use
% the following tautology: 
%  \[ (P /\ []Q ~> R) \;=>\; (P /\ []Q ~> R /\ []Q) \]
% This means that, when using the Leads-To Induction Rule, if some
% $F_{n}$ equals $P /\ []Q$, then we can let $[]Q$ be a conjunct of
% $F_{m}$ for all $m$ with $n\succ m$.

% When we want to prove that a specification satisfies a liveness
% property of the form $P~>Q$, the formulas $P$ and $Q$ are usually
% state predicates.  The operator $~>$ was defined and used informally
% for state predicates before the introduction of temporal logic into
% computer science.  The Leads-To Induction rule was also used, with the
% formulas $F_{n}$ being state predicates.  
% 
% The great advance provided by temporal logic was the power obtained by
% letting the $F_{n}$ be temporal formulas---in particular, formulas of
% the form $R /\ []S$, for state predicates $R$ and $S$.  The tautology
%   \[ (R /\ []S ~> T) => (R /\ []S ~> T /\ []S)
%   \]
% by now should be obvious to you.  It means that, when using the
% Leads-To Induction Rule, if some $F_{n}$ equals $R /\ []S$, then we
% can let $[]S$ be a conjunct of $F_{m}$ for all $m$ with $n\succ m$.
% We will see that this 

\paragraph{The \protect\ensuremath{\Box\leadsto} Rule}\mbox{}\V{.2}
%
  \ctindex{1}{+3v+r2rule@\mmath{\icmd{Box}\icmd{leadsto}} rule}{+3v+r2rule}%
  \ctindex{1}{rule!\mmath{\icmd{Box}\icmd{leadsto}}}{rule+3v+r2}%
From the meaning of $F~>H$ and $[]$, it's obvious that
 \[([]F~>H)\,=>\,([]F~>(([]F) /\ H ))\] 
is a tautology.  This is a special case of the following tautology
(with \TRUE\ substituted for $G$):
 \[(([]F /\ G)~>H)\,=>\,(([]F /\ G)~>(([]F) /\ H ))\] 
Suppose we're proving $([]P /\ Q)~>R$ by Leads-To Induction using a
graph having $[]P /\ Q$ as its only source node.  The second tautology
implies that we can let $[]P$ be a conjunct of all the formulas in the
proof graph.  Instead of explicitly making it a conjunct, we can
simply assume $[]P$ in the proof of $Q~>R$, usually employing this
proof structure:
\begin{display}
$<<i>>j$. $([]P /\ Q)~>R$\V{.4}
\s{1}$<<i+1>>1$. \textsc{Suffices }$\begin{noj2}
                               \textsc{Assume:} & []P \\
                                \textsc{Prove:} & Q ~> R
                               \end{noj2}$
\end{display} 
The justification for the \textsc{Suffices} step is this proof rule:
\begin{display}
$[]~>$ Rule: $\proofrule{[]P => (Q~>R)}{([]P /\ Q) ~> ([]P /\ R)}$
\end{display}
For a short Leads-To Induction proof, we may not bother with this
rule and just conjoin $[]P$ to the formulas in the proof graph.

\paragraph{Proving \protect\ensuremath{\leadsto} Formulas by 
   Contradiction}\mbox{}\V{.2}
%
 \tindex{1}{contradiction, proof by}%
Proofs by contradiction are nice because they allow us to use an
additional hypothesis---namely, the negation of the formula we are
trying to prove.  This is a very strong hypothesis because, if what we
are trying to prove is true, then the hypothesis is equivalent to
\FALSE, which is the strongest possible hypothesis.

A proof by contradiction of a $~>$ formula is based on the
tautology:
 \[ F ~> (G \/ (F /\ []~G))
 \]
This is a tautology because, at any point in an execution, either
$G$ eventually becomes true or it is always false.  Hence, to
prove $F~>G$, it suffices to prove that $(F /\ []~G)$ can never be
true.  We do that by proving $(F /\ []~G)~>\FALSE$, since
only $\FALSE$ can lead to $\FALSE$.  In other words, a proof
by contradiction of $F~>G$ uses this tautology:
 \[ ( (F /\ []~G) ~> \FALSE ) \; => \; (F ~> G)
 \]
To prove $(F /\ []~G) ~> \FALSE$, it is often convenient to use the
proof rule:
  \[ \proofrule{[]H => (F ~> G)}
               {F /\ []H \, ~> G}
 \]
This proof rule shows that, to prove $F /\ []~G ~> \FALSE$, it suffices
to assume $[]~G$ and prove $F ~> \FALSE$.

In the one-step property
 \[ (pc[i]="e2") /\ []~x[1-i] \; ~>\;(pc[i]="cs") \]
\lref{boxx1i}{discussed above}, the hypothesis $[]~x[1-i]$ 
is deduced from an assumption $[]~G$ in a proof by contradiction
of a property $F~>G$.

REDUCTION STUFF


Taking these to be the elementary data items, and allowing a single
step to either read or write a single item, the body of the outer
\textbf{while} loop should be:
\begin{display}
\begin{nopcal}
e1: unchecked := Procs \ {self} ;
e2: max := 0;
e3: while (unchecked # {}) 
      { e4: ...
\end{nopcal}
\begin{tlatex}
 \@x{ e1\@s{.5}\textrm{:}\@s{3} unchecked \.{:=} Procs \.{\,\backslash\,} \{
 self \} {\p@semicolon}}%
\@x{ e2\@s{.5}\textrm{:}\@s{3} max \.{:=} 0 {\p@semicolon}}%
 \@x{ e3\@s{.5}\textrm{:}\@s{3} {\p@while} {\p@lparen} unchecked \.{\neq} \{
 \} {\p@rparen}}%
\@x{\@s{24.82} {\p@lbrace} e4\@s{.5}\textrm{:}\@s{3} \.{\dots}}%
\end{tlatex}
\end{display}
Note that a constant like $Procs$ or $self$ is not part of the state
and is not a data item.  Action $e1$ writes the elementary data item
$unchecked[self]$, action $e2$ writes the item $max[self]$, action
$e3$ reads the item $unchecked[self]$, etc.

This approach produces an algorithm with a fine enough grain of
atomicity, but it's finer-grained than we would like.  To make model
checking faster and to make proving correctness easier, we want our
algorithm to be as coarse-grained as possible.  We can make a PlusCal
algorithm coarser grained by removing labels.  So, we address the
question: When can we remove a label from a PlusCal algorithm?  To
answer it, we need some notation about actions.

For states $s$ and $t$ and action $A$, let $s\ar{A}t$ be the
assertion that transition $s->t$ is allowed by action $A$.  For any
actions $A$ and $B$, let $A\cdot B$ be the action that first performs
$A$ and then $B$.  More precisely, define $A\cdot B$ to be the
action such that $s\ar{A\cdot B}t$ is true iff there is a state $u$
such that $s\ar{A}u$ and $u\ar{B}t$.  We abbreviate ``$s\ar{A}u$ and
$u\ar{B}t$'' as $s\ar{A}u\ar{B}t$.

Recall that a statement labeled $a$ produces in the \tlaplus\
translation an action $a(i)$ that describes the steps permitted by
process $i$ executing statement $a$.  In our mutual exclusion code
\begin{display}
\begin{nopcal}
e1: unchecked := Procs \ {self} ;
e2: max := 0;
e3: ...
\end{nopcal}
\begin{tlatex}
 \@x{ e1\@s{.5}\textrm{:}\@s{3} unchecked \.{:=} Procs \.{\,\backslash\,} \{
 self \} {\p@semicolon}}%
\@x{ e2\@s{.5}\textrm{:}\@s{3} max \.{:=} 0 {\p@semicolon}}%
 \@x{ e3\@s{.5}\textrm{:}\@s{3} \.{\dots}}%
\end{tlatex}
\end{display}
$e1(i)\cdot e2(i)$ is the action $e1(i)$ of the algorithm obtained by
removing the label~$e2$.

We say that actions $A$ and $B$ \emph{commute} if executing them in
either order has the same effect.  More precisely, $A$ and $B$ commute
iff $A\cdot B$ is equivalent to $B\cdot A$.  That is, $A$ and $B$
commute iff these two conditions are equivalent, for any states $s$
and $t$:
\begin{itemize}
\item There exists $u$ such that $s\ar{A}u\ar{B}t$.
\item There exists $v$ such that $s\ar{B}v\ar{A}t$.
\end{itemize}
For our mutual exclusion example, $e1(i)$ and $e2(i)$ do not commute
because $e2(i)\cdot e1(i)$ equals $\FALSE$.  For any states $s$ and
$t$ there is no state $u$ with $s\ar{e2(i)}u\ar{e1(i)}t$ because
$s\ar{e2(i)}u$ implies $pc[i]="e3"$ in state $u$, while $u\ar{e1(i)}t$
implies $pc[i]="e1"$ in that state.  However, $e1(i)$ and $e(j)$ commute 
for any process $j$ different from~$i$.
Action $e1(i)$ reads only $pc[i]$ and writes only $pc[i]$ and
$unchecked[i]$.  Action $e2(j)$ reads only $pc[j]$ and writes
only $pc[j]$ and $max[j]$.  Hence, executing the two actions in either
order has the same effect.  In fact, since no action of process~$j$
can access (read or write) $pc[i]$ or $unchecked[i]$ (since $unchecked$
is a process-local variable), $e1(i)$ commutes with $f(j)$ for any
label $f$.  A little thought generalizes from this example to:
\begin{display}
\textbf{PlusCal Commutativity Rule } If $e$ and $f$ are labels of
an algorithm and $e$ labels a statement that (a)~reads no
elementary data item written by another process and (b)~writes no
elementary data item accessed by another process, then actions $e(i)$
and $f(j)$ commute for any two distinct processes $i$ and~$j$.
\end{display}
We now use this rule to show that we can remove the label $e2$.

Let $\Pi$ be the finer-grained algorithm, and let $\widehat{\Pi}$ be
the coarser-grained algorithm obtained by removing label $e2$.  We
want to show that we can deduce that $\Pi$ satisfies mutual exclusion
by proving that $\widehat{\Pi}$ does.  (We ignore liveness for now.)
To do this, we show that if there exists a behavior $\sigma$ of $\Pi$
in which mutual exclusion is violated, then there exists a behavior
$\widehat{\sigma}$ of $\widehat{\Pi}$ in which mutual exclusion is
also violated.  Here's how we construct $\widehat{\sigma}$ from
$\sigma$.  For simplicity, we assume that $\sigma$ has no stuttering
steps.  Let $\sigma$ be \,$s_{1}-> s_{2} -> \cdots$\,.  We can find
actions $A_{j}$ such that
  \[ s_{1}\ar{A_{1}}s_{2}\ar{A_{2}}s_{3}\ar{A_{3}}s_{4}\;\cdots \]
where each $A_{j}$ is an action $r(i)$ for some label $r$ and process
$i$.  The idea is that if $A_{j}$ is $e2(i)$ for some process $i$,
then we remove the $j$\tth\ step; and if $A_{j}$ is $e1(i)$ then we
make the $j$\tth\ step an $e1(i)\cdot e2(j)$ step.

Suppose that the 41\st\ step is an $e2(7)$ step (an $e2$ step of process~7).
Find the most recent $e1(7)$ step before that 41\st\ step; let's suppose
it's the 37\tth\ step. Steps 38--41 are steps of other processes.  Suppose
that part of the behavior is:
 \[ \cdots\ s_{37} \ar{e1(7)} s_{38} \ar{e3(9)} s_{39} 
      \ar{cs(14)} s_{40} \ar{e4(9)} s_{41} \ar{e2(7)} s_{42} \ \cdots
 \]
By the PlusCal Commutativity Rule, $e2(7)$ commutes with all actions
of all processes other than process~14, including the $e4(9)$
action.  We can therefore find a state $t_{41}$ such that
  $s_{40} \ar{e2(7)} t_{41} \ar{e4(9)} s_{42}$, so 
   \[ \cdots\ s_{37} \ar{e1(7)} s_{38} \ar{e3(9)} s_{39} 
      \ar{cs(14)} s_{40} \ar{e2(7)} t_{41} \ar{e4(9)} s_{42} \ \cdots
  \]
is a possible behavior of algorithm $\Pi$.  Similarly, 
$e2(7)$ commutes with $cs(14)$ and $e4(9)$, so we can find
state $t_{40}$ and  $t_{39}$ so 
  \[ \cdots\ s_{37} \ar{e1(7)} s_{38} \ar{e2(7)} t_{39} 
      \ar{e3(9)} t_{40} \ar{cs(14)} t_{41} \ar{e4(9)} s_{42} \ \cdots
  \]
is a behavior of algorithm $\Pi$.  Finally, combining the $e1(7)$ and
$e2(7)$ actions, we get this behavior. 
  \[ \cdots\ s_{37} \ar{e1(7)\cdot e2(7)} t_{39} 
       \ar{e3(9)} t_{40} \ar{cs(14)} t_{41} \ar{e4(9)} s_{42} \ \cdots
  \]  
If we do this type of transformation simultaneously for all $e2(i)$
actions, for all processes $i$, we obtain a behavior
$\widehat{\sigma}$ of $\widehat{\Pi}$.  It is easy to see that if
mutual exclusion is violated in $\sigma$---that is, if some state has
$pc[i]="cs"$ for two different processes $i$---then it is also
violated in $\widehat{\sigma}$.

There is one flaw in this argument: what if some process $i$ executes
$e1(i)$ and stops without executing a subsequent $e2(i)$ action?  (We
have not yet assumed any fairness conditions.)  If $\sigma$ violates
mutual exclusion, then there it does so in some state---say the
351\st\ state.  We can then find a behavior $\tau$ of $\Pi$ that has
the same first 351 states as $\sigma$, and then executes the algorithm
in such a way that every enabled $e2(i)$ action is eventually
executed.  We can then apply the argument to construct
$\widehat{\tau}$.

\medskip

It is clear that this procedure generalizes to removing a label $e$
from any algorithm $\Pi$ for which $e(i)$ commutes with $f(j)$ for any
label $f$ and any processes $i$ and $j$ with $i#j$.  For any behavior
$\sigma$ satisfying the original algorithm, we obtain a behavior
$\widehat{\sigma}$ of the coarser-grained algorithm by using
commutativity to combine an $e(i)$ step with the preceding step of
process~$i$.  The procedure requires that an $e(i)$ step is enabled
whenever control in process~$i$ is at $e$.

This procedure effectively combines step $e$ with the preceding step
(or steps) of the algorithm.  If $e(i)$ commutes with all actions
of other processes, we can also combine $e$ with the following
step of the algorithm.  For example, we can replace
 \[ \ldots\ e: E\,; \ f : F\,; \ g : \ \ldots
 \]
with
 \[ \ldots\ \ e : E\,; F\,; \ g : \ \ldots
 \]
The argument is similar, except we construct $\widehat{\sigma}$ from
$\sigma$ by moving each $e(i)$ step to the right until it immediately
precedes an $f(i)$ step.  In this case, no enabledness assumption is
needed because if an $e(i)$ step is not followed by an $f(i)$ step, we
just move the $e(i)$ step to the right past the state point at which
$\sigma$ violates the safety property and then complete the behavior
finite prefix 


construct $\tau$ as above
from that 

\medskip

It is clear that, as long as we 

-----------------------------------------------------------------------------



\subsection{The Bounded Channel in PlusCal}

\subsubsection{Getting Started}
We now rewrite the Bounded Channel specification in PlusCal.
Create a new module named $PCalBoundedChannel$.  It begins like
the $BoundedChannel$ module:
\begin{twocols}
\begin{notla}
EXTENDS Integers, Sequences
CONSTANT Msg, N
ASSUME N \in Nat \ {0}
\end{notla}
\begin{tlatex}
\@x{ {\EXTENDS} Integers ,\, Sequences}%
\@x{ {\CONSTANT} Msg ,\, N}%
\@x{ {\ASSUME} N \.{\in} Nat \.{\,\backslash\,} \{ 0 \}}%
\end{tlatex}
\midcol
%\begin{verbatim*}
\verb*|EXTENDS Integers, Sequences|\V{.2}
\verb*|CONSTANT Msg, N|\V{.2}
\verb*|ASSUME N \in Nat \ {0}|
%\end{verbatim*}
\end{twocols}
Instead of writing the initial predicate and next-state action in
\tlaplus, we write PlusCal code that produces them.  As before, the
algorithm goes in a multi-line comment.  It begins with the
\textbf{-{}-algorithm} keyword and its name, which we take to be
$BChan$; and it next declares the variable $ch$ with its initial value:
\begin{display}
$(****************************************************$\\
\algorithm\ $BChan$ \{\\
\s{1.5}\variable\ $ch\;=\;<< >>$;\V{.5}
\}\\
$*****************************************************)$
\end{display}

A process's 
  \ctindex{1}{process!identifier}{process-identifier}%
  \ctindex{1}{identifier!process}{identifier-process}%
identifier is usually a simple value like an integer or a
string, but it could be any value---for example, the pair $<<"proc",
42>>$.  However, all processes in an algorithm must have identifiers
that are unequal to one another.  This means that we cannot let $Send$
have identifier $"S"$ and $Rcv$ have identifier $<<"Rcv">>$, because
the semantics of \tlaplus\ does not determine whether or not the
string $"S"$ equals the one-tuple $<<"Rcv">>$.  In practice, this
means that we usually let all the process identifiers of an algorithm
have the same ``type''---for example, all strings or all numbers.

The body of each process is repeatedly executed forever, so it consists
of a \pwhile~$(\TRUE)$ loop.  For the $Send$ process, the loop is
\begin{display}
\begin{tabbing}
\pwhile\ $(\TRUE)$ 
\s{.5}\= \{ \= \await\ $Len(ch) # N$ ; \\
\>\>            \with\ $(v \in Msg)$ \{ $ch := Append(ch, v)$ \}\\
\>        \}
\end{tabbing}
\end{display}


% The 
%       \ctindex{2}{await (PlusCal statement)@\icmd{await} (PlusCal statement)}{await-pcal}%
% \await\ statement can be executed only when its predicate,
$Len(ch) # N$, equals $\TRUE$, in which case the next statement can
then be executed.  The 
    \ctindex{9}{with (PlusCal keyword)@\icmd{with} (PlusCal keyword)}{with-pcal}%
\with\ statement nondeterministically chooses
an arbitrary value $v$ in the set $Msg$ and executes its body, in this
case the assignment statement, for that value of $v$.  The body of
process $Rcv$ is similar, except $ch$ is set to the tail of its
current value.
\begin{display}
\begin{tabbing}
\pwhile\ $(\TRUE)$ 
\s{.5}\= \{ \= \await\ $Len(ch) # 0$ ; \\
\>\>            $ch := Tail(ch)$ \\
\>        \}
\end{tabbing}
\end{display}
% 
% We then add the lines
% \begin{display}
% \verb|\* BEGIN TRANSLATION|\\
% \verb|\* END TRANSLATION|
% \end{display}
% after the comment containing the algorithm, 
% 
Save the file, and run the
translator.  It reports something like this:
\begin{display}
\tt
-- Missing labels at the following locations:
   line 12, column 8
   line 18, column 9
\end{display}
where the line and column locations point to the two \pwhile\ statements.
Let's now see what the problem is.

-----------------------------------------------------------------------------



\subsubsection{Specifying the Grain of Atomicity} 
\xlabel{main:intro-atomicity}

To understand why the translator is complaining, let's examine the
PlusCal version of the one-bit clock specification.  The algorithm's
body consists of the loop:
\begin{display}
\pwhile\ $(\TRUE)$ \{ \pif\ $(b = 0)$ $b := 1$ \pelse\ $b := 0$ \}
\end{display}
Most people think of an execution of one iteration of the \pwhile\
loop as consisting of the following three steps:
\begin{enumerate}
\item Evaluate the \pwhile\ statement's test and find that it is true.

\item Evaluate the test $b=0$ of the \pif\ statement.

\item \begin{describe}{(a)}
      \item[(a)] If the \pif\ statement's test equals $\TRUE$, then execute
            the assignment $b := 1$, else
      \item[(b)] If the \pif\ statement's test equals $\FALSE$, then execute
            the assignment $b := 0$.
      \end{describe}
\end{enumerate}
However, 
  \target{main:atomic-action}%
the \tlaplus\ translation of this body yields a next-state
relation in which each iteration of the \pwhile\ loop is executed as a
single step (state change).  
A single step of a behavior is often
called an 
  \tindex{1}{atomic action}%
   \ctindex{1}{action!atomic}{action-atomic}%
\emph{atomic action}, and choosing what constitutes a single
step is often called the choosing the 
   \tindex{1}{grain of atomicity}%
   \ctindex{1}{atomicity!grain of}{atomicity-grain}%
\emph{grain of atomicity}.
Why did the translator choose this grain of atomicity?

For a sequential algorithm (one with no processes), the translator by
default chooses the coarsest grain of atomicity (the fewest steps)
that it can.  The translator cannot combine two iterations of a
\pwhile\ loop into a single step, so the best it can do is to make
each iteration of the loop a single step.  We usually don't care about
the grain of atomicity of a sequential algorithm, so we prefer a
coarse grain of atomicity because it makes model checking more
efficient (there are fewer reachable states) and it makes proving
correctness of the algorithm simpler (because the next-state action is
simpler).

The grain of atomicity is crucial to the correctness of a multiprocess
(concurrent) algorithm.  For example, consider the following algorithm:
\begin{display}
\begin{tabbing}
\algorithm\ $Increment$ \= \{ 
   \= \variable\ $x = 0$;\V{.2}
\>\> \process\ $(A = 1)$ \{ $x := x+1$ \} \V{.2}
\>\> \process\ $(B = 2)$ \{ $x := x+1$ \} \\
\> \}
\end{tabbing}
\end{display}
The algorithm starts with $x$ equal to 0, and each process simply
executes the assignment statement $x := x+1$ and halts.  If both
assignments are executed as a single (atomic) step, then the algorithm
terminates (when both processes terminate) with $x$ equal to 2.
However, if the assignment statement is executed in two steps, the
first step evaluating $x+1$ and the second step assigning the value to
$x$, then the algorithm can terminate with $x$ equal to either 1 or 2.
\begin{aquestion}{atomicity -question}
(a) When execution of each assignment statement takes two steps,
describe executions that end with $x$ equal to 1 and with $x$ equal to~2.

(b) If the assignment statements are executed in more than two steps,
what other possible values can $x$ have upon termination?
\end{aquestion}
By default, the translator requires the user to specify the grain of
atomicity for a multiprocess algorithm.  This is done by adding labels
  \tindex{9}{labels, PlusCal}%
  \ctindex{9}{PlusCal!labels in}{pluscal-labels-in}%
to the algorithm.  A single step consists of an execution from one
label to the next.  There are certain rules about where labels must or
must not appear.  The most important ones are:
\begin{itemize}
\item The first statement of a process must have a label.

\item Each \pwhile\ statement must be labeled.
\end{itemize}
The translator will tell you if you violate any of the labeling rules.
In the unlikely event that you can't figure out from the error message
what you need to do to fix a labeling problem, see Section~2.7 of the
   \hyperref{http://research.microsoft.com/en-us/um/people/lamport/tla/c-manual.pdf}{}{}{PlusCal
  language manual}.
The language manual also explains how to tell the translator to insert
any necessary labels that are missing.

For algorithm $BChan$, we can satisfy both of the rules above by
labeling the \pwhile\ statement in each process.  Since a step
consists of execution from one label to the next, using only these
labels means that an entire execution of one loop iteration is a
single step.  This is the same grain of atomicity as in the \tlaplus\
specification of module $BoundedChannel$, so let's use it.  A label
can consist of any sequence of letters, digits, and underscore (\_)
characters containing at least one letter.  Let's use the labels
$s$ and $r$, to get this complete algorithm:
\begin{display}
\begin{tabbing}
  \target{bounded-channel-process}%
\algorithm\ $BChan$ \{ \V{.3} 
\s{1}\variable\ $ch = << >>$;\V{.3}
\s{1}\process\ $(Send = "S")$\\
\s{2}\{ \=$s$: \=\+\pwhile\ $(\TRUE)$\+\\
\s{.5}\= \{ \= \await\ $Len(ch) # N$ ; \\
\>\>            \with\ $(v \in Msg)$ \{ $ch := Append(ch, v)$ \}\\
\>        \} \-\-\\
\s{2}\} \V{.5}
\s{1}\process\ $(Rcv = "R")$\\
\s{2}\{ \=
$r$: \>\+ \pwhile\ $(\TRUE)$ \\
\> \{ \> \await\ $Len(ch) # 0$ ; \\
\>\>            $ch := Tail(ch)$ \\
\>        \}\-\\
\s{2}\} \\
\s{.5}\}
\end{tabbing}
\end{display}
The \textsc{ascii} version of the module with the algorithm
\popref{PCalBoundedChannel}{is here}.  Run the translator (from the
\textsf{File} menu or by typing \textsf{control+t}).  The \tlaplus\
translation is the same as the specification in module
$BoundedChannel$ except that:
\begin{itemize}
\item The formatting is a little different.

\item The translator adds a definition of $ProcSet$, which it is not
clever enough to realize is not needed for this algorithm.

\item The translator adds the definitions of $vars$ and $Spec$, which
we will discuss later.
\end{itemize}
The sender's statement 
   \[ \await\ Len(ch)# N \]
is translated to the conjunct 
  $Len(ch)# N$
of the process's action.  A conjunct of an action that contains no
primes is an enabling condition for the action.  Observe how the
\with\ statement is translated to an existential quantification.  
 \sref{main}{main:nondeterministic-choice}{As we observed above},
nondeterministic choice is expressed in an action by existential
quantification.

-----------------------------------------------------------------------------









%
% 
% \begin{display}
% \begin{describe}{$Append(s, e)$}
% \item[$Seq(S)$] The 
%   \ctindex{1}{Seq@\mmath{Seq}}{Seq}%
% set of all finite sequences with elements in $S$.
% For example, $<<0, 42>>$ is an element of $Seq(Nat)$.
% 
% \item[$Len(s)$] The 
%     \ctindex{1}{Len@\mmath{Len}}{Len}%
% length of the finite sequence $s$.  For example:
% \[ Len(<<0, 42>>)=2 \mbox{\s{1}and\s{1}}Len(<< >>)= 0 \]
% 
% \item[$Append(s,e)$] The 
%      \ctindex{1}{Append@\mmath{Append}}{Append}%
% sequence obtained by appending the element $e$
% to the end (as the right-most element) of the finite sequence $s$.
% For example: 
%  \[ Append(<<4, "abc", -2>>, "d") = <<4, "abc", -2, "d">>\]
% 
% \item[$Tail(s)$] The 
%      \ctindex{1}{Tail@\mmath{Tail}}{Tail}%
% sequence obtained from the nonempty finite sequence
% $s$ by deleting its first element.  For example:
%   \[Tail(<<4, "abc", -2>>)=<<"abc", -2>>\]
% \end{describe}
% \end{display}
With these operators, writing the \tlaplus\ specification is
straightforward.  

In the Toolbox, create a new spec named
$BoundedChannel$.  The module begins as follows, where the constant
$Msg$ is the set of all possible messages that can be sent.
\begin{twocols}
\begin{notla}
EXTENDS Integers, Sequences

CONSTANT Msg, N

ASSUME N \in Nat \ {0}
% 
% VARIABLE ch
\end{notla}
\begin{tlatex}
\@x{ {\EXTENDS} Integers ,\, Sequences}%
\par\vspace{8.0pt}%
\@x{ {\CONSTANT} Msg ,\, N}%
\par\vspace{8.0pt}%
\@x{ {\ASSUME} N \.{\in} Nat \.{\,\backslash\,} \{ 0 \}}%
% \par\vspace{8.0pt}%
% \@x{ {\VARIABLE} ch}%
\end{tlatex}
\midcol
\verb*|EXTENDS Integers, Sequences|\\[-.4em]
\verb*| |\\
\verb*|CONSTANT Msg, N|\\[-.4em]
\verb*| |\\
\verb*|ASSUME N \in Nat \ {0}|\\[-.4em]
\end{twocols}
Since the value of $ch$ is always the sequence of messages that have
been sent so far, which is initially the empty sequence, the
type-correctness invariant and the initial predicate should be:
\begin{twocols}
\begin{notla}
TypeOK == ch \in Seq(Msg)

Init == ch = << >>
\end{notla}
\begin{tlatex}
\@x{ TypeOK \.{\defeq} ch \.{\in} Seq ( Msg )}%
\par\vspace{8.0pt}%
\@x{ Init \.{\defeq} ch \.{=} {\langle}\, {\rangle}}%
\end{tlatex}
\midcol
\verb*|TypeOK == ch \in Seq(Msg)|\\[-.2em]
\verb*| |\\
\verb*|Init == ch = << >>|
\end{twocols}
We now write the algorithm in PlusCal, in a comment in the module,
with the following skeleton.
\begin{display}
$(****************************************************$\\
\algorithm\ $BChan$ \{\\
\\
\}\\
$*****************************************************)$
\end{display}
Our single variable $ch$ initially equals the empty set $<< >>$,
so the algorithm begins with:
\begin{display}
\begin{twocols}
\variable\ $ch\;=\;<< >>$;
\midcol
\begin{verbatim}
variable ch = << >> ;
\end{verbatim}
\end{twocols}
\end{display}
Like the \popref{alternation}{our specification of $Alternation$},
the bounded channel algorithm has two processes, which we name
$Send$ and $Rcv$  give the identifiers $"S"$ and $"R"$,
respectively:
\begin{display}
\begin{tabbing}
\= \process\ $(Send = "S")$ \\
      \>\s{.5}\= \{   \verb|\*| process body\\ % \pwhile\ $(\TRUE)$ \\
%\>\>\s{1}\= \{ \\
%\>\>\>       \}\\
\>\>    \}\V{.5}
\> \process\ $(Rcv = "R")$\\
\>\> \{ \verb|\*| process body \\ % \pwhile\ $(\TRUE)$ \\ 
% \>\>\> \{ \\
% \>\>\> \} \\
\>\>    \}
\end{tabbing}
\end{display}
The $Send$ process repeatedly executes an atomic action that appends
an arbitrary message to the channel; it is enabled if the channel
has fewer than $N$ messages.  The body of the process
is:
\begin{display}
\begin{tabbing}
$s$: \pwhile\ $(\TRUE)$ 
\s{.75}\= \{ \= \await\ $Len(ch) < N$ ; \\
\>\>            \with\ $(v \in Msg)$ \{ $ch := Append(ch, v)$ \}\\
\>        \}
\end{tabbing}
\end{display}
The \rref{main}{main:with}{\textbf{with} statement} sets $v$
to a 
    \ctindex{1}{choice, nondeterministic}{choice-nondeterministic}%
    \tindex{1}{nondeterminism}%
nondeterministically chosen element of $Msg$ and appends it
to the sequence $ch$.

The $Rcv$ process repeatedly executes an atomic action that removes
the first message in the channel (and does nothing with it); it is
enabled if the channel has at most one message.  Its body is:
\begin{display}
\begin{tabbing}
\pwhile\ $(\TRUE)$ 
\= \{ \= \await\ $Len(ch) # 0$ ; \\
\>\>            $ch := Tail(ch)$ \\
\>        \}
\end{tabbing}
\end{display}
Here is \popref{BoundedChannel}{the complete spec} and
here is its
\popref{PCalBoundedChannel}{\textsc{ascii} text}, which you should
copy into the Toolbox.  I made one minor
change to the code above: To make the two processes more
symmetric, I changed the enabling condition of the $Send$ process's
action from $Len(ch) < N$ to $Len(ch) # N$.  Since the length of
 $ch\in1\dd N$ is true in any reachable state, the two
conditions are equivalent.

Run the PlusCal translator (by typing \textsf{Control+F}), and examine
the \tlaplus\ translation.  Observe that the definition of the
$Send$ action is:
 \[Send == \begin{conj}
         Len(ch) # N \\ \E\, v \in Msg : ch'= Append(ch, v)
         \end{conj}
  \]
Note how the 
   \ctindex{1}{nondeterminism!expressed by \mmath{\icmd{exists}}}{nondeterminism-exists}%
nondeterministic choice of $v$ is expressed mathematically by
existential quantification.  In general, nondeterminism of a system is
represented mathematically by existential quantification in the
next-state action.  It's important that you understand why this is
true, so you should understand why this formula describes a
``nondeterministic assignment to $ch$''.

Let's use TLC to check for errors.  The first thing to check is type
correctness.  The ``type'' of the variable $ch$ is \emph{sequence of
messages}.  Hence, the type-correctness invariant is:
\begin{display}
\begin{twocols}
$TypeOK == ch \in Seq(Msg)$
\midcol
\begin{verbatim}
TypeOK == ch \in Seq(Msg)
\end{verbatim}
\end{twocols}
\end{display}
 \popref{create-new-model}{Create a new model}.
Assign the value 4 to $N$, and assign to $Msg$ a set consisting of the
three \popref{model-value}{model values} $m_{1}$, $m_{2}$, and $m_{3}$
by selecting the \emph{Set of model values} option, typing the value
\begin{display}
\verb|{m1, m2, m3}|
\end{display}
and finishing by choosing the \emph{Leave untyped} option.
Enter $TypeOK$ as the invariant to check and run TLC\@.
It should find no error.

The specification does not distinguish between the elements of $Msg$.
This means that given any behavior that satisfies our specification,
permuting the values of $Msg$ the same way in all the states yields
another behavior that satisfies the specification.  In this case, we
say that the specification is 
 \ctindex{1}{symmetry of a spec under permutations of a set}{spec-symmetry}%
\emph{symmetric under permutations of the set}
$Msg$.  Knowing that a specification is symmetric under 
permutations of a set allows TLC to reduce the number of states that it
must explore.  We can tell TLC that our specification is symmetric
under permutations of $Msgs$ by checking the 
  \tindex{1}{symmetry set}%
\emph{Symmetry set} option when we assign the set of model values to
it.  Edit the substitution for $Msgs$ to do that and observe the
number of distinct states that TLC finds.  You will see that it finds
approximately $1/6$\tth\ as many states as it did before, because there
are 6 different permutations of the 3-element set $Msgs$.

When you tell TLC that a set is a symmetry set of the specification,
TLC doesn't check that it really is.  If it's not, this could cause TLC
to miss an error by not checking all the states it should.  

TLC can make use of symmetry only under a set of model values.  It
could not take advantage of symmetry if we had assigned a set of numbers
to $Msg$.

\begin{aquestion}{bbuf-answer -2}
What is the meaning of the bounded channel specification if $Msg$
is the empty set?  How does TLC confirm your answer?
\end{aquestion}
%
Our specification may not seem very interesting, since the sender
sends arbitrarily chosen messages that the receiver simply throws
away.  The Bounded Channel specification describes just the part of a
system used to send messages from one process to another.  A complete
specification of the system would describe how the messages are
created and what the receiver does with the ones it receives.
 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



\subsubsection{The \protect\tlaplus\ Translation} 

Run the PlusCal translator (from the \textsf{File} menu or by typing
\textsf{control+t}) and examine the \tlaplus\ translation.  The
definitions of the initial predicate $Init$ and next-state action
$Next$ are quite similar to the ones for the bounded channel
algorithm's PlusCal code.  They should be easy to understand, except
for the second conjunction of the $Producer$ action, which is the
translation of the PlusCal statement:
\begin{display}
\with\ $(v \in Msg)$ \{ $buf[p \,\%\, N] := v$ \}
\end{display}
Most readers probably expect this to be translated as:
\begin{display}
$\E v \in Msg : buf[p \,\%\, N]' = v$
\end{display}
While this formula specifies the new value of $buf[p \,\%\, N]$, it
doesn't specify the new value of $buf[i]$ for any $i$ other than $p
\,\%\, N$.  In fact, it doesn't even assert that the new value of
$buf$ is a function with domain $0\dd(N-1)$.  For example, the formula
can be satisfied by letting $buf'$ be a function whose domain is the
singleton set $\{p \,\%\, N\}$.  The correct translation of the
PlusCal statement is a formula
\begin{display}
$\E v \in Msg : buf' = f$
\end{display}
where $f$ is a function with the same domain as $buf$, such that
$f[p\,\%\,N] = v$ and $f[i]=buf[i]$ for all other values $i$ in the
domain of $buf$.  That function $f$ is written in \tlaplus\ as:%
      \ctindex{9}{except@\icmd{textsc}{except}}{except}%
\begin{display}
$[buf \EXCEPT ![p \,\%\, N] = v]$%
 \marginpar[.5]{\popref{except-notation}{What do the \textsc{except}
and the \,!\, mean?}}
\end{display}
We continue to ignore the definition of $Spec$ for a little while
longer.

You should now use TLC to check that you haven't made any mistakes.
Add the following type-correctness invariant to the module, after
the \tlaplus\ translation.
\begin{twocols}
\begin{notla}
TypeOK == /\ buf \in [0..(N-1) -> Msg]
          /\ p \in 0..(2*N-1)
          /\ c \in 0..(2*N-1)
\end{notla}
\begin{tlatex}
 \@x{\target{main-bbuf-typeok}{TypeOK} \.{\defeq} \.{\land} buf \.{\in} [ 0 \.{\dotdot} ( N \.{-} 1 )
 \.{\rightarrow} Msg ]}%
\@x{\@s{56.14} \.{\land} p \.{\in} 0 \.{\dotdot} ( 2 \.{*} N \.{-} 1 )}%
 \@x{\@s{56.14} \.{\land} c\@s{0.57} \.{\in} 0 \.{\dotdot} ( 2 \.{*} N \.{-} 1
 )}%
\end{tlatex}
%
%\target{main-bbuf-typeok}{
\midcol
\begin{verbatim*}
TypeOK == /\ buf \in [0..(N-1) -> Msg]
          /\ p \in 0..(2*N-1)
          /\ c \in 0..(2*N-1)
\end{verbatim*}
\end{twocols}
Create a small model that checks if $TypeOK$ is an invariant, and
run TLC on it.  TLC should find no error.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 XXXXXXXXXXXXXXXXXXXXXXXXXX









\newcommand{\estate}[5]{\left[\!\begin{array}{l@{\,\,}c@{\,\,}l}
                        p & = & #1 \\ c & = & #2 \\
                        buf & = & 0:>\tlastring{#3} % \,@@ 
                                         \\ & &
                                  1 :> \tlastring{#4}% \, @@ 
                                   \\ 
                            & &     2 :> \tlastring{#5}
                        \end{array}\!\right]}

\newcommand{\Estate}[7]{\left[\!\begin{array}{l@{\,\,}c@{\,\,}l}
                        in & = & \langle #6\!,\ldots\rangle \\ 
                        out & = & \langle #7\rangle \\
                        p & = & #1 \\ c & = & #2 \\
                        buf & = & 0:>\tlastring{#3} % \,@@ 
                                         \\ & &
                                  1 :> \tlastring{#4}% \, @@ 
                                   \\ 
                            & &     2 :> \tlastring{#5}
                        \end{array}\!\right]}

%
%
Now suppose $N=3$ and the set $Msg$ of messages consists of the set of
all one-character strings.  Consider the following possible
behavior of the algorithm, which I will call $\sigma$.  The behavior
$\sigma$ begins in an initial state with $buf[0]="a"$, $buf[1]="b"$,
$buf[2]="c"$, and continues by having the producer send the message
$"u"$, then send the message $"v"$, and the receiver then receive the
first message.  (I have used an \emph{ad hoc} method for writing the
value of the function $buf$; its meaning should be clear.)
\smallskip 
\begin{display}
\mbox{$\estate{0}{0}{a}{b}{c} \rightarrow 
 \estate{{ 1}}{0}{{u}}{b}{c} \rightarrow 
 \estate{{ 2}}{0}{u}{{v}}{c} \rightarrow 
 \estate{2}{{ 1}}{u}{v}{c} \rightarrow\;  \cdots
$}\s{-30}
\end{display}

\begin{display}
$\Estate{0}{0}{x}{y}{z}{"a"}{\,} \rightarrow 
 \Estate{{ 1}}{0}{a}{y}{z}{"b"}{\,} \rightarrow 
 \Estate{{ 2}}{0}{a}{b}{z}{"c"}{\,} \rightarrow 
 \Estate{2}{{ 1}}{a}{b}{z}{"c"}{"a"} \rightarrow\;  \cdots
$\s{-30}
\end{display}


%try
\renewcommand{\estate}[6]{
    \begin{noj}
     \left[\!\begin{array}{l@{\,\,}c@{\,\,}l}
                        p & = & #1 \\ c & = & #2 \\
                        buf & = & 0:>\tlastring{#3} % \,@@ 
                                         \\ & &
                                  1 :> \tlastring{#4}% \, @@ 
                                   \\ 
                            & &     2 :> \tlastring{#5}
                        \end{array}\!\right] \\
      \s{1.5}\rule{0pt}{1.5em}\ov{ch} = \langle #6 \rangle    
    \end{noj}}
%
\smallskip\noindent
Below each state in behavior $\sigma$, we now write the value of \ov{ch} 
in that state.
\smallskip
\begin{display}
\mbox{$\estate{0}{0}{a}{b}{c}{} \rightarrow 
 \estate{1}{0}{u}{b}{c}{\tlastring{u}} \rightarrow 
 \estate{2}{0}{u}{v}{c}{\tlastring{u}, \; \tlastring{v}}  \rightarrow 
 \estate{2}{1}{u}{v}{c}{\tlastring{v}} \rightarrow\;  \cdots
$}\s{-30}
\end{display}
\smallskip\noindent
We now erase the state and just keep the sequence of values of \ov{ch}.
%
\renewcommand{\estate}[6]{
      [\,\ov{ch} = \langle #6 \rangle\,]}
%
\smallskip
\[ \estate{0}{0}{a}{b}{c}{} \s{.5}->\s{.5} 
 \estate{1}{0}{u}{b}{c}{\tlastring{u}} \s{.5}->\s{.5} 
 \estate{2}{0}{u}{v}{c}{\tlastring{u}, \; \tlastring{v}}  \s{.5}->\s{.5} 
 \estate{2}{1}{u}{v}{c}{\tlastring{v}} \s{.5}->\s{.5}\;  \cdots
\]
\smallskip
%
\newcommand{\ovsig}{\ovs{\sigma}}%
Finally, we erase the overbars (replacing \ov{ch} by $ch$), to get the
following sequence that I will call \ovsig.
%
\renewcommand{\estate}[6]{
      [\,ch = \langle #6 \rangle\,]}
%
\smallskip
\[ \estate{0}{0}{a}{b}{c}{} \s{.5}->\s{.5} 
 \estate{1}{0}{u}{b}{c}{\tlastring{u}} \s{.5}->\s{.5} 
 \estate{2}{0}{u}{v}{c}{\tlastring{u}, \; \tlastring{v}}  \s{.5}->\s{.5} 
 \estate{2}{1}{u}{v}{c}{\tlastring{v}} \s{.5}->\s{.5}\;  \cdots
 \] \smallskip 
We say that the bounded buffer algorithm 
  \tindex{9}{implements under refinement mapping}%
  \tindex{9}{refinement mapping}%
  \ctindex{9}{mapping!refinement}{mapping-refinement}%
\emph{implements} the bounded
channel \emph{under the refinement mapping} $ch <- \ov{ch}$ iff for
every possible behavior $\sigma$ of the bounded buffer specification,
the sequence \ovsig\ constructed in this way is a possible behavior of
the bounded channel specification.  We say that $\sigma$ is
  \tindex{1}{mapped to by refinement mapping}%
\emph{mapped to} \ovs{\sigma} by this refinement mapping. 

Here's what we have just done.  Let a \emph{channel state} be an
assignment of a value to the variable $ch$, and let a \emph{buffer
state} be an assignment of values to the variables $p$, $c$, and
$buf$.  We informally defined \ovs{ch} to be a mapping from buffer
states to values---for example, it assigns to the buffer state
%
%
\renewcommand{\estate}[5]{\left[\!\begin{array}{l@{\,\,}c@{\,\,}l}
                        p & = & #1 \\ c & = & #2 \\
                        buf & = & 0:>\tlastring{#3} % \,@@ 
                                         \\ & &
                                  1 :> \tlastring{#4}% \, @@ 
                                   \\ 
                            & &     2 :> \tlastring{#5}
                        \end{array}\!\right]}
%
\[ \estate{2}{1}{u}{v}{c}\]
%
the value $<<"v">>$.  This defines a mapping from buffer states to
channel states, which maps any buffer state $s$ to the channel state
\ov{s} that assigns the value of \ov{ch} in state $s$ to the variable
$ch$.  This in turn defines a
mapping from any sequence 
 \[ s_{1} -> s_{2} -> s_{3} -> \cdots \]
of buffer states to the sequence
 \[ \ov{s_{1}} -> \ov{s_{2}} -> \ov{s_{3}} -> \cdots \]
of channel states.  For any sequence $\sigma$ of buffer states, we let
\ovsig\ be the corresponding sequence of channel states.  We say that
the bounded buffer algorithm implements the bounded channel under the
refinement mapping $ch <- \ov{ch}$ iff, for every behavior allowed by
the bounded buffer algorithm's specification, the behavior \ovsig\ is
allowed by the bounded channel's specification.

===============================================

\subsubsection{Showing Implementation} \xlabel{main:bbuf-impl-bchan}

Since TLC finds no counterexample, we can try to prove
$Spec_{B}=>\ov{Spec_{C}}$.  Let's subscript all defined formula names
by either $B$ or $C$ to indicate which module they come from.
We saw in 
  \rref{main}{\xlink{main:tl-refinement}}{Section~\xref{main:tl-refinement}}
that to prove $Spec_{B}=>\ov{Spec_{C}}$, we have to prove two things:
\begin{enumerate}
\item[R1.] $Init_{B}=>\ov{Init_{C}}$

\item[R2.] $Inv_{B} /\ Inv_{B}' /\ Next_{B} => [\ov{Next_{C}}]_{\ov{vars_{C}}}$
\end{enumerate}
for some invariant $Inv_{B}$ of the bounded buffer.  Let's start with R1.

Looking at the translations of the two PlusCal algorithms, and
remembering that $\ov{in}=in$ and $\ov{out}=out$, we see that:
%try
\begin{twocols}
\s{2}$
Init_B = \begin{conj}
         in = Input
         \\ out = << >>
         \\ buf \in [0\dd(N-1) -> Msg]
         \\ p = 0
         \\ c = 0
         \end{conj}
$
\midcol
$
\ov{Init_{C}} = \begin{conj}
         in = Input
         \\ out = << >>
         \\ \ov{ch} = << >>
         \end{conj}
$
\end{twocols}  
%try
Obviously, $Init_{B}$ implies the first two conjuncts of
$\ov{Init_{C}}$.  To see that it also implies $\ov{ch}=<<>>$,
% remember that if we picture the elements $buf[0]$, $buf[1]$,
% \ldots\,, $buf[2N-1]$ arranged in a circle, then 
% the $\ov{ch}$ is the sequence of elements starting from 
% $buf[c\%N]$ and going clockwise around the circle up to but
% excluding $buf[p\%N]$---for example, the sequence
%  \[ << buf[N-2],\; buf[N-1],\; buf[0],\; buf[1],\; buf[2]>> \]
% \popref{modular-arithmetic-fig-3}{in this picture}.  
recall that \ov{ch} is the sequence
  \[ <<\,buf[c\,\%\,N],\; buf[(c\oplus1)\,\%\,N],\; \ldots\,, \;
       buf[(p\ominus1)\,\%\,N]\,>>
 \]
of length $p\ominus c$.  Since $p=c$ implies $p\ominus c = 0$,
$Init_{B}$ implies $\ov{ch}=<<>>$, proving R1.  (A rigorous proof uses
the third conjunct of $Init_{B}$, which implies that $buf$
is a function with domain $0\dd(N-1)$.)

Let's now prove R2.  We expect that $Inv_{B}$ should imply
$TypeOK_{B}$.  We have defined \ov{ch} to be a sequence of length
$p\ominus c$.  Since $Spec_{C}$ implies that $ch$ is always a sequence
of length at most $N$, to prove $Spec_{C}$ we must be able to prove
that $p\ominus c$ is at most $N$.  Hence $Inv_{B}$ must imply 
$p\ominus c\leq N$.  It turns out that this is the only additional
property we need to prove R2, so we can define:
 \[ Inv_{B} == TypeOK_{B}\, /\ \, (p\ominus c\leq N)\]
Note that by definition of $\oplus$ and $TypeOK_{B}$, this implies
$p\ominus c \in 0\dd N$.

From the specifications, we see that
 \[\begin{noj3}
    \ov{Next_{C}} &\;=\;&\ov{Send_{C}}\, \/ \, \ov{Rcv_{C}} \V{.4}
    Next_{B} &\;\deq\;& Producer_{B} \, \/ \, Consumer_{B}
  \end{noj3}\]
We expect a $Producer_{B}$ step of the bounded buffer to implement a
$Send_{C}$ step of the bounded channel, and a $Consumer_{B}$ step of
the bounded buffer to implement a $Rcv_{C}$ step of the bounded
channel.  To prove R2, we therefore prove
\begin{enumerate}
\item $Inv_{B} /\ Inv_{B}' /\ Producer_{B} \implies \ov{Send_{C}}$

\item $Inv_{B} /\ Inv_{B}' /\ Consumer_{B} \implies \ov{Rcv_{C}}$
\end{enumerate}
% 
% \step{1}{}
% 
% \vspace{.5\baselineskip}%
% \step{2}{}
% 
% \vspace{.5\baselineskip}%
% \qedstep
% \vspace{.2\baselineskip}%
% \begin{proof}
% \pf\ By \stepref{1}, \stepref{2}, and the definitions of $Next_{B}$
% and $Next_{C}$.
% \end{proof}
% \end{proof}
% \end{display}
\popref{bbuf-r2}{Here is a partial proof of R2} containing
the proof of property~$1$.  It uses these definitions:
  \[\begin{noj}
    \ov{Send_{C}} == 
  \begin{conj}
  Len(\ov{ch}) # N \\
   \ov{ch}' = Append(\ov{ch}, IHead(in)) \\
    in' = ITail (in) \\
    out' = out
   \end{conj}\\
 Producer_{B} == 
    \begin{conj}
    p \ominus c # N \\
   buf' = [buf \EXCEPT ![p \% N] = IHead(in)] \\
   in' = ITail (in) \\
    p' = p \oplus 1 \\
   \UNCHANGED << out, c >>
    \end{conj}
    \end{noj}\]
The proof of property~2 is left as an exercise, as is the proof of
invariance of $Inv_{B}$.
\begin{question}
Complete the proof of R2 and show that $Inv_{B}$ is an 
inductive invariant of $Spec_{B}$.
\end{question}


XXXXXXXXXXXXXXXXXXXXXXXXXXXX

\documentclass[fleqn,leqno]{article}
\usepackage{hypertlabook}
\pdftitle{ASCII Text}
\fixverbatim
\begin{popup}
\begin{verbatim*}

\end{verbatim*}
\end{popup}
\makeasciipopup
