% model.tex

\begin{figure}[t]
\rule{8cm}{0.1 em}
{\small
\begin{tabbing}
XXXX\= L: XX \= \kill
\> {\bf Process $i$:} \\
\> {\bf repeat forever} \\
\> \> {\em remainder region} \\
\> \> {\em trying region} \\
\> \> {\em critical region} \\
\> \> {\em exit region} \\
\> {\bf end repeat};
\end{tabbing}
} % end of small
\rule{8cm}{0.1 em}
\caption{Program of Process $i$.}
\label{fig: mutual exclusion}
\end{figure}


\absrem{ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{I/O Automata Protocols and Time}


\label{ioa}
[[[ Comment: I have decided to slice here and leave it all 
to the  full paper. Since I cut out most of the proofs, 
we are OK for the abstract. ]]]

[[[ old comment by Nir: In this section, we present the definitions for the underlying
formal model.  In particular, we define I/O automata and timed
automata. We also show how we model shared memory protocols.
[[[ Comment: Nancy, I agree with the idea of using a definition of 
Timed I/O Automata that  has regular automata as a special case.
However,  it would be best, at least in the extended abstract, to limit the 
model to half-3/4 ofa page. 
I will try to now create a truely UNCLEAN variant of what I mean, that takes 
little space (after all, cutting 
down space is what this paper is all about, ha ha).
If I have time I will get back to cleaning it.]]]

We begin by summarizing some of the key definitions for the
I/O automaton model.
We refer the reader to \cite{LynchT87,LynchT89} 
for a complete presentation of the model and its properties.

An {\em I/O automaton}, $A$, consists of the following pieces:
$\ms{acts}(A)$, a set of {\em actions}, classified as {\em output}, 
{\em input} and {\em internal} 
(input and output actions are called {\em external});
$\ms{states}(A)$, a set of {\em states}, including a
distinguished subset, $\ms{start}(A)$, of {\em start states};
$\ms{steps}(A)$, a set of steps, where a {\em step} is defined to
be a ({\em state, action, state}) triple;
and $\ms{part}(A)$, a {\em partition} of the locally controlled 
(output and internal) actions into equivalence classes; the
partition groups together actions that are to be thought of as under
the control of the same underlying process.

An action $\pi$ is said to be {\em enabled} in a state $s'$ provided
that there is a step of the form $(s',\pi,s)$.  An automaton is
required to be {\em input enabled}, which means that every input
action must be enabled in every state.  
[[[To model time, we define
a {\em boundmap} mapping $b$ for an I/O automaton $A$,
associating a [[[]]] subinterval of $[0,\infinity)$ with 
the class of operations of any process, 
representing the range of possible lengths of time between successive
times when this process ``gets a chance'' to perform an action.]]]
[[[ add something to say non-zero]]]

[[[A {\em timed execution fragment} of an I/O automaton $A$
is a (finite or infinite) sequence of
alternating states and (action,time) pairs,
\[  s_0,(\pi_1,t_1),s_1,(\pi_2,t_2),...  ~,\]
where for every $i$, $(s_{i-1},(\pi_i,t_i),s_i) \in steps(A)$,
the times $t_1$, $t_2$,... are successively nondecreasing
nonnegative real numbers, and
if the sequence is finite, then it ends with a state.]]]
An {\em execution} is an execution fragment 
with $s_0 \in \ms{start}(A)$.
Two events 
The {\em schedule} of an execution $\alpha$ is the subsequence of $\alpha$
consisting of all the events appearing in $\alpha$, and 
the {\em behavior} of $\alpha$ is the 
subsequence consisting of all the external events.
The {\em schedules} and {\em behaviors} of $A$ are just those of
the executions of $A$.
%An {\em extended step} is a triple $(s',\beta,s)$ for which there is
%an execution fragment that starts and ends with $s'$ and $s$, respectively,
%and whose schedule is $\beta$.

[[[Ordinary I/O automata are just a special case of timed automata,
where the boundmap provides all intervals of the form $[0,\infty)$
\cite{CONCUR91}. ]]]
Concurrent systems are modeled [[[in the natural way as]]]
compositions of I/O automata \cite{LynchT87,LynchT89}.

\subsection{Timed Automata}

[[[Taken from mappings paper with Hagit.]]]

In this subsection, we augment the I/O automaton model to allow
discussion of timing properties.  The treatment here is
similar to the one described in \cite{AttiyaL89} and is a
special case of the definitions proposed 
in \cite{MerrittMT90}.

A {\em boundmap} for an I/O automaton $A$ is a a mapping that
associates a closed subinterval of $[0,\infinity]$ with each class in
$\ms{part}(A)$, where the lower bound of each interval is not $\infty$
and the upper bound is nonzero.\footnote{ 
	In \cite{MerrittMT90} the model is defined in a more general manner,
	to allow for open or semi-open intervals as the boundmaps.}
Intuitively, the interval associated with a class $C$ by the boundmap
represents the range of possible lengths of time between successive
times when $C$ ``gets a chance'' to perform an action.
We sometimes use the notation $b_\ell(C)$ to denote the lower bound
assigned by boundmap $b$ to class $C$, and $b_u(C)$ for the
corresponding upper bound.
A {\em timed automaton} is a pair $(A,b)$, where $A$ is an I/O
automaton and $b$ is a boundmap for $A$.

We require notions of ``timed execution'', ``timed schedule''
and ``timed behavior'' for timed automata, corresponding to
executions, schedules and behaviors for ordinary I/O automata.
These will all include time information.  We begin by defining
the basic type of sequence that underlies the definition of a
timed execution.

\begin{definition}
A {\em timed sequence} (for an I/O automaton $A$)
is a (finite or infinite) sequence of
alternating states and (action,time) pairs,
\[  s_0,(\pi_1,t_1),s_1,(\pi_2,t_2),...  ~,\]
satisfying the following conditions.
\begin{enumerate}
\item The states $s_0$, $s_1$, ... are in $\ms{states}(A)$.
\item The actions $\pi_1$, $\pi_2$,... are in $\ms{acts}(A)$.
\item The times $t_1$, $t_2$,... are successively nondecreasing
nonnegative real numbers.
\item If the sequence is finite, then it ends in a state $s_i$.
\item If the sequence is infinite then the times are unbounded.
\end{enumerate}
\end{definition}

For a given timed sequence, we use the convention that $t_0 = 0$.  
For any finite timed sequence $\alpha$, we define $\tend(\alpha)$
to be the time of the last event in $\alpha$, if $\alpha$
contains any (action,time) pairs, or $0$, if $\alpha$ contains
no such pairs.
Also, we define $\send(\alpha)$
to be the last state in $\alpha$.
We denote by $\ms{ord}(\alpha)$ (the ``ordinary'' part of
$\alpha$) the sequence
\[  s_0,\pi_1,s_1,\pi_2,...  ~,\]
{\it i.e.}, $\alpha$ with time information removed.

If $i$ is a nonnegative integer and $C \in \ms{part}(A)$, we say that
$i$ is an {\em initial index} for $C$ in $\alpha$ if 
$s_i \in \ms{enabled}(A,C)$ and
either $i = 0$ or $s_{i-1} \in \ms{disabled}(A,C)$ or $\pi_i \in C$.
Thus, an initial index for class $C$ is the index of an event
at which $C$ becomes enabled;
it indicates a point in $\alpha$ from which we will begin measuring upper
and lower time bounds.

\begin{definition}   \label{timed execution of (A,b) definition}
Suppose $(A,b)$ is a timed automaton.
Then a timed sequence $\alpha$ is a
{\em timed execution} of $(A,b)$
provided that $ord(\alpha)$ is an execution of $A$
and $\alpha$ satisfies the following conditions,
for each class $C \in \ms{part}(A)$ and every initial index $i$ for 
$C$ in $\alpha$.
\begin{enumerate}
\item 
If $b_u(C) < \infty$
then there exists $j > i$ 
with $t_j \leq t_i + b_u(C)$ 
such that either $\pi_j \in C$ or $s_j \in \ms{disabled}(A,C)$.

\item 
There does not exist $j > i$ with $t_j < t_i + b_\ell(C)$ and $\pi_j$ in $C$.
\end{enumerate}
\end{definition}

The first condition says that, starting from an initial index for $C$,
within time $b_u(C)$ either some action in $C$ occurs or 
there is a point at which no such action is enabled.  
Note that if $b_u(C) = \infty$, no upper bound requirement is imposed.  
The second condition says that,
again starting from an initial index for $C$,
no action in $C$ can occur before time $b_\ell(C)$ has elapsed.
Note in particular that if a class $C$ becomes disabled and then
enabled once again, the lower bound calculation gets ``restarted''
at the point where the class becomes re-enabled.

[[[Here, we should look up MMT CONCUR 91, and generalize the
definition to permit open intervals as bounds as well as closed
intervals.  With an upper-open interval with upper bound $\infty$, we
can model eventual steps in the class.]]]

The {\em timed schedule} of a timed execution of a timed
automaton $(A,b)$ is the subsequence consisting of the
(action,time) pairs, and the {\em timed behavior} is the
subsequence consisting of the (action,time) pairs for which the
action is external.  The {\em timed schedules} and {\em timed
behaviors} of $(A,b)$ are just those of the timed executions of
$(A,b)$.

[[[Informally, our model of computation consists of a collection of sequential
threads of control called {\em processes} that communicate through 
shared objects called {\em registers}.
Formally, ]]]we model each timing-dependent concurrent system as a single timed 
automaton $(A,b)$, where $A$ is a composition of ordinary I/O automata
(possibly with some output actions hidden),[[[ and $b$ is a boundmap.
Details of the model will be presented in the full version of the paper.
We refer the reader to \cite{LynchT87,LynchT89,MMT,AttiyaLynch} 
for a complete presentation of the model and its properties.

[[[Comment: We need to define operations and 
say what it means for them to be concurrent and terminating.]]]

[[[Comment: Nancy, I do not agree that my way of stating 
all things in terms of separate automata
has unfortunate consequences. One can easily enough define operations as
pairs of invocation and matching response, and use tools
such as sequential specification to formalize possible interactions. 
This would make our modeling of the system more `true to life.''
However, it is not a big thing with me, and 
your proposal has proven itself in the past so why not.]]]

\footnote{
An equivalent way of looking at each system is as a composition
of timed automata.  An appropriate definition for a composition
of timed automata is developed in \cite{MerrittMT90}, together
with theorems showing the equivalence of the two
viewpoints.}
} %%%%%%%%%%%55 remoevd from abstract %%%%%%%%%%
\remove{ %%%%%%%%%%%%
[[[The following is what Nir wrote earlier.]]]
Probably we should revise it as I indicate above.]]]
%
A process $P$ is an I/O automaton with output events
{\sc write}$(P,v,R)$, {\sc read}$(P,R)$,
input event {\sc return}$(P,v,R)$;
\remove{ %%%% FOR CASE OF RANDOMIZED LOWER BOUND we need %%%%% 
and an internal event {\sc coin-flip}$(P,x)$ where $v$ is a value, $R$ a register,
and $x$ (the value of the coin-flip) an element of the set $\{\mbox{\it heads},
\mbox{\it tails}\}$.
The two {\sc coin-flip} events of a process represent the possible 
results of a random decision made within the process; if either is enabled 
in a particular state, the other must also be enabled.
} %%%%%%%%%%%% END CASE OF RANDOMIZED LOWER BOUND %%%%%%%%%%%
A {\it register R}
is an I/O automaton with input events 
{\sc write}$(P,v,R)$, {\sc read}$(P,R)$ and output event {\sc return}$(P,v)$,
where $P$ is a process and $v$ a value. A {\it protocol} 
$\{P_1,\ldots,P_n;R_1,\ldots,R_m\}$ is the I/O automaton composed by 
identifying in the obvious way the events for processes $P_1,\ldots,P_n$
and registers $R_1,\ldots,R_m$. {\sc read} and {\sc write} events are 
called invocations, and {\sc return} events are called responses. An 
invocation and response {\em match} if their process and register 
names agree, and 
{\it complete}$(H)$ is the maximal subsequence of {\em H} consisting
only of invocations and matching responses. If $H$ is a schedule,
an {\it operation} of $H$ is a pair consisting of an invocation and matching 
response. $H$ is {\it sequential} if (1) the first event of {\em H} is an 
invocation, (2) each invocation, except possibly the last, is immediately 
followed by a matching response, and each response is immediately 
preceded by a matching invocation. A schedule that is not sequential is 
{\it concurrent}. A protocol schedule is {\it well-formed} if each $H|P_i$ is
sequential, and a protocol is {\it well-formed} if each of its histories is 
well-formed. We assume all protocols are well-formed.
[[[ Nancy, we need to add stuff about the probability 
of each schedule to allow the 
results about the stochastic model. We also need to say what a global state 
is. ]]] A {\it higher level operation} by a process consists of a sequence of 
operations. It is {\it terminating} if the number of such operations is finite.
% 
If we restrict our attention to sequential histories, then the behavior of 
a register can be specified in a particularly simple way: each value read
was the last value written. We would like to ensure that a protocol's
concurrent histories are ``equivalent,'' in some sense, to its sequential 
histories. We capture this using the notion of linearizability
\cite{Her-Wing}. 
It is a valid proof technique to ignore any
specific implementation details of the read/write registers,
and to assume that these operations occur as atomic actions
sometime within the corresponding operation interval
\cite{L86a,HW87,LynchT87b}.
} %%%%%%%%%%% removed %%%%%%%%%%%%%%%%%%%
\absrem{ %%%%%%%%%%%%%%%% removed fo abstract %%%%%%%%
[[[I have not done anything above to model randomized algorithms.
I suggest we not clutter up the main body of the paper with
randomization issues - there is quite enough other stuff without it.
Rather, let's discuss extensions to the randomized case in the
conclusions section (((((((OK, no problem))))))).]]]
} %%%%%%%%%%%%%%%% removed fo abstract %%%%%%%%

%The sections that follow present the algorithms in
%familiar psuedo-code style. Translating them into
%timed automata is a straightforward but tedious exercise.  

\section{The Mutual Exclusion Problem}
\label{lxdef}

We consider a system of $n$ sequential threads of control called 
{\em processes}, which communicate through shared 
%[[[
{\em multi-writer, multi-reader} atomic registers.
Communication consists of {\em read} and {\em write} operations,
each of which is assumed in this paper to be executed instantaneously.
In the usual model for atomic registers %\cite{Lamport-atom}, 
%[[[Joanne: This is his ``On Interprocess Communication'' paper, Part I.]]]
each operation is separated
into an {\em invocation} event and a {\em response} event, 
concurrent invocations are allowed, 
and it is assumed that every invocation eventually
terminates in a matching response, in such a way as to produce the
illusion of instantaneous operation. 
Our work applies to this setting, but
we do not need to deal with this extra complication here.
%]]]

Formally, we model each 
%[[[
such
%]]] 
system as a single {\em timed automaton} \cite{MMT} $(A,b)$, 
where $A$ is a composition of %ordinary 
I/O automata \cite{LynchT87},
%[[[This is the Lynch, Tuttle PODC paper.]]]
%(possibly with some output actions hidden), 
and $b$ is a boundmap.
%Details of the model will be presented in the full version of the paper.
We keep the discussion in this abstract informal
and refer the interested reader to \cite{LynchT87,LynchT89,MMT,AttiyaLynch} 
for a complete presentation of the model and its properties.

We view the program of every process as consisting of two
distinguished regions: a {\em remainder region} and a
{\em critical region}.
%[[[(Formally, for a given process,
%the code of a region defines a 
%subclass of events in $\ms{part}(A)$) of the system automaton.]]]
%[[[The above comment refers to a definition that is not included
%here.
%In addition, I don't understand what you mean.  N.]]]
Each process alternates between executing its remainder and its
critical region.
%[[[
No process remains forever within any particular execution of
its critical region, although it may remain forever in its remainder region.
%]]]
The {\em mutual exclusion problem} is to guarantee that the system
does not enter a global state in which more than one process
is executing its critical region \cite{Dijkstra}.

To coordinate the entrance to the critical region, a {\em trying region}
and an {\em exit region} of 
code are added to the program of each process as in 
Figure~\ref{fig: mutual exclusion}.

%These program regions define a set of possible 
%schedules of higher level operations.
%[[[I don't understand this statement.  N.]]]

\absrem{ %%%%%%%%%%%%%%%%%%%%%%%%%% remove from abs %%%%%%%5
So, I let $\ms{user}_i$ be a timed automaton with states
consisting of the value of one variable, called $\ms{region}$, with
values in $\{ R, T, C, E \}$.
There are outputs $\ms{try}_i$ and $\ms{exit}_i$, and inputs
$\ms{crit}_i$ and $\ms{rem}_i$.  
The user respects the cyclic behavior
(what should it do if the system does not respect the cyclic behavior?)
In addition, there should be a liveness constraints:
that a user in $C$ eventually does an $\ms{exit}_i$.  
We can do this using the upper bound of $\infty$, in a right-open
interval, for the singleton class of $\ms{exit}_i$.
We don't want to say that the user in $R$ eventually does a
$\ms{try}_i$, however.
Thus, the singleton class of $\ms{try}_i$ just has an interval
$[0,\infty]$ associated (meaning the action never has to occur.
]]]
} %%%%%%%%%%%%%%%%%%%%%%%%%% remove from abs %%%%%%%5

%\subsection{Properties}

The following safety property is required of any solution to the problem.

\begin{description}
\item[{\em Mutual Exclusion:}]
A system satisfies {\em mutual exclusion}
if in any reachable system state, at most one user is in its 
critical region.
\end{description}

We also require that a process running alone will always get access to
the critical region.
%[[[ Nancy, I agree, we could make the exit regions
%wait-free, but then we nedd to define wait-free etc 
%so in the4 end we do the same amount of work...]]]

%[[[I changed terminology to ``deadlock-free''.]]]

\begin{description}
\item[{\em Weak Deadlock-Freedom:}]
A system is {\em weakly deadlock-free} 
if in any execution,
%the following holds in any execution.
%\begin{enumerate}
%\item
%\begin{quote}
if a process' trying region (resp. exit region) is concurrent only 
with other processes' remainder regions, then its trying region (resp. exit
region) terminates.
%\end{quote}
%\item
%If a process' exit region is concurrent only 
%with other processes' remainder region, then its exit region terminates.
%\end{enumerate}
\end{description}

The following property guarantees progress, and will 
be required to hold only under certain conditions.

\begin{description}
\item[{\em Deadlock-Freedom:}]
A system is {\em deadlock-free} 
if the following are true in any execution.
\begin{enumerate}
\item
If in some state, some user is in the trying region and no user
is in the critical region,
then subsequently some user enters the critical region.
\item
If in some state, some user is in the exit region
then subsequently some user enters the remainder region.
\end{enumerate}
\end{description}

\absrem{ %%%%%%%%%%%%%%%% remove from abstract %%%%%%%%
[[[The following lemma follows immediately from the above definitions:]]]
\begin{lemma}
If a system is {\em deadlock-free} 
then it is {\em weakly deadlock-free}.
\end{lemma}

%\subsection{Time Bounds}
} %%%%%%%%%%%%%%%% remove from abstract %%%%%%%%

We define a time-bounded version of the deadlock-freedom property.
This involves putting an upper bound on the time 
%[[[
processes
%]]]
%[[[Your change was incorrect.  This property does not have to do with
%an individual process, but rather with the ensemble of all processes.  N.]]]
can spend executing the added {\it trying} and {\it exit} regions
of code. We define a number $b$ to be an {\em upper bound} for a {\em
deadlock-free} system providing that the deadlock freedom
definition above holds if we replace ``subsequently'' with ``within time at
most $b$.''
\absrem{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{enumerate}
\item  
If in some state, some user is in the trying region and no user
is in the critical region,
then within time at most $b$, some user enters the critical region.

\item
If in some state, some user is in the exit region
then within time at most $b$, some user enters the remainder region.
\end{enumerate}
} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%