\section{The Asynchronous Case}

\begin{figure}[t]
\rule{8cm}{0.1 em}
{\small \begin{tabbing}
X\= LL: XX \= XX \= \kill
\\
\> \> $x,y$: {\it shared registers, initially} $y=0$; \\ \\
\> \> {\bf repeat forever} \\
\> \> 0b:\> $\ms{remainder\_exit}_i$ \\
\> \> L: \> $x$ := $i$; \\
\> \> 1:   \> {\bf if} $y \neq 0$ {\bf then goto} $L$; \\
\> \> 2:\> $y$ := 1; \\
\> \> 3:\> {\bf if} $x \neq i$ {\bf then goto} $L$;  \\ 
\> \> 4a: \> $\ms{critical\_entry}_i$ \\
\> \> 4b: \> $\ms{critical\_exit}_i$ \\
\> \> 5: \> $y$ := 0; \\
\> \> 0a:\> $\ms{remainder\_entry}_i$ \\
\> \> {\bf end repeat};
\end{tabbing}
} %%%% end of small
\rule{8cm}{0.1 em}
\caption{Algorithm 1: Lamport Style Mutual Exclusion -- 
Code for Process $i$.}
\label{fig: mutex1}
\end{figure}

%In this section, we present several results for the asynchronous case.
\absrem{ %%%%%%%%%%%%%%%%%%%% remove for absreatvct %%%%%%%%%%%
[[[(Formally,]]] the case where the system 
is a timed automaton with the boundmap assigning
the interval $[0,\infty]$ to all the processes.)
The user automata also have this interval associated with the critical
region.  Note that the user automata will always have this interval,
even later in the paper when the system has more interesting boundmap
conditions.

\subsection{Impossibility of Mutual Exclusion and Deadlock-Freedom,
with Fewer than $n$ Registers}
} %%%%%%%%%%%%%%%%%%%% remove for absreatvct %%%%%%%%%%%

The following theorem is due to Burns and Lynch \cite{BL}.
\begin{theorem}
\label{thm: BL}
There is no asynchronous algorithm providing mutual exclusion with
deadlock-freedom for $n \geq 2$ processes, using fewer than $n$ shared
read/write registers.
\end{theorem}

\absrem{ %%%%%%%%%%%%%%%%%%%
\subsection{A $2$ Register Algorithm 
for Mutual Exclusion and Weak Deadlock-Freedom}
} %%%%%%%%%%%%%%%%%%

Since Theorem~\ref{thm: BL} rules out asynchronous solutions 
for deadlock-free mutual exclusion with fewer than $n$ 
shared registers, 
we will consider timing-based algorithms. 
A natural requirement for a timing-based mutual exclusion algorithm 
is that mutual exclusion and weak deadlock-freedom be guaranteed
always, even if the timing assumptions are violated.
We thus begin our development by showing that there 
exists an asynchronous 2-register algorithm for $n \geq 2$, 
giving mutual exclusion and weak deadlock-freedom.
%[[[
This algorithm, which we call Algorithm 1,
has a structure similar to some described by Lamport in \cite{Lamport-mutex}.
%]]]
%[[[Joanne ask Nancy: This should be the 86 paper. ???]]]
The algorithm uses two shared registers, $x$ and $y$.
Each process $P_i$ writes its index $i$ into $x$, to indicate
that it wishes to enter the critical region, and then 
checks register $y$ 
to see if it might have just overwritten 
the value of some other process $P_j$ that is attempting to enter.
If there is such a process (i.e., if $y=1$), $P_i$ gives up, otherwise, 
it sets $y$ for other processes and tests $x$ to see if 
it has not been overwritten by some later process $P_j$ attempting 
to enter the critical region.
If $x$ is still set to $i$, $P_i$ enters the critical region,
setting $y$ to $0$ before returning to the remainder region.

The code is presented in Figure \ref{fig: mutex1}, in a standard
psuedo-code style. Translating this code into
timed automata is a straightforward but tedious exercise.  
The other algorithms in this paper are also presented in the same style.

%[[[comment: Nancy, I changed the cs and rm code line titles in
%the code, also, no need for x to initially be 0]]]
To aid in the proof, we 
%[[[
describe the program states as a combination of
{\it program counter} values as above, 
local variable values and shared register values.
%]]]
In any state of the algorithm, we define: 
\begin{description}
\item[$F1$:] the set of process indices $i$ such that 
$x = i$ and $\ms{pc}(i) = 2$,
\item[$F2$:]
the set of process indices $i$ such that 
$x = i$ and $\ms{pc}(i) = 3$,
\item[$CR$:] the set of process indices $i$ such that 
$\ms{pc}(i) \in \{ 4a, 4b, 5 \}$.
\item[$RM$:]
the set of process indices $i$ such that 
$\ms{pc}(i) \in \{ 0a, 0b \}$.
\end{description}

We prove the following lemma by induction on the length of the execution.
\begin{lemma}
\label{invt-alg1}
The following are true in any reachable state of Algorithm 1.
\begin{description}
\item[$I1:$]  \label{invt-alg1-1}
       $|F1| + |F2| + |CR| \leq 1$. 
