% timed
\section{Timing-Based Exclusion}
\begin{figure}[t]
\rule{8cm}{0.1 em}
{\small
\begin{tabbing}
X\= LL: XX \= XX \= \kill
\\
\> \> $x$: {\it shared register initially} $0$; \\
\> \> {\it delay}: {\it positive integer constant}; \\ \\
\> \> {\bf repeat forever} \\
\> \> 0b:\> $\ms{remainder\_exit}_i$ \\
\> \>  L:  \> {\bf if} $x \neq 0$ {\bf then goto} $L$; \\
\> \> 1:\> $x$ := $i$; \\
\> \> 2: \> {\it pause\/}({\it delay}); \\
\> \> 3: \> {\bf if} $x \neq i$ {\bf then goto} $L$; \\
\> \> 4a: \> $\ms{critical\_enter}_i$ \\
\> \> 4b: \> $\ms{critical\_exit}_i$ \\
\> \> 5:\> $x$ := 0; \\
\> \> 0a:\> $\ms{remainder\_enter}_i$ \\
\> \> {\bf end repeat};
\end{tabbing}
} %%%%%%% end of small
\rule{8cm}{0.1 em}
\caption{Algorithm 2: Fischer's Timed Mutual Exclusion -- 
Code for Process $i$.}
\label{fig: mutex2}
\end{figure}

In this section, we consider the {\em real-time} version of the
problem,
where we assume bounds in the interval $[c_1, c_2]$ for the time
between successive steps of a process, when it is in its trying or
exit region.
We assume that $0 < c_1 \leq c_2 < \infty$. 
Let $C = c_2/c_1$; $C$ is a measure of the {\em timing uncertainty}.
Define a process $i$ to be {\em slow} (respectively, {\em fast})
in an execution or execution fragment if the time for
any step when the process is in its trying or exit region is exactly
$c_2$ (resp., $c_1$).

\subsection{A $1$ Register Algorithm for Mutual Exclusion and Deadlock
Freedom}
\label{section: Simple Timing-Based Algorithm}

We begin by presenting, in Figure~\ref{fig: mutex2},
a timing-based mutual exclusion algorithm due to Mike Fischer 
\cite{Fischer-mutex}; we call this Algorithm 2.
Algorithm 2 has the property that if the timing constraints are met,
and the value of the $\mbox{\it delay}$ parameter is chosen to be
strictly greater than the timing uncertainty $C$, then 
mutual exclusion and deadlock-freedom are guaranteed. 
However, it has the drawback that
if the constraints are not met, then many processes may
enter the critical region concurrently.

The key idea behind Algorithm 2 is to delay each process
$i$ for a period greater than $C \cdot c_1$ 
after it has written $x$ in Line~1 and before testing it in 
Line~3. Thus, by the time process $i$ has reached
Line~3, any process $j$ that has passed the test in Line~L
and might overwrite $x=i$ with $x=j$, has already done so since 
$C \cdot c_1 \geq c_2$, the longest time such a step might take. 
If $i$ reads $x = i$ in Line~3, it can safely enter the 
critical region, since all other processes are either before 
Line~L and will not pass it, or after Line~1 with their index in 
$x$ overwritten by process $i$, so they will fail the test on Line~3.
To implement the delay, 
the procedure {\it pause\/}({\it delay}) causes the process to delay
by some number of steps, where a {\it delay} of $1$ 
means skipping no steps at all, and 
a {\it delay} of $k$ amounts to doing $k-1$ dummy steps. 

%[[[
We need to expand the discussion of the delay to be more precise.
Specifically, let's think of pause(k) as a shorthand for including 
$(k - 1)$ lines of code, each a no-op.
Here, let us assign program counter values 
$2.1, 2.2, \ldots, 2.(k-1)$ to those $(k-1)$ lines.
This convention will require rewriting some of the invariants and
proofs below.  Victor did things a little differently, with a single
longer step, but that's further from what our basic model allows.
%]]]

%[[[
Some rewriting below in the declarations.
%]]]


%[[[
We need to discuss the optimization I suggested for the algorithms --
replacing the no-ops by explicit tests such as appear in statement 3.
%]]]

