%Formal Models Underlying the M.E. Paper
%Nancy Lynch
%June 15, 1992

\section{General Models and Relationships Between Them}

The general model used in this paper seems to be MMT, including the
possibility of right-open $\infty$ upper bound intervals to represent
eventuality.
We call this model MMT here.
Note that this is not the same as the model used, e.g., in
Attiya-Lynch work, because that model ruled our the open $\infty$
upper bounds.

For any MMT automaton $A$, 
we should be able to perform the construction in
Attiya-Lynch to get an augmented automaton $A'$.
However, the augmentation would not do anything with the open $\infty$
upper bounds.
This means that to get an ``equivalent'' automaton, we would need to couple
the augmented automaton with an additional liveness condition $L$ stating
eventuality constraints for the open $\infty$ upper bounds.
There should then be an equivalence theorem saying that
the admissible behaviors of the augmented automation $A'$ that satisfy the
liveness condition $L$
are exactly the same as the behaviors of the original MMT automaton $A$.
Other correspondences should also hold, for example, that any
invariant that is true of $A'$ and that only involves the state of $A$
(and not the $\ms{now}$, $\ms{ftime}$ and $\ms{ltime}$ components)
is also true of $A$.

Each augmented automaton should essentially be a special case of a
Lynch-Vaandrager automaton (up to some minor syntactic differences).
However, the liveness conditions do not fit the LV model - they are
externally-imposed restrictions to be added.

As a special case of MMT, consider an automaton $A$ in which all
boundmap intervals are $[0, \infty)$.
Then the augmentation $A'$ ignores all the bounds, so that
$\ms{ftime}$ is always $0$, 
$\ms{ltime}$ is always $\infty$, and $\ms{now}$ changes with time.
The added liveness condition $L$ 
expresses all the eventuality conditions, for all classes.
The automata $A$ and $(A',L)$ are both ``equivalent'' to a
naturally-defined I/O automaton $A''$, in a very strong sense.  
In particular, the behaviors of $A$ are the same as the admissible
behaviors of $A'$ that satisfy $L$, which are in turn the same as the
fair behaviors of $A''$.
Also, invariants are true of the I/O automaton $A''$ are also true of
$A'$ and of $A$.

Now we consider the organization of the various proofs in the m.e.
paper.

\section{Lamport Algorithm}

This is formulated as an MMT automaton $A$, with all boundmap intervals
being $[0,\infty)$.
Thus, we consider the equivalent I/O automaton $A''$

ME: We prove the invariants for the I/O automaton $A''$.
They carry over, as above, to the MMT automaton $A$.

WDF: We do an operational proof using the I/O automaton $A''$.
Since the fair behaviors of $A''$ are the same as the behaviors
of the MMT automaton $A$, the WDF result carries over to $A$.

\section{Fischer Algorithm}

This is formulated as an MMT automaton $B$, with the boundmap intervals
for the users leaving the critical regions being $[0,\infty)$, but the
boundmap intervals for the process steps being $[c_1,c_2]$.

ME, assuming time bounds:
We do the invariant proof using the augmented state machine $B'$.
Recall this imposes no limits for the $\infty$ upper bounds.
The invariants do not require the additional liveness condition giving
the critical region upper bounds, for their proof.
Recall that any invariant that is true of $B'$ and that only involves 
the state of $B$
(and not the $\ms{now}$, $\ms{ftime}$ and $\ms{ltime}$ components)
is also true of $B$.
Thus, in particular, mutual exclusion is true for $B$.

DF, assuming no time bounds:
We consider another MMT automaton $C$ related to $B$, which just loosens
all boundmap intervals to $[0,\infty)$.  
As before, this has a naturally-corresponding I/O automaton $C''$.
We do an operational argument to show DF for $C''$ (i.e.,
for its fair behaviors), which therefore implies DF for $C$
(i.e., for its behaviors).

time-bounded DF, assuming time bounds:
This is an operational argument, done directly on the MMT automaton $B$.
It uses as a lemma, the result about DF proved for $C$ (with no time bound
assumptions).
But since $C$ is ``looser'' than $B$, this implies DF for $B$ as well.
Note that in this operational argument, there is no need of the
open $\infty$ upper bound for exiting the critical region.
It follows that time-bounded DF holds for the augmented automaton $B'$
as well, without the extra liveness condition.
(A general theorem might be possible here.)

\section{Hybrid Algorithm}

This is formulated as an MMT automaton $D$, with the boundmap intervals
for the users leaving the critical regions being $[0,\infty)$, but the
boundmap intervals for the process steps being $[c_1,c_2]$.

We also consider $E$, the ``loosened''version of $D$.

WDF:  
Direct operational argument using the loosened version $E$.

ME, assuming no time bounds:
This is proved by a mapping from this algorithm to the Lamport
algorithm (actually, to a slight modification of the Lamport algorithm).
More specifically, we map the I/O automaton $E''$
to the I/O automaton $A''$ corresponding to the Lamport algorithm.
The result of this gives inclusion of behaviors of the two I/O
automata, 
which implies that the mutual exclusion invariant carries
over from $A''$ to $E''$.
Since mutual exclusion only involves the state of $E$,
mutual exclusion holds for $E$ as well, and hence for $D$, since $E$
is a loosening of $D$.

time-bounded ND assuming time bounds:
This is proved using a mapping from this algorithm to the Fischer
algorithm.
More specifically, we map the augmented algorithm $D'$ (without the
time bounds for the critical region) to the augmented algorithm $B'$.
Actually, there is a little renaming involved in the algorithm $D'$.
Then the result of the mapping is the inclusion of the 
admissible timed behaviors of 
(the renamed) $D'$ in those of $B'$.

The timed DF condition was proved operationally for $B'$.
This implies that the time for algorithm $D'$ to reach the beginning
of its portion of code designated as the ``Fischer critical region''
is as for $B'$ reaching the critical region.
Carry this result over to $D$, and finish the argument operationally
in $D$ (bounding how long it takes to reach the actual critical
regions of $D$).