\item[$I2:$]  If $|F2| + |CR| > 0$ then $y = 1$. 
\item[$I3:$]  \label{invt-alg1-2} 
       If $y = 1$ then some process $i$ is not in $RM$.
\end{description}
\end{lemma}

\absrem{ %%%%%%%% removed from abstract %%%%%%%%%%%
\begin{proof}
[[[ Comment: Nancy, we need a line in the model section that says that 
since we use atomic read write registers, its enough to 
think of the execution as a sequence of none overlapping 
{\it operations}, this or something that captures it 
in terms of the global automaton.]]]

By induction on the length of an execution.
Initially $I1$, $I2$ and $I3$ hold vacuously since all processes 
are in the remainder ($pc(i)=0$), and $y=1$.
We assume that the invariants hold in some reachable state $s$, 
and for the inductive step, go over all the possible 
operations (or operation and $pc$ change ) $\pi_i$ of a process $i$,
leading from $s$ to a new state $s'$ in 
a given execution. We refer to these operations
by their relative line numbers in the code. 
First note that in any state, there is at 
most one process $i$ for which $x=i$, so $|F1|$ + $|F2|$ is always 
equal to $1$.
\begin{description}
\item[{\rm Line~L}]
$CR$ remains the same, and $|F1|$ and $|F2|$ can only decrease,
so $I1$ holds in $s'$. Since
$y$ remains unchanged, and $pc(i)=1$ following the operation, 
$I2$ and $I3$ hold.
\item[{\rm Line~1}]
$I3$ holds since in $s'$ $pc(i)$ is either $L$ or $2$.
If $x \neq i$ both $I1$ and $I2$ hold immediately.
The only state change is in $pc(i)$. 
If $x=i$ in $s$ then it was the case that $|F1|+|F2|=0$.
From $I2$ we thus have that in $s$ if $|CR|>0$ then $y=1$.
If $y$ was $1$, then $i$ reads $y=1$ and in $s'$ $i$
changes to $pc(i)=L$, 
implying that $I1$ and $I2$ continue to hold since 
$F1$ and $F2$ remain unchanged. 
If $y$ was $0$, process  $i$ will read $y=0$
and in $s'$ $pc(i)=2$, implying $|F1|=1$ and $|F2|=0$.
Since by $I2$ this implies $|CR|=0$ in $s$,  $|F1| + |F2| + |CR| \leq 1$
and $I1$ and $I2$ also hold. 
\item[{\rm Line~2}]
$I2$ holds since in $s'$ $y=1$ and $I3$ holds since $pc(i)=3$.
If $x \neq i$ in $s$, $I1$ also holds immediately.
If $x=i$, then in $s$ $|F1|=1$ and $|F2|=0$, and in $s'$
$|F1|=0$ and $|F2|=1$, and $I1$ holds.
\item[{\rm Line~3}]
$I3$ holds since in $s'$ $pc(i)$ is either $L$ or $4a$.
If $x \neq i$ in $s$, then $F1$ and $F2$  and $CR$ remain unchaged 
implying that $I1$ and $I2$ hold.
If $x=i$, then in $s$ $|F1|=0$, $|F2|=1$, and $|CR|=0$, and in $s'$
$|F1|=0$, $|F2|=0$ and $|CR|=1$, so $I1$ holds.
By $I2$ and $|F2|=1$ it must be that $y=1$ in $s$ and remains so 
in $s'$, implying $I2$.
\item[{\rm Line~4 (a and b)}]
$I3$ holds since in $s'$ $pc(i)$ is $4b$ or $5$.
Both invariants hold immediately.
\item[{\rm Line~5}]
$I3$ holds since in $s'$ $y=0$.
Since $pc(i)=4b$ in $s$, it follows by $I1$ that $|CR|=1$ and by $I2$ 
that  $|F1|+|F2|=0$. Thus, since in $s'$ $pc(i)=0a$,
$F1$ and $F2$ remain unchanged,
and $|CR|=0$, implying that both $I1$ and $I2$ hold.
\item[{\rm Line~0a}]
All invariants hold immediately.
\item[{\rm Line~0b}]
Since in $s'$, $i$ is not in $RM$, $CR$ is unchanged and $|F1|$ and $|F2|$ 
can only decrease, all the invariants hold.
\end{description}
\end{proof}
} %%%%%%%%%%%%%% end remove %%%%%%%%5
By $I1$ of Lemma \ref{invt-alg1} we have:
\begin{lemma}
\label{Lemma: Lamport ME}
Algorithm 1 has the mutual exclusion property.
\end{lemma}

