<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">% timed
\section{The Timing-Based Case}

\begin{figure}[t]
\rule{8cm}{0.1 em}
{\small
\begin{tabbing}
X\= LL: XX \= XX \= \kill
\\
\&gt; \&gt; $x$: {\it shared register initially} $0$; \\
\&gt; \&gt; {\it delay}: {\it positive integer constant}; \\ \\
\&gt; \&gt; {\bf repeat forever} \\
\&gt; \&gt; 0b:\&gt; $\ms{remainder\_exit}_i$ \\
\&gt; \&gt;  L:  \&gt; {\bf if} $x \neq 0$ {\bf then goto} $L$; \\
\&gt; \&gt; 1:\&gt; $x$ := $i$; \\
\&gt; \&gt; 2: \&gt; {\it pause\/}({\it delay}); \\
\&gt; \&gt; 3: \&gt; {\bf if} $x \neq i$ {\bf then goto} $L$; \\
\&gt; \&gt; 4a: \&gt; $\ms{critical\_enter}_i$ \\
\&gt; \&gt; 4b: \&gt; $\ms{critical\_exit}_i$ \\
\&gt; \&gt; 5:\&gt; $x$ := 0; \\
\&gt; \&gt; 0a:\&gt; $\ms{remainder\_enter}_i$ \\
\&gt; \&gt; {\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 &lt; c_1 \leq c_2 &lt; \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$).

\absrem{ %%%%%%%%%%%%%%%%%%
\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.
%[[[ Comment: Nancy, I did not find it interesting to mention that 
%it continues to provide mutex when the timing constraints are 
%not met. This is a property that we do  not use in our solutions.]]]

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. 
Specifically, let {\it pause\/}$(k)$ be a shorthand for a sequence of
$(k - 1)$ lines of code, each a no-op operation, and let us accordingly 
assign program counter values 
$2.1, 2.2, \ldots, 2.(k-1)$ to those $(k-1)$ lines.

We now outline the correctness proof of the algorithm. 
Let Algorithm~2' be the same as Algorithm~2 but asynchronous
%(i.e.,with all the process' classes having bounds $[0,\infty)$)
. The following lemma follows by induction on the length of the
execution.
\begin{lemma}
\label{invt-alg2'-asynch}

Then in any reachable state of Algorithm~2':
\begin{quote}
If $x = i \neq 0$
then $\ms{pc}_i \in \{ 2, 3, 4a, 4b, 5\}$.
\end{quote}
\end{lemma}

\absrem{  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{proof}
By induction on the length of the execution.
Initially the claim holds vacuously since $x=0$.
We assume it holds in any reachable state $s$, 
and for the inductive step, go over all the possible 
operations (or operation and $pc(i)$ change ) $\pi_i$ of a process $i$,
leading from $s$ to a new state $s'$ in any
given execution. We refer to these operations
by their relative line numbers in the code. 
\begin{description}
\item[{\rm Lines~0a,0b,L}:]
Holds since $x$ remains $0$ in $s'$. 
\item[{\rm Line~1}:]
Holds since in $s'$ $x=i$ and $pc(i)=2$.
\item[{\rm Line~2}:]
In $s'$ $pc(i)=3$ so if $x=i$ we are done, and if $x=j$, $j \neq i$ 
the claim follows from the inductive hypothesis given that 
$x$ remains unchanged.
\item[{\rm Line~3}:]
If in $s$ $x = i$ then in $s'$ $pc(i)=4a$ and the claim holds.
If $x \neq i$ then it holds in $s'$ by the inductive hypothesis 
applied to $s$ and the fact that $x$ remains unchanged.
\item[{\rm Lines~4a,4b}:]
The claim follows from the inductive hypothesis on $s$ given that 
\item[{\rm Line~5}:]
In $s'$ $x = 0$ and the claim follows immediately.
\end{description}
\end{proof}

[[[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.]]]
} %%%%%%%%%%% end of absrem %%%%%%%%%5

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. 
\absrem{ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note that by the construction of the timed
%augmented automaton, 
} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
From our definitions,
it follows that 
if $\ms{pc}(i) \notin \{ 0b, 4b \}$ 
then $\ms{ltime}(i) \leq \ms{now} + c_2$.

Let CR be defined similarly to before. We prove the following collection
of invariants by induction on the number of steps in an
execution. They are similar to those proposed in \cite{Abadi-Lamport} for a
weaker form of the mutual exclusion problem.
%We prove the following 
%[[[
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}
In any reachable state of Algorithm 2, the following are true.
\begin{description}
\label{Lemma: Fischer x:=i}

\item[$I1$:]  \label{invt-alg2-1}
       If $i \in \mbox{\it CR}$ then 
       \begin{enumerate}
       \item $x = i$, and 
       \item for all $j$, $\ms{pc}(j) \neq 1 $.
       \end{enumerate}
\item[$I2$:]  If $\ms{pc}(i) = 2.d$, $x = i$ and $\ms{pc}(j) = 1$ 
              then $\ms{ltime}(j) &lt; \ms{ftime}(i) + (delay - d\/) c_1 $.
\item[$I3$:]  If $\ms{pc}(i) = 3$, $x = i$ and $\ms{pc}(j) = 1$ 
              then $\ms{ltime}(j) &lt; \ms{ftime}(i)$.
%
%\item[$I3$:]  If $\ms{pc}(i) = 1$ then $\ms{ltime}(i) &lt; \ms{now} + c_2$.
\end{description}
\end{lemma}

\absrem{ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{proof}
By induction on the length of the execution.
Initially all three invariants hold vacously since 
all processes are in the remainder regions.
We assume they hold in any reachable state $s$, 
and for the inductive step, go over all the possible 
operations (or operation and $pc(i)$ change ) $\pi_i$ of a process $i$,
leading from $s$ to a new state $s'$ in any
given execution. As before, we refer to these operations
by their relative line numbers in the code. 
\begin{description}
\item[{\rm Lines~0a,0b,L}:]
Holds since $x$ remains $0$ in $s'$. 
[[[to be completed]]]
\end{description}
\end{proof}
} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

From $I1$ of Lemma \ref{invt-alg2} we have:
\begin{lemma}
\label{Lemma: Fischer ME}
Algorithm 2 has the mutual exclusion property.
\end{lemma}

\absrem{ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{proof}
By Lemma \ref{invt-alg2}, Part \ref{invt-alg2-1}.
\end{proof}
} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

We prove the following based on Lemma \ref{invt-alg2'-asynch}. 

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

\absrem{ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{proof}
[[[Consider any reachable state $s$ in which some process 
is in the trying region and no process is in the critical region, 
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
with $\ms{pc} \in\{4a,4b,5\}$, and no additional processes
enter the trying region.
We can without loss of generality
assume this holds throughout the execution.

We claim that $x$ eventually reaches a state $s''$
following which in all states $x=i$ for some $i \in \{1..n\}$,
that is, the index of some process.
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 some
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 $\mbox{\it delay\/} = C+1$. Then Algorithm 2 
has an upper bound of $(2C + 7) c_2$.
\end{lemma}

\absrem{ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{proof}
[[[Consider any reachable state $s$ in which some process 
is in the trying region and no process is in the critical region
(Lines~$4a$ and $4b$).
Then within $c_2$ time there is a state $s'$
in which either a process is in the critical region 
or no processes are with $\ms{pc} \in\{4a,4b,5\}$.
By Lemma~\ref{alg2-DA}, there must be a process 
$i$ that executes the critical region next.                     

Assume $x \neq 0$ in state $s'$. By the above, $pc(i) \neq L$
in any state following $s'$.
Thus, $i$ cannot be in the remainder and 
since $pc(i) \in \{1,2,3\}$, and $i$ 
never executes Line~$L$ again, within $(C + 3) c_2$ time
it will enter the critical region. 

Assume $x = 0$ in state $s'$. Since there is some 
process in the remainder, within $(C + 2) c_2$ 
some process sets $x \neq 0$ or some process is in
Line~4a in a new state $s''$. In the latter case, 
a process enters the critical region in $c_2$ 
additional time. In the former case, since in $s''$
$x \neq 0$, the above argument implies that within 
$(C + 3) c_2$ time
some process will enter the critical region. 

Summing it all up, within at most 
$(2C + 7) c_2$ time from the time the system is in state $s$,
some process enters the critical region.
\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.
Our original bound of  $C c_2$ was strengthened by 
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 &lt; (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 requires 
%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
\\
\&gt; \&gt; $x,y$: {\it shared registers initially} $0$; \\ 
\&gt; \&gt; {\it delay}: {\it positive integer constant}; \\ \\
\&gt; \&gt; {\bf repeat forever} \\
\&gt; \&gt; 0b:\&gt; $\ms{remainder\_exit}_i$\\
\&gt; \&gt;  L:  \&gt; {\bf if} $x \neq 0$ {\bf then goto} $L$; \\
\&gt; \&gt; 1:\&gt; $x$ := $i$; \\
\&gt; \&gt; 2: \&gt; {\it pause\/}({\it delay}); \\
\&gt; \&gt; 3: \&gt; {\bf if} $x \neq i$ {\bf then goto} $L$; \\

\&gt; \&gt; \&gt; \% Start of Fischer Critical Region\\
\&gt; \&gt; 4: \&gt; {\bf if} $y \neq 0$ {\bf then goto} $L$; \\
\&gt; \&gt; 5: \&gt; $y$ := 1; \\
\&gt; \&gt; 6: \&gt; {\bf if} $x \neq i$ {\bf then goto} $L$;  \\ 
\&gt; \&gt; 7a: \&gt; $\ms{critical\_enter}_i$ \\
\&gt; \&gt; 7b: \&gt; $\ms{critical\_exit}_i$ \\
\&gt; \&gt; 8: \&gt; $y$ := 0; \\
\&gt; \&gt;  \&gt; \% End of Fischer Critical Region\\
\&gt; \&gt; 9:  \&gt; $x$ := 0; \\
\&gt; \&gt; 0a:\&gt; $\ms{remainder\_enter}_i$ \\
\&gt; \&gt; {\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}.

%[[[Nancy comment: 
%Need to redefine RM here - those in $\{ 0a, 0b, L \}$.
%Nir Comment: I think we can get away with RM being 0a and 0b
%only, which will keep us more consistent with former sections.]]]
%[[[I don't understand either my comment or yours here.  I thought
%this WAS the definition of RM.  N.]]]

\absrem{ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
We prove the following by induction on the length of the execution.
[[[ 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.]]]
\begin{lemma}
\label{invt-alg3'-asynch}
Let Algorithm 3' be the asynchronous version of Algorithm 3.
Then in any reachable state of Algorithm 3', the following are true.
\begin{enumerate}
\item If $|RM| = n$ then $x = y = 0$.
\item If all processes [[[$i$ outside]]] of $RM$ 
have $pc(i) =9$, 
%are at the
%point just before the last ($x := 0$) assignment 
then $y = 0$.
\end{enumerate}
\end{lemma}

\begin{proof}
By induction.
[[[needs doing]]]
\end{proof}
} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\absrem{ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{proof}
[[[Nir to work on this]]]
Uses Lemma \ref{invt-alg3'-asynch}.
WDA follows easily, since when a process enters alone in the
situation where $x = y = 0$, it will zip right through.
\end{proof}

Now we define an invariant for the 2V algorithm:

I. If no process is either in the critical region (the real critical
region, that is) or just at the point of checking $x = i$ before the
critical region,
then $y = 0$.

I think we can do one big induction, proving at the
same time (a) that there is a timed forward simulation from 2V to Fischer
and (b) that 2V satisfies Invariant I.
In this simulation, we have to allow the real critical region of 2V
to correspond to the real critical region of Fischer, so that we will
show that the extra steps (those involving y, and the extra test for x
= i) simulate no-ops in Fischer.

Consider the inductive step.
E.g., suppose the 2V algorithm does a step where pi tests the value of
y.  If it found y = 1, then that would be bad, because the resulting
jump back to L would not simulate any allowed step of Fischer.
But mutual exclusion of the Fischer algorithm 
in the pre-state and the definition of the mapping
implies that pi is the only process in the ``Fischer critical
region'' part of the 2V code; therefore, no process is 
either in the (real) critical region of 2V nor 
just at the point of checking x = i before the critical region.
Then invariant I in the pre-state implies that y = 0 in the pre-state,
a contradiction.

Also e.g., suppose the 2V algorithm does a step where pi tests the
value of x just before entering the critical region, finding it
unequal to i.
Again, the resulting jump back to L would not simulate Fischer
correctly.
But pi is in the ``Fischer critical region'' part of the 2V code in
the pre-state, so that by Lemma \ref{invt-alg2}, part \ref{invt-alg2-1}
and the correspondence, it must be that x = i in the pre-state.
This is a contradiction.

Thus, it looks like all the steps correspond properly.
Now consider preserving Invariant I.
The only steps that need to be considered here are the step that sets
y to 1 and the steps that cause a process to leave the designated
portion of the code.
The step that sets y to 1 simultaneously puts a process in the
designated portion of the code, so it cannot cause a problem.
Also, if a process leaves the designated portion by means of a normal
exit, then it simultaneously sets y to 0, so it cannot cause a
problem.
The only remaining possibility is that a process pi leaves the designated
portion of code by finding $x \neq i$ in the test just prior to the
critical region.
But we argued above that this cannot occur.

Therefore, we have the simulation, and Invariant I.

Now we complete the proof of timed ND.
[[[Actually, maybe this is not needed at all.
If we show a timed simulation of Fischer, and Fischer has the time
bound property, then I think it may carry over to this algorithm
without any further work.  Sound right?
We need to take into account the fact that the time blows up somewhat
in the simulation.]]]

Here, I will proceed for now somewhat operationally.
First, if anyone is in the exit region (that must be between the two
assignments restoring the 0 values) then there is nothing preventing
it from  moving to the remainder region.
So we consider the trying region.

Suppose we are in a timed execution alpha in which, from some point on,
at least one process is in T, no one is in C, 
and no process moves from T to C.
Then after some point $t$ in alpha, no process changes regions at
all, and there is no one in the exit region - there are just some
bunch of processes in T, continually taking steps and getting nowhere.
Since no one goes to C and everyone continues taking steps, they must
all be continually dropping back to L.

Consider any time when x has value 0 in alpha.
I claim that there must be some later time when some process sets x to
its index (because it reaches L and sees x = 0).
But past time $t$, if a process sets x to its index, then x can never
be set back to 0 (since x only gets set to 0 when a region change
occurs).
So there is some last time when x has value 0, after which it only has
values that are process indices.
Thus, eventually in alpha, no process will be able to get past
statement L,
because they will all see $x \neq 0$.
This implies that there is some last time, say $t'$,
that x gets a value assigned to it.
Let i be the last index assigned to x.
(Note that this time $t'$ could be before or after $t$.)

Now, register $x$ keeps value $i$ from time $t'$ on, for the rest of the
infinite execution alpha.
Then F1 implies that process pi is one of the processes that stays
in the trying region after point $t$.
But consider pi just after it assigns x := i at time $t'$.
I claim there is nothing preventing pi from advancing to the (real)
critical region.
Since this is the last assignment to x, when pi tests x (both times),
it must find x = i.
Also, when pi reaches the test of y, it is in the ``Fischer critical
region'' portion of the 2V code, so as in the simulation proof above,
y = 0.
This means that pi has a clear path to the (real) critical region,
since all its tests come out right.
This contradicts the fact that pi is one of the looping processes.

A little ugliness here:
This is not quite a contradiction.  Process pi could have gone to its
critical region and then come back in, before time $t$.  But if it
did this, then it would set x := 0 when it exited, and we have assumed
that there are not further assignments to x.

Ugh! Operational proofs aren't nice.
Maybe later, we will want to do this ND proof via a mapping, proving a
time bound rather than an ``eventually'' result.

[[[ Nancy, I suggest that we do the proofs here at this stage 
by repeating the invariants and proofs of the Fischer and Lamport.
We should later, in the final version, do it all with mappings.
]]]
} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
To prove correctness of Algorithm 3,
%[[[
we let Algorithm 3' be the same as Algorithm 3, but without the timing
constraints.
We show the following by induction on the length of the computation.

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

%\begin{lemma}
%The following are true in all reachable states of Algorithm 3'.
%\begin{enumerate}
%\item[{\rm I1}:] If for all $i$, $pc(i) \in RM$,
%then $x = 0$.
%\end{enumerate}
%\end{lemma}

Then we define a forward simulation mapping \cite{LV-REX} 
from Algorithm 3' to Algorithm 1.
From this we prove that:

\begin{lemma}
Algorithm 3' satisfies the mutual exclusion and 
weak deadlock-freedom properties.
\end{lemma}

That is, Algorithm 3 has these properties even if the timing
constraints are not satisfied.
%]]]

\absrem{ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{proof}
The same three invariants as in the proof of Lamport's algorithm seem
to hold for this algorithm.
[[[Need to be careful about making the right redefinitions for the
sets CR, RM, etc.]]]
The proof is by induction just as before, and mutual exclusion follows
from 1. 

Alternatively, I think we could prove ME by producing a mapping from
the 2V algorithm to the Lamport algorithm.  But in order to do this,
we would probably have to add some more nondeterministic choices to
the Lamport algorithm.  E.g., we would need to add an option of going
back to L after setting x to i and before seeing y = 0, 
if x is detected as unequal to i.
With such additional nondeterminism, the original ME proof (using the
invariants above) should still work.
Then a forward simulation mapping of the usual sort might work out OK.
(The value x = 0 in the 2V algorithm would probably need to correspond
to arbitrary values of x in the Lamport algorithm.)
I think that your Lemma 1.1 could probably (and profitably) 
be restated in this mapping style.
[[[ Nir to work on this]]]
\end{proof}
} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5

We prove the following two lemmas by defining a timed forward simulation
\cite{LV-REX} from Algorithm 3 (with the timing constraints)
to the Fischer algorithm, Algorithm 2,
and then proving it and the 
following invariant by induction on the length of the computation:
\begin{description}
\item[{\rm I3}:] 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}

\absrem{ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{proof}
[[[This is just a collection of various remarks.
They begin with some of Nancy's old remarks, probably prior to the
lengthy sketch that was presented above.]]]

As in the proof of the Fischer algorithm, the state needs to be
augmented with timing predictions for the times until the next steps
of each process.
Maybe operational is a little easier for now, here.
But at any rate, we probably want to prove 
invariant 4 from the Fischer algorithm again, for this algorithm.
Then ND should follow from timed ND and timed ME of Fischer.

[[[What follows now is some suggestions by Nir.]]]

[[[ I suggest that we prove by a mapping to Fischer
and Lemma~\ref{Lemma: Fischer ME}
we are guaranteed that one, and
no more than one process $i$ will concurrently
execute the ``Fischer critical region,'' and that while it is executing it,
$x=i$.

Now prove the invariant that if $y=1$ there is a process 
between $y :=1$ and $y :=0$.
So $i$ must read $x=i$ and $y=0$ and 
thus it will enter the critical region.]]]

\end{proof}
In the mapping proof to the Fischer algorithm
of Figure~\ref{fig: mutex2} (in which he step in Line~4a is
replaced by 3 steps) and  Lemma~\ref{lemma: fischer lb}, we have:]]]
} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{lemma}
Algorithm 3 (with the timing constraints) has an upper bound of 
$(2C + 10) c_2$ time.
\end{lemma}
</pre></body></html>