%[[[
Let Algorithm~2' be the same as Algorithm~2 but asynchronous
(i.e.,with all the process' classes having bounds $[0,\infty)$).

We now prove the correctness of the algorithm.
Similarly to before, define:

CR: the set of process indices $i$ such that $pc(i) \in \{ 4a, 4b, 5 \}$.

In the following, we write $pc(i) = 2$ as a convenient shorthand for
$pc(i) \in \{ 2.1, \ldots 2.(delay - 1) \} $.

\begin{lemma}
\label{invt-alg2'-asynch}
Then in any reachable state of Algorithm~2':
\begin{quote}
If $x = i$, $i \in \{1..n\}$
then $pc(i) \in \{ 2, 3, 4a, 4b, 5\}$.
\end{quote}
\end{lemma}

\begin{proof}
By induction on the length of the execution.
Initially the claim holds vacuously since $x = 0$.
For the inductive step,
assume the claim holds in any reachable state $s'$, 
and consider steps of the form $(s',\pi,s)$.
Suppose that $\pi$ is an action of process $i$. 
Fix any $j \in \{ 1, \ldots n \}$, and suppose that $s.x = j$.
As before, we consider cases based on line numbers in the code. 

\begin{description}
\item[{\rm Lines~0a,0b,L}:]
Then by the code, we also have $s'.x = j$.
By the claim for $s'$, it follows that
$s'.pc(j) \in \{ 2, 3, 4a, 4b, 5\}$.
Since $s'.pc(i) \in \{ 0a, 0b, L \}$, this implies that $j \neq i$.
Therefore, $s.pc(j) = s'.pc(j)$,
so $s.pc(j) \in \{ 2, 3, 4a, 4b, 5\}$, as needed.

\item[{\rm Line~1}:]
By the code, it must be that $j = i$.
Since $s.pc(i) = 2$, the claim follows.

\item[{\rm Line~2}:]
Then by the code, we also have $s'.x = j$.
By the claim for $s'$, it follows that
$s'.pc(j) \in \{ 2, 3, 4a, 4b, 5\}$.
If $j = i$ then the claim follows from the fact 
that $s.pc(i) \in \{ 2, 3 \}$.
On the other hand, if $j \neq i$, the claim follows since
$s.pc(j) = s'.pc(j)$.

\item[{\rm Line~3}:]
Then by the code, we also have $s'.x = j$.
By the claim for $s'$, it follows that
$s'.pc(j) \in \{ 2, 3, 4a, 4b, 5\}$.
If $j = i$ then $s'.x = i$, so that $s.pc(j) = 4a$
and the claim follows.
On the other hand, if $j \neq i$, the claim follows since
$s.pc(j) = s'.pc(j)$.

\item[{\rm Lines~4a,4b}:]
Then by the code, we also have $s'.x = j$.
By the claim for $s'$, it follows that
$s'.pc(j) \in \{ 2, 3, 4a, 4b, 5\}$.
If $j = i$ then the claim follows from the fact that 
$s.pc(j) \in \{ 4b, 5 \}$.
On the other hand, if $j \neq i$, the claim follows since
$s.pc(j) = s'.pc(j)$.

\item[{\rm Line~5}:]
Then $s.x = 0$ and the claim follows immediately.
\end{description}

%[[[
This proof is too repetitious.  It should be condensed, some cases
combined.
%]]]
\end{proof}

%[[[
I am modifying the following proof to take account of the new way of
splitting up the pause statement.
We still lhave ftime(i) and ltime(i) as indicated below.
However, now I will just assign them the values $c_1$ and $c_2$ when
control reaches statement 2.1.
This requires a change to the invariants, namely, splitting the old I2
into the new I2 and I3.
%]]]

[[[Nancy comment: 
Now some assertions for the {\em timed} version of the algorithm.
These will be in the style of those I did with Hagit, 
involving state components that predict the time until the
following step.
Here, the state components involving time are exactly:
$\ms{now}$, representing the current real time, and
for each process $i$, $\ms{ftime}(i)$ and $\ms{ltime}(i)$,
representing the first and last (absolute) time that the next step of
process $i$ is allowed to occur.
For now, I am not considering the individual steps within the pause
statement, but just making the prediction times for the completion of
that statement equal to the bounds for the entire pause statement to
execute.
E.g., when control first reaches point 2, I set $\ms{ftime} =
\ms{delay} c_1$ and $\ms{ltime} = \ms{delay} c_2$.
Before the ltime elapses, the algorithm must do the statement at line
3, thereby passing to line 4.
Come to think of it, this means that the way I am modeling it, the pc
value is never actually at 3 - it just goes directly from 2 to 4 after
the time specified in the statement.  Need to fix this later.
The invariants below are adapted from the Abadi-Lamport REX paper,
``An Old-Fashioned Recipe for Real Time''.
Note that the algorithm there is slightly different, so the invariants
and proof need to be redone in our setting.

Note that your extra $x = i$ condition, which you stated in a funny
operational way previously, is now part of the following invariant
assertion.]]]

To aid in the main proof, let us 
define several state components involving time:
$\ms{now}$, representing the current real time, and
for each process $i$, $\ms{ftime}(i)$ and $\ms{ltime}(i)$,
representing the first and last (absolute) time that the next step of
process $i$ is allowed to occur.
We prove the following by induction on the number of steps in an
execution.
Note that the only executions that are considered here are those in
which the timing assumptions are satisfied; the timing assumptions are
required to guarantee these key properties.

\begin{lemma}
\label{invt-alg2-1}
If $\ms{pc}(i) \notin \{ 0b, 4b \}$ 
then $\ms{ltime}(i) \leq \ms{now} + c_2$.
\end{lemma}

\begin{proof}
By the construction of the augmented automaton.
\end{proof}

%[[[
Give nice thanks to Victor here.
%]]]

\begin{lemma}
\label{invt-alg2-2}
In any reachable state of Algorithm 2, the following are true.
\begin{description}
\item[$I1$:]  If $\ms{pc}(i) = 2.d$, $x = i$ and $\ms{pc}(j) = 1$ 
              then $\ms{ltime}(j) < \ms{ftime}(i) + (delay - d) c_1 $.
\item[$I2$:]  If $\ms{pc}(i) = 3$, $x = i$ and $\ms{pc}(j) = 1$ 
              then $\ms{ltime}(j) < \ms{ftime}(i)$.
\end{description}
\end{lemma}

\begin{proof}
By induction on the length of an execution.
The basis, length $0$, is immediate.
Suppose $s'$ is a reachable state of the algorithm, and the claims are
true in $s'$.
Suppose that $(s',\pi,s)$ is a step of the algorithm.
Now $\pi$ can be either an action of a process, or can be a
time-passage action.
But time-passage steps do not affect the truth of either of the
claims, so we can assume that $\pi$ is an action of a process, say
process $k$.
If $k \notin \{ i, j \}$ then the claims for $s$ follow immediately
from those for $s'$, so assume that $k \in \{ i, j \}$.

As before, we consider cases based on lines in the code.

\begin{description}
\item[{\rm Lines~0a,0b,3,4a,4b,5}:]

Then $s.pc(k) \in \{ 0a, 0b, L, 4a, 4b, 5\}$.
Since $k$ is either equal to $i$ or $j$, both claims are true
vacuously.

\item[{\rm Line~L}:]

If $s'.x \neq 0$ then $s.pc(k) = L$, which means that 
either $s.pc(i) = L$ or $s.pc(j) = L$; then both claims are
true vacuously.
On the other hand, if $s'.x = 0$, then also $s.x = 0$, 
so again both claims are true vacuously.

\item[{\rm Line~1}:]

Then $s.x = k$.
If $k \neq i$ then $s.x \neq i$ and both claims are true vacuously, so
assume that $k = i$ (and hence $s.x = i$).

Since $\ms{delay} > C = c_2/c_1 \geq 1$, we have that $\ms{delay} \geq
2$.
This implies that $s.pc(i) = 2.1$.
It follows that $I2$ is vacuously true in $s$.
We consider $I1$.
Suppose that $s.pc(j) = 1$.
Then $s.\ms{ltime}(j) \leq s.\ms{now} + c_2$, by Lemma \ref{invt-alg2-1}.
Also, $s.\ms{ftime}(i) = s.\ms{now} + c_1$,
so that $s.\ms{ltime}(j) \leq s.\ms{ftime}(i) - c_1 + c_2$ \\
$= s.\ms{ftime}(i) + (c_2 - c_1)$.
Since $\ms{delay} > c_2/c_1$, 
we have $c_2 - c_1 < (\ms{delay} - 1)c_1$.
Therefore, $s.\ms{ltime}(j) < s.\ms{ftime}(i) + (\ms{delay} - 1)c_1$,
as needed.

\item[{\rm Line~2.e}, $1 \leq e < \ms{delay} - 1$:]

Then $s.pc(k) = 2.(e+1)$.
Since $k \in \{ i, j \}$, $I2$ is vacuously true in $s$.
We consider $I1$.
If $k = j$ then $s.pc(j) = 2.(e + 1)$,
and $I1$ is vacuously true in $s$, so assume that $k = i$.

Suppose that $s.pc(j) = 1$ and $s.x = i$.
Then $s'.pc(j) = 1$ and $s'.x = i$.
Since $s'.pc(i) = 2.e$ and $I1$ holds in $s'$, it follows that
$s'.\ms{ltime}(j) < s'.\ms{ftime}(i) + (\ms{delay} - e) c_1$.
We must show that
$s.\ms{ltime}(j) < s.\ms{ftime}(i) + (\ms{delay} - (e+1)) c_1$.
But $s.\ms{ltime}(j) = s'.\ms{ltime}(j)$,
$s'.\ms{ftime}(i) \leq s'.\ms{now}$,
$s'.\ms{now} = s.\ms{now}$,
and $s.\ms{now} = s.\ms{ftime}(i) - c_1$, all by the construction of
the augmented automaton.
Substituting, we get the desired inequality.

\item[{\rm Line~2}.$(\ms{delay} - 1)$:]

Then $s.pc(k) = 3$.
Since $k \in \{ i, j \}$, $I1$ is vacuously true in $s$.
We consider $I2$.
If $k = j$ then $s.pc(j) = 3$, and $I2$ is vacuously true in $s$, so
assume that $k = i$.

Suppose that $s.pc(j) = 1$ and $s.x = i$.
Then $s'.pc(j) = 1$ and $s'.x = i$.
Since $s'.pc(i) = 2.(\ms{delay} - 1)$ and $I1$ holds in $s'$, 
it follows that
$s'.\ms{ltime}(j) < s'.\ms{ftime}(i) + c_1$.
We must show that
$s.\ms{ltime}(j) < s.\ms{ftime}(i)$.
But $s.\ms{ltime}(j) = s'.\ms{ltime}(j)$,
$s'.\ms{ftime}(i) \leq s'.\ms{now}$,
$s'.\ms{now} = s.\ms{now}$,
and $s.\ms{now} = s.\ms{ftime}(i) - c_1$, all by the construction of
the augmented automaton.
Substituting, we get the desired inequality.
\end{description}

\end{proof}

\begin{lemma}
\label{invt-alg2-3}
In any reachable state of Algorithm 2, the following is true:
\begin{description}
\item[$I3$:]
       If $i \in CR$ then 
       \begin{enumerate}
       \item $x = i$, and 
       \item for all $j$, $\ms{pc}(j) \neq 1 $.
       \end{enumerate}
\end{description}
\end{lemma}

(Note that this invariant does not involve timing.)

\begin{proof}
By induction on the length of the execution.
The basis, length $0$, is immediate.
Suppose $s'$ is a reachable state of the algorithm, and the claim is
true in $s'$.
Suppose that $(s',\pi,s)$ is a step of the algorithm.
Again, $\pi$ can be either an action of a process, or can be a
time-passage action.
But time-passage steps do not affect the truth of the claim,
so we can assume that $\pi$ is an action of a process, say process $k$.
As before, we consider cases based on lines in the code.

\begin{description}
\item[{\rm Lines~0a,0b,2,4a,4b}:]

Then no changes are made that can falsify the claim.

\item[{\rm Line~L}:]

If $s'.x \neq 0$ then no changes are made that can falsify the claim,
so suppose that $s'.x = 0$.
Then $s'.x$ is unequal to any process index, so by $I3$ applied to
$s'$,
we have $s'.CR = \emptyset$.
Then also $s.CR = \emptyset$, which implies that $I3$ is vacuously
true in $s$.

\item[{\rm Line~1}:]

Then $s'.pc(k) = 1$, so by $I3$ applied to $s'$, we have that $s'.CR =
\emptyset$.
Then also $s.CR = \emptyset$, which implies that $I3$ is vacuously
true in $s$.

\item[{\rm Line~3}:]

(Here is where the timing is used.)
If $s'.x \neq k$ then no changes are made that can falsify the claim,
so suppose that $s'.x = k$.

Consider $i \in s.CR$.
If $i \neq k$ then $i \in s'.CR$, so by $I3$ applied to $s'$ we have
$s'.x = i$.  This is a contradiction, so suppose that $i = k$.
Then $s.x = s'.x = k = i$, satisfying the first part of $I3$ for $s$.
For the second part, suppose that $s.pc(j) = 1$.
Then $s'.pc(j) = 1$, $s'.pc(k) = 3$ and $s'.x = k$.
By $I2$ applied to $s'$, we have that $s'.\ms{ltime}(j) <
s'.\ms{ftime}(k)$. 
But this contradicts the fact that the operation of $k$ is enabled in
$s'$.
Therefore, we cannot have $s.pc(j) = 1$, which shows the second part
of $I3$.

\item[{\rm Line~5}:]

Then $k \in s'.CR$, so by $I3$ applied to $s'$, we have $s'.x = k$.
Thus again by $I3$ applied to $s'$, we see that no process other than
$k$ is in $s'.CR$.
Then since $s.pc(k) = 0a$ and no other processes move, we see that
$s.CR = \emptyset$.
This implies that $I3$ is vacuously true in $s$.

\end{description}
\end{proof}

Now we can show mutual exclusion.

\begin{lemma}
\label{Lemma: Fischer ME}
Algorithm 2 has the mutual exclusion property.
\end{lemma}

\begin{proof}
By Lemma \ref{invt-alg2-3}, invariant I3.
\end{proof}

Next, we argue deadlock-freedom.

\begin{lemma}
\label{alg2-DA}
Algorithm 2' is deadlock-free.
\end{lemma}

\begin{proof}
[[[An operational proof here.]]]

[[[Fix the deadlock-freedom definition so it doesn't mention
reachability, but just states occurring within the execution.  N.]]]

Consider any execution of the algorithm, and consider any state $s$ in
the execution in which some process 
is in the trying region and no process is in the critical region
(Line $4b$), 
and assume by way of contradiction that 
no process goes critical after that state.
Since there are at most $n$ processes,
after some state $s'$ in this execution, there are no processes
in $CR$, and no additional processes enter the trying region.
We can without loss of generality
assume this holds throughout the execution fragment.

We claim that a state $s'''$ is eventually reached such that from that
state on, $x$ is always equal to $i$ for some fixed process index $i$.
Since there is at least one process in the trying region 
and all the processes in the trying region keep taking steps,
and never reach the critical region, 
it must be that they all repeatedly execute Line~$L$.
Then if any process $i$ ever reads $x = 0$ in Line~$L$, 
it sets $x=i$ in Line~1.
Since Line~5 is never executed, there is a state $s''$ following which
in every state, $x \neq 0$.
But any process that executes Line~L following $s''$,
remains in Line~$L$, implying that there is a state $s'''$ following 
which Line~1 is never executed
(i.e., there are no further assignments to $x$).
Since $x \neq 0$, it must be that $x=i$ for some $i \in \{1..n\}$.

Lemma \ref{invt-alg2'-asynch} implies
that process $i$ has $\ms{pc}(i) \in \{ 2, 3, 4a, 4b, 5\}$ in $s'''$.
But we have assumed that no process has $\ms{pc}(i) \in \{ 4a, 4b, 5\}$
following $s$, so it must be that $\ms{pc}(i) \in \{ 2, 3 \}$.
But then there is nothing stopping $i$ from 
reading $x=i$ in Line~3, and executing the critical
region, a contradiction.
\end{proof}

The following is an almost tight upper bound on the time $b$ for any
process to enter the critical region.
(It can be made tighter by a slight modification to
Algorithm 2, which we will describe in the full version 
of the paper.)

\begin{lemma}
\label{lemma: fischer lb}
[[[Suppose that $\ms{delay} \leq C + 1$.]]]
Then Algorithm 2 has an upper bound of $(2C + 7) c_2$.
\end{lemma}

\begin{proof}
Consider any execution of the algorithm,
and consider any state $s$ of that execution in which some process
is in the trying region and no process is in the critical region
(Line $4b$).
By Lemma~\ref{alg2-DA}, there must be a process 
that executes the critical region next; let $i$ be the index of this
next process.
Let $\alpha$ be the execution fragment (note:  this is of the
augmented automaton) starting from $s$ and ending with the first state
at which $i$ is in the critical region
(i.e., at line $4b$), and let $u$ be the final state of $\alpha$.
Suppose the stated bound does not hold, in the given execution.
Then $u.\ms{now} > s.\ms{now} + (2C + 7) c_2$.
Define $s'$ to be the last state in $\alpha$ with
$s'.\ms{now} \leq s.\ms{now} + c_2$,
and define $\alpha'$ to be the suffix of $\alpha$ starting with $s'$.

Claim 1:  No process is at line $5$ in any state in $\alpha'$.

Proof:
Any process at line $5$ in state $s$ executes that
line by time $s.\ms{now} + c_2$, and no process can reach line $5$
during $\alpha$ (since no process is at line $4b$ until the last state
of $\alpha$).

Claim 2: If $x$ is nonzero in any state in $\alpha'$,
then $x$ is also nonzero in all subsequent states in $\alpha'$.

Proof:
By Claim 1.

Claim 3:
There exists a state $s''$ in $\alpha'$ such that $s''.s \neq 0$ and
$s''.\ms{now} \leq s.\ms{now} + (C+4) c_2$.

[[[must check the 4]]]

Proof:
There is some process in the trying region in state $s'$,
so (by case analysis, using the fact that $\ms{delay} \leq C + 1$) 
either $s'.x \neq 0$
or else by time $s.\ms{now} + (C + 4) c_2$,
some process executes line $1$ or reaches line $4b$.
But by assumption, no process reaches line $4b$ in this interval,
so it must be that $x$ is nonzero in some state $s''$ 
in the indicated interval.

Now fix $s''$ to be as claimed in Claim 3, and
let $\alpha''$ be the suffix of $\alpha$ starting with $s''$.

Claim 4: $x \neq 0$ for all states in $\alpha''$.

Proof:
By Claims 3 and 2.

Claim 5:  Process $i$ is not at line $L$ in any state in $\alpha''$.

Proof:
If it is, it finds $x \neq 0$ and gets stuck at label $L$, so could
not reach its critical region at the end of $\alpha''$.

Claim 6:  Process $i$ in the trying region in state $s''$.

Proof:
If not, then since it is in the critical region in state $u$,
it must reach line $L$ during $\alpha'$, which contradicts Claim 5.

But then there is a limit to how long process $i$ can remain in the
trying region without reaching $L$.
Namely (by case analysis), we can show that $u.\ms{now} \leq
u''.\ms{now} + (C + 3) c_2$.
Combining this bound with Claim 3 shows that $u.\ms{now} \leq (C + 7) c_2$,
as needed.
\end{proof}

[[[Comment by Nancy: Actually, I realized this morning that the algorithm has an easy
modification that gets the bound back down to $C c_2 + 3 c_2$ (or some
constant other than $3$.
The trick is just to replace the pause statement by an explicit
repeated read of $x$ (to be done approximately $C$ times (maybe it's
$C - 1$, I can't get the boundary condition right).  
If $x$ is ever seen $\neq i$, then process $i$ immediately goes back
to $L$, without waiting for the full number of reads to be completed.
I have not changed the algorithm above in this way, because I don't
know exactly how the change might affect the later argument about the
hybrid algorithm.  It probably doesn't matter there, but I'm not
certain.]]]

\subsection{Lower Bound of $C c_2$ for Mutual Exclusion and Weak Deadlock-
Freedom With $1$ Register}

The following theorem proves the near optimality of 
the time complexity of Algorithm 2.
Note that the statement below is a strengthening of our original
statement of this result to include the $3 c_2$ term.
The strengthened result and the proof we present below are due to
Faith Fich \cite {FFpersonal}.

\begin{theorem}
There is no $[c_1, c_2]$ timed algorithm providing mutual exclusion 
with weak deadlock-freedom for $n \geq 2$ asynchronous processes,
that uses only one shared read/write register, and that takes time
$b < (C+3) c_2$.
\end{theorem}

%Subject: Faith's Lower Bound Weak Deadlock-Freedom 2 Processors 1 Register
\begin{proof}
(Sketch)
%[[[ Comment: very delicate proof, and really reqires 
%us to amke the model defs of when ops happen in time precise, 
%since it relays on them. Slight revisions, please check.]]]
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 process must 
first read and then write the shared register in its execution.
Let $r_1$ and $r_2$ be the number of steps
prior to the first write of the shared register in $e_1$ and $e_2$,
respectively (by Lemma~\ref{lemma:read-write-me-wda-1},
$r_1$ and $r_2$ are greater than $0$). 

Suppose that one of these executions, say $e_1$, contains at most
$C$ steps after its first write to the shared register.
%[[[
Let $t = \max\{c_1 (r_1 + 1), c_2 (r_2)\}$ and consider the execution $e$
formed by running $e_1$ fast starting at time $t - c_1 (r_1 + 1)$
and running $e_2$ slowly starting at time $t - c_2 (r_2)$.
In $e$, the $r_2$th step of $e_2$ occurs at time $t$, followed
immediately (at the same real time) by the first write of $e_1$,
then the rest of $e_1$ until time $t + C c_1$ and finally the rest of
$e_2$,
starting with the first write in $e_2$.

In $e$, all of $e_1$ occurs before the first write of $e_2$.
Therefore process $1$ cannot distinguish between executions $e$ and $e_1$.
Furthermore, all of the writes of $e_1$ occur between the first write
of $e_2$ and the read that precedes it.
Thus process $2$ cannot distinguish between executions $e$ and $e_2$.
But $e$ violates mutual exclusion.

It follows that both $e_1$ and $e_2$ contain at least $C + 3$ steps.
Then if either execution is run slowly by itself,
at least $(C + 3) c_2$ time will elapse
before the critical region is entered.
\end{proof}

\section{The Combined Algorithm}
\label{section: timed asynchronous}

\begin{figure}[t]
\rule{8cm}{0.1 em}
{\small
\begin{tabbing}
X\= LL: XX \= XX \= \kill
\\
\> \> $x,y$: {\it shared registers initially} $0$; \\ 
\> \> {\it delay}: {\it positive integer constant}; \\ \\
\> \> {\bf repeat forever} \\
\> \> 0b:\> $\ms{remainder\_exit}_i$\\
\> \>  L:  \> {\bf if} $x \neq 0$ {\bf then goto} $L$; \\
\> \> 1:\> $x$ := $i$; \\
\> \> 2: \> {\it pause\/}({\it delay}); \\
\> \> 3: \> {\bf if} $x \neq i$ {\bf then goto} $L$; \\

\> \> \> \% Start of Fischer Critical Region\\
\> \> 4: \> {\bf if} $y \neq 0$ {\bf then goto} $L$; \\
\> \> 5: \> $y$ := 1; \\
\> \> 6: \> {\bf if} $x \neq i$ {\bf then goto} $L$;  \\ 
\> \> 7a: \> $\ms{critical\_enter}_i$ \\
\> \> 7b: \> $\ms{critical\_exit}_i$ \\
\> \> 8: \> $y$ := 0; \\
\> \>  \> \% End of Fischer Critical Region\\
\> \> 9:  \> $x$ := 0; \\
\> \> 0a:\> $\ms{remainder\_enter}_i$ \\
\> \> {\bf end repeat};
\end{tabbing}
} % end of small
\rule{8cm}{0.1 em}
\caption{Algorithm 3: Combined Exclusion Algorithm -- Code for process $i$.}
\label{fig: mutex3}
\end{figure}

In this section we give our first main result:
we show how to overcome the drawbacks
of the Fischer algorithm, Algorithm 2, providing an algorithm that 
always provides mutual exclusion and weak deadlock-freedom,
and also provides deadlock-freedom if the timing constraints 
$[c_1,c_2]$ are met.
The algorithm that accomplishes this uses only 
two shared registers and has a
``nice'' time bound close to that of Algorithm 2.

By combining Algorithms 1 and 2, one can create an
algorithm that uses three shared registers.
The way to do this is to replace
the critical region of Algorithm 2, by Algorithm 1.
However, it is also possible to get a two register algorithm, by
combining the two algorithms in a more elaborate way, 
as seen in Figure~\ref{fig: mutex3}.
The construction is based on the observation,
implied immediately by Lemma~\ref{Lemma: Fischer x:=i}, 
that in Algorithm 2,
once a process $i$ enters the critical region,
the register $x$ remains equal to $i$.
This implies that the test of $x$ in Algorithm 1
will not fail if it is embedded in Algorithm 2's critical region
{\em even if Algorithm 2 allows processes to set the same register}.

[[[fix formatting of earlier code]]]
Let Algorithm 3' be the asynchronous version of Algorithm 3.

[[[ Comment: nancy, I think we should get WND from the Lamport simulation
by adding the invariant I stated below together with the Lamport 
proof invariant I3.]]] 

Define as before: 
$RM$:  the set of process indices $i$ such that $pc(i) \in \{ 0a, 0b,
L \}$.

\begin{lemma}
\label{invt-alg3'-asynch}
In any reachable state of Algorithm 3', the following are true.
\begin{enumerate}
\item $H1$: If $|RM| = n$ then $x = y = 0$.
\item $H2$: If all processes $i \notin RM$ have $pc(i) =9$, then $y = 0$.
\end{enumerate}
\end{lemma}

[[[must work out the modelling issues -- here, ``reachable'' refers to
the augmented automaton, although the time is not important for the
asynchronous case.]]]

\begin{proof}
By induction.
The basis is trivial.
For the inductive step, consider $(s',\pi, s)$, where $s'$ is
reachable and satisfies the conditions, and $\pi$ is a step of process
$k$.
The only interesting lines to consider are lines $1$, $5$, $8$ and
$9$.
For $1$ and $5$, both conditions are vacuously true.
For $8$, Condition $H1$ is vacuously true, and Condition $H2$ is
guaranteed by the code.
For $9$, Condition $H1$ for $s$ follows from the code and from
Condition $H2$ for $s'$,
while Condition $H2$ for $s$ follows from Condition $H2$ for $s'$.
[[[check this]]]
\end{proof}

\begin{lemma}
Algorithm 3' satisfies the weak deadlock-freedom property.
\end{lemma}

\begin{proof}
By Condition $H1$, when a process enters alone, it must be that $x = y = 0$.
In this situation, the process will proceed unimpeded to the critical region.
\end{proof}

\begin{lemma}
Algorithm 3' satisfies mutual exclusion.
\end{lemma}

\begin{proof}
A proof similar to that given for Algorithm 1 can be done, with
essentially the same invariants.
(A redefinition is needed for $CR$, because of the different labels.)
It would be nicer to give a proof based on a formal simulation of the Lamport
algorithm. 
But in order to do this, we must modify the Lamport algorithm slightly.

Define Algorithm 1' to be the same as Algorithm 1, except that:
\begin{enumerate}
\item  Right after line $L$, a new line is added:
       M: if $x \neq i$ then goto L.
\item  The data type of $x$ is augmented to $\{ 0, 1, \ldots, n \}$.
\item  $x$ is initialized at $0$.
\item  Right after line $5$, a new line is added:
       N: $x := 0$.
\end{enumerate}
The modified algorithm still satisfies exactly the same invariants as
before, and so satisfies mutual exclusion as before.

We define a forward simulation (actually, a refinement)
from Algorithm 3' to Algorithm 1'.
Namely, if $s$ and $u$ are states of Algorithms 3' and 1'
respectively, we define $(s,u) \in R$ provided that the following
conditions hold.

\begin{enumerate}
\item  $s.x = u.x$.
\item  $s.y = u.y$.
\item  For every $i \in \{ 1, \ldots , n \}$,
       \begin{enumerate}
       \item  If $s.pc(i) \in \{ 0a, 0b, L,  \}$ then $s.pc(i) =
              u.pc(i)$.
       \item  If $s.pc(i) = 1$ then $u.pc(i) = L$.
       \item  If $s.pc(i) \in \{ 2, 3 \}$ then $u.pc(i) = M$.
       \item  If $s.pc(i) = 4$ then $u.pc(i) = 1$.
       \item  If $s.pc(i) = 5$ then $u.pc(i) = 2$.
       \item  If $s.pc(i) = 6$ then $u.pc(i) = 3$.
       \item  If $s.pc(i) = 7a$ then $u.pc(i) = 4a$.
       \item  If $s.pc(i) = 7b$ then $u.pc(i) = 4b$.
       \item  If $s.pc(i) = 8$ then $u.pc(i) = 5$.
       \item  If $s.pc(i) = 9$ then $u.pc(i) = N$.
       \end{enumerate}
\end{enumerate}

We show that $R$ is a forward simulation.
Base condition:
If $s$ is the initial state of Algorithm 3', then $s.x = s.y = 0$ and
$s.pc(i) = 0b$ for all $i$.
Let $u.x = u.y = 0$ and $u.pc(i) = 0b$ for all $i$.
Then $(s,u) \in R$ and $u$ is an initial state of Algorithm 1'.

Inductive step:
Consider a step $(s',\pi,s)$ of Algorithm 1', 
where $s'$ is a reachable state of Algorithm 1', 
and $\pi$ is an action of process $k$.
Suppose that $u'$ is a reachable state of Algorithm 3',
where $(s',u') \in R$.
Consider cases.

\begin{enumerate}
\item Line $0a$, $0b$.

Then the step simulates line $0a$ or $0b$, respectively, in Algorithm 3'.

\item Line $L$.

Then the step simulates a no-op in Algorithm 3'.
That is, $(s,u') \in R$.

\item Line $1$.

Then the step simulates line $L$.

\item Line $2$.

Then the step simulates a no-op.
That is, $(s,u') \in R$.

\item Line $3$.

Then the step simulates line $M$.

\item Line $4$.

Then the step simulates line $1$.

\item Line $5$.

Then the step simulates line $2$.

\item Line $6$.

Then the step simulates line $3$.

\item Line $7a$.

Then the step simulates line $4a$.

\item Line $7b$.

Then the step simulates line $4b$.

\item Line $8$.

Then the step simulates line $5$.

\item Line $9$.

Then the step simulates line $N$.
\end{enumerate}

[[[needs checking, maybe a few details]]]
\end{proof}

It remains to show (time-bounded) deadlock-freedom.
In order to show this, we define another invariant for the hybrid
algorithm:

\begin{description}
\item[{\rm H4}:] If for all $i$, $pc(i) \not\in \{6,7a,7b,8\}$
then $y = 0$.
\end{description}

\begin{lemma}
Algorithm 3 (with the timing constraints) is deadlock-free.
\end{lemma}

\begin{proof}
The basic idea is to give a forward simulation from Algorithm 3 to
Algorithm 2 (the Fischer algorithm with the timing constraints).
In order to make this work, we have to be careful about the
correspondence.
Namely, we consider a ``renamed''version 3'' of the hybrid algorithm, 
in which Line 4 is renamed as 
$\ms{Fischer\_critical\_enter}_i$
and Line 8 as 
$\ms{Fischer\_critical\_exit}_i$.
We also reclassify the actions so that the external actions are 
$\ms{remainder\_enter}_i$,
$\ms{remainder\_exit}_i$,
$\ms{Fischer\_critical\_enter}_i$, and
$\ms{Fischer\_critical\_exit}_i$.
(The reason I have to choose these statements rather than just insert
extra statements into Algorithm 3 is that the simulation is supposed
to preserve all the timing behavior.)

Then we define a simulation relation $R$ by:
$(s,u) \in R$ if:
\begin{enumerate}
\item  $s.x = u.x$.
\item  For every $i \in \{ 1, \ldots , n \}$,
       \begin{enumerate}
       \item  If $s.pc(i) \in \{ 0a, 0b, L, 1, 2, 3  \}$ 
              then $s.pc(i) = u.pc(i)$.
       \item  If $s.pc(i) = 4$ then $u.pc(i) = 4a$.
       \item  If $s.pc(i) \in \{ 5, 6, 7a, 7b, 8 \}$ then $u.pc(i) = 4b$.
       \item  If $s.pc(i) = 9$ then $u.pc(i) = 5$.
       \end{enumerate}
\item  $s.\ms{now} = u.\ms{now}$.
\item  For every $i \in \{ 1, \ldots , n \}$,
       if $u.pc(i) \neq 4b$ then 
       $s.\ms{ftime}(i) = u.\ms{ftime}(i)$ and
       $s.\ms{ltime}(i) = u.\ms{ltime}(i)$.
\end{enumerate}

We do a combined proof, showing that $R$ is a timed forward simulation
(really, a timed refinement)
and showing that invariant $H4$ is satisfied.

For the basis,
the initial state $s$ of Algorithm 3'' has $x = y = 0$, all program
counters at $0b$, $\ms{now} = 0$ and bounds for all processes
initialized at $c_1$ and $c_2$ respectively.
The same component values (except for $y$)
comprise the initial state $u$ of Algorithm
2, and $(s,u) \in R$.

For the inductive step, consider step $(s',\pi,s)$ of Algorithm 3'',
where $s'$ is a reachable state of Algorithm 3'', and suppose $(s',u')
\in R$.
Also suppose that $H4$ holds in $s'$.
If $\pi$ is a time-passage action, then it is easy to see that it
simulates the same time-passage action in Algorithm 2, and that $H4$
is preserved.
So suppose that $\pi$ is an action of a process, say of process $k$.
We consider cases.

\begin{enumerate}

\item Lines $0a$, $0b$, $1$, $2$, $3$:
Then these simulate the corresponding Lines of Algorithm 2, and also
$H4$ is preserved.

\item Line $4$
We show that this simulates Line $4a$ of Algorithm 2.
This is straightforward provided that control moves to Line $5$, i.e.,
if $s.pc(k) = 5$.  So we must show that this is the case.
It suffices to show that $s'.y = 0$.

Since $(s',u') \in R$, we have $u'.pc(k) = 4a$.
Then $k \in u'.CR$, so by $I3$ for the Fischer algorithm, it must be
that every $i \neq k$ has $i \notin u'.CR$.
Since $(s',u') \in R$, this implies that every $i \neq k$ has
$s'.pc(i) \notin \{ 4, 5, 6, 7a, 7b, 8, 9\}$, so in particular
$\notin \{ 6, 7a, 7b, 8 \}$.
Moreover, $s'.pc(k) = 4$, so also $s'.pc(k) \notin \{ 6, 7a, 7b, 8
\}$.
Thus, $s'.pc(i) \not\in \{6,7a,7b,8\}$ for any $i$.
Since $s'$ is assumed to satisfy $H4$, it follows that $s'.y = 0$, as needed.

The invariant $H4$ is preserved.

\item Line $5$

Then the step simulates a no-op in Algorithm 2 (since $y$ is not used in 
Algorithm 2).
The invariant $H4$ is satisfied vacuously, since $s.pc(k) = 6$.

\item Line $6$

We show that this simulates a no-op.
This is straightforward provided that control moves to Line $7a$, i.e.,
if $s.pc(k) = 7a$.  So we must show that this is the case.
It suffices to show that $s'.x = k$.

Since $(s',u') \in R$, we have $u'.pc(k) = 4b$.
Since $u'$ satisfies $I3$ of the Fischer algorithm, we have $u'.x =
k$.
But since $(s',u') \in R$, this means that $s'.x = k$, as needed.

$H4$ holds vacuously in $s$ because $s.pc(k) = 7a$.

\item Line $7a$, $7b$.

This simulates a no-op, and $H4$ is satisfied vacuously.

\item Line $8$

We claim that this simulates Line $4b$ (since $y$ is not used in
Algorithm 2).
To see $H4$, note that $s.y = 0$ from the code.

\item Line $9$:
Then this simulates Line 5 of Algorithm 2, and also
$H4$ is preserved.
\end{enumerate}

Thus, we have shown the simulation, as well as the invariant $H4$.

Now we argue deadlock-freedom.
Instead of arguing the ``eventual'' version of the property as before,
we just argue the time-bounded version.

[[[In the various no-deadlock proofs, must consider the exit region as
well as the trying region, but that should always be easy.]]]

Consider any execution $\alpha$ of Algorithm 3;
with the additional naming conventions,
$\alpha$ can also be regarded as an execution of Algorithm 3'.
Consider any state $s$ of
that execution in which some process is in the trying region and no
process is in the critical region (Line $4b$).
Then by the forward simulation of the Fischer algorithm, there is an
execution $\alpha'$ of the Fischer algorithm that has the same events
from among the four: $\ms{remainder\_enter}$, $\ms{remainder\_exit}$
$\ms{Fischer\_critical\_enter}$, and $\ms{Fischer\_critical\_exit}$,
occurring at the same real times.
Since the Fischer algorithm satisfies deadlock freedom with time bound
$(2C + 7) c_2$ (provided that $\ms{delay} \leq C + 1$),
this means that within time $(2C + 7) c_2$ from $s.\ms{now}$, some
process, say $k$, executes Line $4$.

Then within additional time $3 c_2$, process $i$ will execute Line
$7a$ and hence enter the critical region.
To see this, we need to verify that process $k$ does not branch back
to $L$ at either line $4$ or line $6$.
But this has already been argued in the proof of the simulation, where
we consider these cases.
[[[Proof can probably be organized a little better here.]]]
\end{proof}

Thus, we actually have:

\begin{lemma}
Algorithm 3 (with the timing constraints) has an upper bound of 
$(2C + 10) c_2$ time.
\end{lemma}