\absrem{ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{proof}
By $I1$ of Lemma \ref{invt-alg1}.
\end{proof}
} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%[[[I put the explicit names for the algorithms back in the statements
%of the results.  Naming them by the figure numbers does't work right!]]]

The following lemma follows from $I3$ and the fact that the executing the 
exit region takes a bounded nember of steps.


\begin{lemma}
Algorithm 1 is weakly deadlock-free.
\end{lemma}

\absrem{ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{proof}
[[[If some process enters when everyone else is in the remainder
region,  then $I3$ of Lemma \ref{invt-alg1} %part \ref{invt-alg1-2} 
implies that  $y = 0$ at that time, 
which allows the process to proceed directly to the critical region.
The exit region is wait-free, so the second part of this claim 
follows immediately.]]]
\end{proof}
} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5

%[[[
We now show that Algorithm 1
optimal in terms of the number of registers.
%]]]

\absrem{ %%%%%%%%%%%%%%%%%%%%%%
%\subsection{Impossibility of Mutual Exclusion and Weak Deadlock Freedom,
%with $1$ Register}
} %%%%%%%%%%%%%%%%%%%%%%%%
\begin{lemma}
\label{lemma:read-write-me-wda-1}
%[[[
In any (timed or asynchronous) algorithm 
providing mutual exclusion and weak deadlock-freedom for $n \geq 2$
processes,
using a single shared register, 
every process that moves from its remainder to its critical region 
must perform at least one read followed by a write. 
%]]]
\end{lemma}
The proof follows since if a process does not write, other processes cannot
tell that it has left the remainder, and if it does not read, it cannot tell 
if any one of them left the remainder. Both cases would lead to a violation of mutual exclusion.
\absrem{ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{proof}
Consider any two processes, say  $1$ and $2$, and let us show that 
process $1$ must have read and then written the register.
From the system start state $s$, by the 
{\em weak deadlock-freedom} property, either process
must be able, on its own, to complete an execution leading to a 
state in which it is in the 
critical region (call these executions $e_1$ and $e_2$ respectively
[[[Comment: Nancy, execution fragments?]]]).

We claim that in $e_1$ in
which process $1$ enters and proceeds to enter the critical
region in state $s'$, it must have written the register.
If it did not, then $s$ and $s'$ differ only in 
the internal state of process $1$, and extending 
$e_1$ by $e_2$ yields an execution 
in which process $2$ behaves just as if it were
on its own, resulting in a state in which both
processes are in the critical region,
a violation of {\em mutual exclusion}.
So process $1$ must write the register in $e_1$.

We further claim that in $e_1$ 
it must have read the register before writing it.
If it did not, then as above
executing $e_2$ followed by $ e_1$ generates an 
execution which process $1$ cannot distinguish 
from the execution of only $e_1$, resulting in  
a state in which both
processes are in the critical region.
So process $1$ must read the register in $e_1$ prior to writing it.
\end{proof}
} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{theorem}
\label{theorem:asynch-imposs-me-wda-1}
There is no asynchronous algorithm providing mutual exclusion 
with weak deadlock-freedom for $n \geq 2$ asynchronous processes,
using only one shared read/write register.
\end{theorem}

\begin{proof}
%[[[I reordered the proof slightly.]]]
Assume by way of contradiction that there exists a one 
register algorithm for the problem.
Consider two processes, say  $1$ and $2$.  
From the system start state $s$, by the 
{\em weak deadlock-freedom} property, either process
must be able, on its own, to complete an execution leading to a 
state in which it is in the critical region;
call these executions $e_1$ and $e_2$ respectively.
By Lemma~\ref{lemma:read-write-me-wda-1},
each of the two processes must write the register during its execution.

Now we construct a bad execution.
Run process $1$ in $e_1$ just until the first state $s'$ at which it is
about to write the register, and let it pause without doing so.
States $s$ and $s'$ differ only in the internal state of process $1$.
Then extend the execution by $e_2$, in which
process $2$  behaves just as if it were
on its own, eventually entering the critical region.
Next, process $1$ continues its execution of $e_1$, 
first performing its write
to the register, which overwrites whatever process $2$ has written.
Following this operation, the state of the system 
differs from the corresponding state in $e_1$ only in the internal 
state of process $2$, and so process $1$ goes
critical,  violating {\em mutual exclusion}.
This is a contradiction.
\end{proof}

\absrem{ %%%%%%%%%%%%% Remove from Abstract %%%%%%%%%%%%%
[[[Comment: Nancy, I would leave this to the conclusions
section only. Faith observed that we could strengthen the WDA assumption to a
WDA(k) assumption, where $k$ is any positive integer.
This strengthened assumption would say that $k$-bounded concurrency
still guaranteed progress (our definition corresponds to $k = 1$).
Then it appears that the Burns-Lynch impossibility proof extends
to $k$ variables.  I have no idea whether the algorithm above extends
correspondingly to a $k+1$-variable algorithm.
Probably make this a remark here, and an open question in the
conclusions section.]]]

[[[Comment: I agree, we should make this remark in the 
proof section of the impossibility result. Faith also suggested that we make a remark, here or somewhere,
about where the 2-variable impossibility proof breaks down, with just
the WDA assumption.
The key is in constructing a spine involving 2 processes.
Inductively, we are able to bring them in to nullify two variables.
But then when we want to let them write,
then send them back to the remainder region, bring
them back in, etc., we don't have the right progress assumption to do
this.  (They are aware of each other's overlapping execution.)]]]
} %%%%%%%%%%%%% End of Remove from Abstract %%%%%%%%%%%%%
