%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                    Section 1: Model of Computation                       %
%                    Created: 4/6/97                                       %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Model}
\label{section: model}
In order to develop a useful and applicable complexity theory for
asynchronous, distributed computer systems, we need to define some
reasonable model of such systems. This model must be detailed enough
so as to accurately and faithfully capture the inherent complexity of
solving tasks in real distributed systems, yet be simple enough so as
to easily lend itself to some practical form of complexity
analysis. The model we consider in this consists of a restricted class
of one-shot distributed problems, called decision tasks, together with
a novel model of computation, a type of shared memory called the {\em
non-uniform immediate snapshot model}. This section contains a
detailed description of these fundamental concepts. It also contains
the complexity measures that will be used to analyze the complexity of
solving decision tasks in the non-uniform immediate snapshot model.

\subsection{Informal Synopsis}
\label{subsection: synopsis}
We begin with an informal synopsis of our model, which largely follows
that of Herlihy and Shavit \cite{HS93,HS94}.  Some fixed number $N =
n+1$ of sequential threads of control, called {\em processes},
communicate by asynchronously accessing shared memory in order to
solve {\em decision tasks}. In such a task, each process starts with a
private {\em input} value and halts with a private {\em output} value.
For example, in the well-known {\em binary consensus} task, the
processes have binary inputs, and must agree on some process's input
\cite{FLP}.  A {\em protocol} is a distributed program that solves a
decision task in such a system.  A protocol is {\em wait-free} if it
guarantees that every non-faulty process will halt in a finite number
of steps, independent of the progress of the other processes. The {\em
time complexity} of solving a decision task in this model on a given
input set is the supremum of the number of accesses to shared memory
made by any process on that input set.

\subsection{Decision Tasks}
\label{subsection: decision tasks}
In this subsection, we define decision tasks more precisely. This class
of tasks is intended to provide a simple model of reactive systems,
such as databases, file systems, or automatic teller machines. An
input value represents information entering the system from the
surrounding environment, such as a character typed at a keyboard, a
message from another computer, or a signal from a sensor. An output
value models an effect on the outside world, such as an irrevocable
decision to commit a transaction, to dispense cash, or to launch a
missile. A decision task is, informally speaking, a relation between
vectors of input values and vectors of output values. We define this
more precisely below.

Let $D_I$ and $D_O$ be two data types, possibly identical, called the
{\em input data type} and the {\em output data type}, respectively. We
first define the concept of an input vector.

\begin{definition}
\label{def: input vector}
An $n+1$-process {\em input vector} $\vI$ is an $n+1$-dimensional
vector, indexed by $\Bbb{Z}$$_{n+1}$(the integers $\mod n$), each
component of which is either an object of type $D_I$, or the
distinguished value $\bot$, with the additional requirement that at
least one component of $\vI$ must be different from $\bot$.
\end{definition}

The definition of output vectors is similar to that for input vectors:

\begin{definition}
\label{def: output vector}
An $n+1$-process {\em output vector} $\vO$ is an $n+1$-dimensional
vector, indexed by $\Bbb{Z}$$_{n+1}$, each component of which is either an
object of type $D_O$, or the distinguished value $\bot$,
\end{definition}

When it is clear from the context, we omit mentioning the number of
processes in specifying input and output vectors. We denote the $i$-th
component of an input vector $\vI$ by $\vI[i]$, and similarly, we
denote the $i$-th component of an output vector $\vO$ by $\vO[i]$. In
the sequel, unless stated otherwise, we will assume that $i$ and $j$
are index values in the set $\Bbb{Z}$$_{n+1}$. These index values will
be used both for specifying vector elements and also to index
processes.

\begin{definition}
\label{def: vector prefix}
A vector $\vU$ is a {\em prefix} of $\vV$ if $\vV[i] = \bot$ implies
that $\vU[i] = \bot$ and for all $i$ such that $\vU[i]
\neq \bot$, $\vU[i] = \vV[i]$.
\end{definition}

%\begin{definition}
%A set $V$ of vectors is {\em prefix-closed} if the following
%conditions are true:
%\begin{itemize}
%\item For all $\vV \in V$, every prefix $\vU$ of $\vV$ is in $V$.
%\item If $\vV, \vU \in V$, and $\vW$ is a prefix of both $\vU$ and $\vV$, then $\vW \in V$.
%\end{itemize}
%\end{definition}

\begin{definition}
\label{def: prefix-closed}
A set $V$ of vectors is {\em prefix-closed} if for all $\vV \in V$,
every prefix $\vU$ of $\vV$ is in $V$.
\end{definition}
In this paper we will only consider sets of input and output vectors
that are prefix-closed.

\begin{definition}
An {\em input set} is a fnite, prefix-closed set of input vectors. An
{\em output set} is a finite, prefix-closed set of output vectors.
\end{definition}

Next, we define the notion of a task specification map, which is
essentially a relation between the input set of and the output set.

\begin{definition}
\label{def: task specification}
Let $I$ and $O$ be input and output sets, respectively.  A {\em task
specification} relating the two sets is a map $\gamma$, carrying each
input vector $\vI$ to a prefix-closed, non-empty set $\gamma(\vI)$ of
output vectors, with the additional requirement that, for all $i$,
$\vI[i] = \bot$ if and only if for all $\vO \in \gamma(\vI)$, $\vO[i]=
\bot$.
\end{definition}

For a given input vector $\vI$, the set of vectors $\gamma(\vI)$
represents the set of legitimate output vectors for the set of inputs
specified by $\vI$. This set will generally contain more than one
allowable output vector.


We are now ready to give a precise definition of
decision tasks.

\begin{definition}
\label{def: decision task}
A {\em decision task} $\dt2$ is a tuple consisting of a set $I$ of
input vectors, a set $O$ of output vectors, and a task specification
map $\gamma$ relating these two sets.
\end{definition}

We note that, by definition, decision tasks are inherently one-shot,
since all participating processes have a single input and must decide
on a single output exactly once.

%A process' output value is said to be its {\em decision value}. Once a
%process has decided on an output value, it remains decided from that
%point on. 

%Tasks are thus inherently one-shot, since all participating
%processes have a single input and must decide on a single output
%exactly once.

%A vector $\vU$ {\em matches} $\vV$ if for all $i$, $\vU[i] = \bot$ if and only if %$\vV[i] = \bot$.

%A vector $\vU$ is a {\em prefix} of $\vV$ if $\vV[i] = \bot$ implies
%that $\vU[i] = \bot$ and for all $i$ such that $\vU[i]
%\neq \bot$, $\vU[i] = \vV[i]$.

%In this thesis, we will only be concerned with a class of decision
%tasks that meet the following {\em extensibility} requirement.

%\begin{definition}
%A decision task $\dt2$ is {\em extensible} if, for any input vectors
%$\vI$ and $\vJ$, where $\vI$ is a prefix of $\vJ$, each vector in
%$\gamma(\vI)$ is a prefix of some vector in $\gamma(\vJ)$.
%\end{definition}

Not all entries in a given input vector need contain an input value;
Some may contain the special value $\bot$, indicating that some
processes do not receive an input value. We formalize this notion of
participation in the definition below.

\begin{definition}
\label{def: vector participating}
For any input vector $\vI$, if the $i$-th component is not $\bot$,
then $i$ {\em participates} in $\vI$. Otherwise, we say that $i$ does
not participate in $\vI$. Moreover, we define the {\em participating
set} in $\vI$ to be set of participating indexes.
\end{definition}

As noted by Herlihy and Shavit \cite{HS93, HS94}, the reason for
incorporating an explicit notion of participating indexes in our
formalism for decision tasks is that it is convenient for
distinguishing between tasks such as the following, which have the
same sets of input and output vectors, but different task
specification maps.

\begin{example}
The $n+1$-process Unique-Id task is defined as follows:
\begin{itemize}
\item $I = \{[0, \ldots, n] \mid x_i \in \{i, \bot\}\}$.
\item $O = \{[x_1, \ldots, x_n] \mid x_i \in \Bbb{Z}$$_{n+1} \cup
\{\bot\}, (x_i = x_j) \Rightarrow (x_i = \bot)\}$.
\item $\forall \vI \in I: \vO \in \gamma(\vI)$ iff for all $i,j$, $(\vO[i] = \vO[j]) \Rightarrow (\vO[i] = \bot)$.
\end{itemize}
\end{example}

\begin{example}
The $n+1$-process Fetch-And-Increment task is defined as follows:
\begin{itemize}
\item $I = \{[x_0, \ldots, x_n] \mid x_i \in \{i, \bot\}\}$.
\item $O = \{[x_1, \ldots, x_n] \mid  x_i \in \Bbb{Z}$$_{n+1} \cup
\{\bot\}, (x_i = x_j) \Rightarrow (x_i = \bot)\}$.
\item $\forall \vI \in I: \vO \in \gamma(\vI)$ iff for all $i, j$, the following two conditions hold:
\begin{itemize}
\item $(\vO[i] = \vO[j]) \Rightarrow (\vO[i] = \bot)$.
\item $\vO[i]$ must be less than the size of the participating set of $\vI$..
\end{itemize}
\end{itemize}
\end{example} 

The two decision tasks above differ in that the task specification map
of {\em Fetch-And-Increment} involves explicit mention of the
participating set of the input vectors in order to capture the fact
that indexes are handed out in an increasing order while that of {\em
Unique-Id} does not. % [[[Gunnar -- remember toi change as above in final 
%tr]]]

%Informally, in an asynchronous, distributed system in which processes
%may fail-stop, {\em Unique-Id} allows identifiers to be assigned
%statically, while {\em Fetch-And-Increment} effectively requires that
%they be assigned dynamically in increasing order, as the task
%specification map involves explicit mention of the participating set
%of the input vectors.

%The first is trivially solved in the
%presence of an arbitrary number of failures, while the second has no
%solution in read/write memory even if only one process can fail. 
%Note that the model of Biran, Moran, and Zaks \cite{BMZ} does not include a
%notion of participating processes, although the same effect can be achieved by
%giving each process an additional ``participate'' bit as an input.

\subsection{One-Shot Immediate Snapshot}
\label{subsection: IS}
Borowsky and Gafni's Immediate Snapshot object (IS)
\cite{BorowskyGafniPODC} has by now been proven to be a useful building 
block for the construction and analysis of protocols in asynchronous,
distributed systems \cite{BorowskyGafniPODC, Neiger, HS93, BGSIMM}.

%It is essentially equivalent to a restriction of standard one-shot
%atomic snapshot memory, in which each maximal run of writes by some
%set of processes is immediately followed by a maximal run or reads by
%the same set of processes. 

Informally, an $n+1$-process IS object consists of a shared
$n+1$-dimensional memory array, and supports a single type of external
operation, called {\mbox{{\it writeread\/}}}. The IS object has $n+1$
ports, one for each process. We typically associate process $i$ with
the $i$-th port. Each \writeread operation writes a value to a single
shared memory array cell, and then immediately returns a snapshot view
of the entire array. There is a separate \writeread operation for each
of the IS object's $n+1$ ports. A \writeread operation on port $i$
writes its value to the $i$-th cell of the memory array.

Formally, we can specify IS objects as I/O automata \cite{automata}.
Let $D$ be any data type, and define $\vartheta (D)$ to be the data
type $(D \cup \{\bot \})^{n+1}$, the set of all $n+1$-arrays each of
whose cells contains either an element of $D$, or $\bot$. We index the
elements of $\vartheta (D)$ using the numbers in ${\Bbb{Z}}_{n+1}$. An
IS automaton for $n+1$ processes and data type $D$ called $IS_x$ is
defined as in Figure ~\ref{ISspec}.  We refer to such an object as an
$IS_D^{n+1}$ object. When the data type and number of processes are
clear from the context, we usually omit the sub- and superscripts
above.

\input{ISspec}
 
For all $i$, the \inv action simply writes the input value $v$ to the
$i$th cell of the
\ivalue array. This array provides temporary storage for
inputs to the $IS_D^{n+1}$ object. At the same time, the flag {\em
``inv''} is written to the $i$-th cell of the \interface array, which
indicates that an input has arrived on port $i$. The \update action
periodically copies a set of values corresponding to the indices in
$\cU$, from the \ivalue array to the \memory array. The set $\cU$ must
be a subset of the indices $i$ with the property that \interfacei $=
inv$. Additionally, a copy of the \memory array is written to the
$i$th cell of the \rvalue array for each $i \in \cU$. Finally, the
flag $ret$ is written to the $i$-th cell of the interface array for
each $i \in \cU$, indicating that a response value to the invocation
on port $i$ is available. The \ret output action provides a response
to a previous invocation on port $i$. Its only effect on the IS object
is to reset the value \interfacei to $\bot$, thereby preventing more
than one response to an invocation.  The \ret action can only occur
after a return value has been written to the $i$-th cell of the
\rvalue array, and the flag {\em ``ret''} has been written to the
corresponding cell in the \interface array.

In the remainder of this subsection, we will state and prove a few basic
properties about IS objects. These properties will be useful later,
when we prove the correctness of a topological framework for analyzing
the complexity of protocols in models of computation that include
multiple IS objects. For the purpose of this discussion, let us for
the remainder of this subsection fix our attention on a single
$IS_D^{n+1}$ object, which we will call $IS_x$.

\begin{definition}
\label{def: IS execution}
An {\em execution} of $IS_x$ is an alternating sequence of object
states and actions\\ 
$s_0, a_1, s_1, a_2, s_2, \ldots$, where $s_0$ is a start state of
$IS_x$, and for all $k$, where $k \geq 1$, the action $a_k$ brings the
object from state $s_{k-1}$ to state $s_k$.
\end{definition}

It is clear that, in any execution $\alpha$ of $IS_x$, \writeread
invocations and responses will occur in alternating order, starting
with an invocation, on each port $i$. The following definition
provides a convenient notation for matching pairs of invocations and
responses in $\alpha$.

\begin{definition}
\label{def: IS operation}
For all $i$, a \writereadvS {\em operation} in an execution $\alpha$
is an \inv action together with the next \ret action on the same port.
\end{definition}

The operation \writereadvS uses the $i$-th port of $IS_x$ to write the
value $v$ to the $i$-th cell of \memory, and subsequently return a
snapshot $S$.

\begin{definition}
\label{def: incomplete IS operation}
For all $i$, an {\em incomplete operation} in an execution $\alpha$ is
an \inv action for which there is no subsequent \ret action on the
same port.
\end{definition}

An incomplete operation \inv in $\alpha$ uses the $i$-th port of
$IS_x$ to write a value $v$ to the $i$-th cell of \memory, but there
is no subsequent response on the $i$-th port in $\alpha$.

We note that the specification of $IS_x$ does not in any way restrict
the number of accesses that may occur on any given port in an
execution. In fact, it even allows two invocations on a port $i$
before any response is given to the first invocation. In this paper,
however, we will only be using IS objects as building blocks to
construct more complicated, long-lived models of computation, not as a
long-lived object in its own right. Therefore, we will only consider a
restricted class of executions of $IS_x$, called {\em one-shot
executions}, as defined below.

\begin{definition}
\label{def: IS one-shot}
A {\em one-shot execution} of $IS_x$ is an execution for which there
is at most one invocation and at most one response on each port.
\end{definition}

In the remainder of this subsection we will be considering only on-shot
executions of $IS_x$.

\begin{lemma}
\label{lemma: update disjoint}
For any two distinct actions \update and {\mbox{{\it update($\cU'$)
\/}}} in a one-shot execution $\alpha$ if $IS_x$, the index sets 
$\cU$ and $\cU'$ are disjoint.
\end{lemma}

\begin{proof}
Suppose without loss of generality that $\cU$ occurs before $\cU'$,
and suppose $i \in \cU$. Immediately after the action{\mbox{{\it
update($\cU$)\/}}}, \interfacei is equal to {\mbox{{\it
``ret''\/}}}. Since we are considering a one-shot execution,
\interfacei will remain equal to {\mbox{{\it ``ret''\/}}} for the
remainder of the execution. Hence, the precondition of the {\mbox{{\it
update($\cU'$) \/}}} action guarantees that $i \not \in \cU'$.
\end{proof}

We can now define what we mean by concurrent operations of $IS_x$.

\begin{definition}
\label{def: IS concurrent}
Two operations {\mbox{{\it writeread($v_i,S_i$)$_{i,IS_x}$ \/}}} and
{\mbox{{\it writeread($v_j,S_j$)$_{j,IS_x}$ \/}}} in a one-shot
execution $\alpha$ of $IS_x$ are concurrent if there exists an action
\update in $\alpha$ such that $i,j \in \cU$.
\end{definition}

%\begin{lemma}(Neiger)
%\label{set-linearizable}
%Any immediate snapshot object is set-linearizable.
%\end{lemma}

%This Lemma \cite{Neiger} implies that each one-shot execution of an IS
%object can be linearized such that the writes of concurrent
%\writeread operations occur before the corresponding snapshot reads.

$IS_x$ exhibits a property called {\em self-containment}. A snapshot
returned on port $i$ by a \ret action in a one-shot execution
$\alpha$, must necessarily contain the value written to \memory in the
matching, preceding \inv action on port $i$ that is part of the same
operation. This property is proven in Lemma~\ref{lemma: IS
self-containment}.

\begin{lemma}
\label{lemma: IS self-containment}
Consider any operation {\mbox{{\it writeread($v_i,S_i$)$_{i,IS_x}$
\/}}} in a one-shot execution $\alpha$ of $IS_x$. Then $S_i[i] \neq
\bot$.
\end{lemma}

\begin{proof}
The input value $v_i$ is written to \memory by an action {\mbox{{\it
update($\cU_i$) \/}}}. In the same action, after the $v_i$ has been
written to \memory, the \memory variable is copied to \rvaluei. This
value is then returned as a response on port $i$. It follows that
$S_i[i] \neq \bot$ for all $i$.
\end{proof}

The values returned by a \ret action are $n$-dimensional arrays of
type $\vartheta(D)$. The following definition provides an order
relation on the set of such arrays.

\begin{definition}
\label{def: array prefix}
An array $A_1$ is a {\em prefix} of $A_2$ if $A_1[i]=\bot$ implies
that $A_2[i]= \bot$, and for all $i$ such that $A_2[i] \neq \bot$,
$A_2[i] = A_1[i]$.
\end{definition}

In the following lemma, we prove that $IS_x$ exhibits the property
that the set of snapshots returned in any one-shot execution can be
totally ordered by the prefix relation defined above.

\begin{lemma}
\label{lemma: IS snapshot}
Consider any two \writeread operations in $\alpha$, {\mbox{{\it
writeread($v_i,S_i$)$_{i,IS_x}$ \/}}}\\
 and {\mbox{{\it writeread($v_j,S_j$)$_{j,IS_x}$ \/}}}. Either $S_i$ is
a prefix of $S_j$ or $S_j$ is a prefix of $S_i$.
\end{lemma}

\begin{proof}
Suppose the values $v_i$ and $v_j$ are written to \memory by the
actions {\mbox{{\it update($\cU_i$) \/}}} and {\mbox{{\it
update($\cU_j$) \/}}}, respectively. 

If these actions are the same, that is, if $\cU_i =
\cU_j$, the two operations {\mbox{{\it
writeread($v_i,S_i$)$_{i,IS_x}$ \/}}} and {\mbox{{\it
writeread($v_j,S_j$)$_{j,IS_x}$ \/}}} are concurrent. In this case, the
value of \memory that is copied to \rvaluei is identical to the value
copied to {\mbox{{\it return\_value[j]\/}}}, since both are copied by
the same {\mbox{{\it update($\cU_i$) \/}}} action. It follows that
$S_i = S_j$. Now suppose $\cU_i \neq \cU_j$, and suppose {\mbox{{\it
update($\cU_i$) \/}}} occurs after {\mbox{{\it update($\cU_j$)
\/}}}. Since no \memory cells are ever reset, it follows that the
\memory version that is written to {\mbox{{\it return\_value[j]\/}}}
during {\mbox{{\it update($\cU_j$) \/}}} is a prefix of the version
that is written to \rvaluei during {\mbox{{\it
update($\cU_i$) \/}}}. Hence $S_j$ is a prefix of $S_i$. The case where
{\mbox{{\it update($\cU_j$) \/}}} occurs after {\mbox{{\it
update($\cU_i$) \/}}} is similar, and in this case we have that $S_i$
is a prefix of $S_j$. The lemma follows.
\end{proof}

The final lemma concerns what is referred to as the {\em immediacy}
property of $IS_x$. If a value written to \memory by an invocation on
port $j$ is contained in a snapshot on port $i$, then the snapshot
returned on port $j$ is a prefix of that returned on port $i$. This
corresponds to the informal notion of a \writeread operation on port
$j$ happening {\em before} a writeread operation on port $i$.

\begin{lemma}
\label{lemma: IS immediacy}
Consider any two \writeread operations in $\alpha$, {\mbox{{\it
writeread($v_i,S_i$)$_{i,IS_x}$ \/}}}\\
and {\mbox{{\it writeread($v_j,S_j$)$_{j,IS_x}$ \/}}}. If $S_i[j] \neq
\bot$ then $S_j$ is a prefix of $S_i$.
\end{lemma}

\begin{proof}
Suppose the values $v_i$ and $v_j$ are written to \memory by the
actions {\mbox{{\it update($\cU_i$) \/}}} and {\mbox{{\it
update($\cU_j$) \/}}}, respectively, and suppose $S_i[j] \neq
\bot$. This implies that $v_j$ was written to \memory during 
{\mbox{{\it update($\cU_i$) \/}}}, in which case $\cU_i = \cU_j$, or
the action {\mbox{{\it update($\cU_j$)\/}}} occured before {\mbox{{\it
update($\cU_i$) \/}}}. In either case, since no \memory cells are ever
reset or written to more than once in a one-shot execution, we have
that $S_j$ must be a prefix of $S_i$.
\end{proof}

Figure ~\ref{ISexample} shows a stylized diagram of the IS object $IS_x$.

\input{ISexample}

\subsection{The Iterated Immediate Snapshot (IIS) Model}
\label{subsection: IIS}
The {\em Iterated Immediate Snapshot (IIS) Model}, first used by
Herlihy and Shavit \cite{HS94}, was recently formulated as a
computation model by Borowsky and Gafni \cite{BGSIMM}. The model
assumes a finite sequence $IS_D^{n+1}, IS_{\vartheta (D)}^{n+1},\\
IS_{\vartheta^2 (D)}^{n+1}, \ldots, IS_{\vartheta^{k-1}(D)}$ of IS
objects, denoted $IS_1, IS_2, IS_3, \ldots, IS_k$, where $k > 0$. In
the $k${\em -shot IIS model}, there are $k$ available IS objects in
sequence.

Each protocol in the IIS model is fully determined by the maximum
number $n+1$ of processes that can participate, the number $k$ of IS
objects available, and a decision map $\delta: \vartheta^k(D)
\rightarrow D_O$, where $D_O$ is an arbitrary data type, which we call
the protocol's {\em output data type}. We refer to the protocol
obtained by fixing these parameters as $\cP_{(n,k,\delta)}$.

We can specify the $\cP_{(n,k,\delta)}$ protocol using I/O automata
\cite{automata} as follows. Each IS object is specified as in 
figure ~\ref{ISspec}, and each process $i$ is specified as in Figure
~\ref{IISprotocol}.  The protocol $\cP_{(n,k,\delta)}$ can then be
specified by composing the automata for the processes with the IS
object automata by matching up operations as follows. Assume that for
each process $i$, and each $x$, where $1 \leq x \leq k$, the object
$IS_x$ is connected to the $x$-th port on $i$, and the $i$-th process
is connected to the $i$-th port on $IS_x$.  For each processor $i$ and
IS object $IS_x$, we match up $i$'s and $IS_x$'s \inv and \ret
actions.  The resulting protocol automaton is denoted
$\cP_{(n,k,\delta)} = \{0, 1, \ldots, n; IS_1, IS_2, \ldots, IS_k\}$.

%Any execution $\alpha$ of a protocol $\cP_{(n,k,\delta)}$ unfolds in
%time from some reference time $t_0$, which is set before any process
%performs any action. After the time $t_0$, the protocol is said to be
%{\em executing}.

%\begin{definition}
%At any time $t > t_0$, the {\em state at time $t$ } of an executing
%protocol $\cP_{(n,k, \mu)}$ is the $n+1$-dimensional vector whose
%$i$-th element equals the value of the \ls variable of process $i$ at
%time $t$.
%\end{definition} 

%\begin{definition}
%The {\em initial state} of an executing protocol $\cP_{(n,k, \mu)}$ is
%the state of the protocol at time $t_0$.
%\end{definition}

%\begin{definition}
% The {\em final state} of an executing protocol $\cP_{(n,k, \mu)}$
%{\em in a finite execution $\alpha$} is the state of the protocol at
%any time $t$ after all processes have stopped performing actions.
%\end{definition}

%We note that the last definition requires the additional restriction
%that the execution $\alpha$ must be finite.

In any execution $\alpha$, the first action executed by any process
$i$ is a \starti action, which stores an {\em input value} $v$ in its
\ls variable. A process $i$ may not have a \starti action in $\alpha$, 
however, in which case it takes no steps at all in this particular
execution.

\begin{definition}
\label{def: protocol participating}
A process $i$ is said to {\em participate} in an execution $\alpha$ of
the protocol $\cP_{(n,k,\delta)}$ if $\alpha$ contains a \starti
action. The set of participating processes in $\alpha$ is called the
{\em participating set} in $\alpha$.
\end{definition}

A process $i$ is said to {\em decide} in an execution $\alpha$ when it
executes a \finishi action. After executing a \finishi action, a
process $i$ does not take any further steps in $\alpha$. The value $S$
returned by the \finishi action is process $i$'s {\em output value} in
$\alpha$.

For any execution $\alpha$ of $\cP_{(n,k,\delta)}$, the processes' input
values can conveniently be represented using an $n+1$-dimensional {\em
input vector} $\vI$, as specified in the previous subsection, with input
data type $D$. The $i$-th entry of $\vI$ is the input of process
$i$. Similarly, the processes' output values in $\alpha$ can be
represented using an $n+1$-dimensional {\em output vector} $\vO$.  The
$i$-th entry of $\vO$ is the output of process $i$.

It should be noted that the notions of participating processes and
sets defined for executions and input vectors are consistent; A
process $i$ participates in an execution $\alpha$ if and only if the index $i$
participates in the input vector $\vI$ corresponding to
$\alpha$. Therefore, when the meaning is clear from the context, we
usually omit qualifying a participating set with an execution or input
vector.

%Just as for tasks, our formalism for protocols includes an explicit
%notion of participation, as defined below.

%\begin{definition}
%Suppose we are given an execution $\alpha$ of $\cP_{(n,k, \mu)}$ with
%corresponding input vector $\vI$.  A process $i$, where $0 \leq i \leq
%n$, is said to {\em participate} in $\alpha$ if $\vI[i] \neq \bot$,
%that is, if $i$ participates in $\vI$. The set of participating
%processes in $\alpha$ is called the {\em participating set} in
%$\alpha$.
%\end{definition}

%For simplicity, when the context is clear, we usually omit qualifying
%a participating set with an execution or input vector.

In any execution $\alpha$ of $\cP_{(n,k,\delta)}$, each participating,
non-failing process $i$ starts by accessing the first IS object by
executing a {\mbox{{\it writeread($v$)$_{i,IS_1}$ \/}}} action, where
$v$ is equal to \ls, which initially contains the input of process
$i$. The response consists of a snapshot $S_i \in
\vartheta(D)$ of the first IS object's shared memory vector, containing
the input values of some of the participating processes. In
particular, process $i$'s input is always contained in the output $i$
receives. Upon receiving the response $S_i$, process $i$ copies this
value to its \ls variable, after which it accesses the second IS
object by executing a {\mbox{{\it
writeread(\ls)$_{i,IS_2}$ \/}}}action. In effect, the output from the
first IS object is used as an input to the second.  Each non-failing,
participating process accesses {\em exactly} $k$ IS objects in
sequence in this manner, for some integer $k$, before deciding. The
number $k$ of IS objects accessed is the same for each non-failing,
participating process in any execution of the protocol.  Once a
process has received an output from the $k$-th IS object and stored
this value in the \ls variable, it applies a task specific decision
map $\mu$ to this value, stores the result in \ls, and halts. The \ls
variable now contains the process' decision value.

%It should be clear that each protocol in the IIS model can be
%characterized completely by the maximum number $n+1$ that can
%participate, the number $k$ of IS objects available, and the decision
%map $\mu$. We refer to the protocol obtained by fixing these
%parameters as $\cP_{(n,k, \mu)}$.

%We can specify the $\cP_{(n,k, \mu)}$ protocol using I/O automata
%\cite{automata} as follows. Each IS object is specified as in 
%figure ~\ref{ISspec}, and each process $i$ is specified as in Figure
%~\ref{IISprotocol}.  The protocol $\cP$ can then be specified by
%composing the automata for the processes with the IS object automata
%by matching up operations as follows. Assume that for each process
%$i$, the $j$-th IS object, $IS_x$, is connected to the $j$-th port on
%$i$, and for each IS object $IS_j$, the $i$-th process is connected to
%the $i$-th port on $IS_j$.  For each processor $i$ and IS object
%$IS_j$, we match up $i$'s and $IS_j$'s \inv and \ret actions.  The
%resulting protocol automaton is denoted $\cP_{(n,k)} = \{0, 1, \ldots,
%n; IS_1, IS_2,
%\ldots, IS_k\}$.

%The iterated immediate snapshot model has recently been shown to be
%computationally equivalent to regular atomic snaphot memory
%\cite{BGSIMM}, that is, each of the two models can be implemented by
%the other in a wait-free manner. 

%\begin{theorem}[Borowsky-Gafni]
%There exists a wait-free implementation of any protocol in the IIS
%model in the atomic snapshot model, and vice versa.
%\end{theorem}

%It remains an open question whether these implementations are optimal
%from a complexity-theoretic viewpoint.

\input{IISprotocol}

A stylized interconnection diagram of the $k$-shot IIS model is given
in Figure ~\ref{IISexample}. The diagram does not show any internal
actions, nor does it show the \start and \decide actions of the
processes.

\input{IISexample}

\subsection{The Non-Uniform Iterated Immediate Snapshot (NIIS) Model}
\label{subsection: NIIS}
In this subsection, we generalize the IIS model by introducing the {\em
Non-Uniform IIS (NIIS) model}. In the standard IIS model, the number
of IS objects available is finite, and the number of IS objects
accessed is fixed over all processes and all executions. The NIIS
model, however, assumes an infinite sequence $IS_D^{n+1},
IS_{\vartheta (D)}^{n+1}, IS_{\vartheta^2 (D)}^{n+1}, \ldots$ of IS
objects, denoted $IS_1, IS_2, IS_3, \ldots$. The number of IS objects
accessed by any two distinct processes in a given execution need not
be the same, and, moreover, the number of objects accessed by any
fixed process may vary from execution to execution. The motivation
behind this is to be able to model complexity more accurately, as will
be shown in later subsections.

Each protocol in the NIIS model is characterized by the maximum number
$n+1$ of processes that can participate, a predicate function $\tau:
\bigcup_{l = 0}^k \vartheta^l(D) \rightarrow \{{\tt true, false}\}$,
which each process applies to its \ls variable after each complete
\writeread operation to determine whether or not to decide, and a
decision map $\delta: \bigcup_{l = 0}^k \vartheta^l(D) \rightarrow D_O$,
where $D_O$ is an arbitrary data type, which we call the protocol's
{\em output data type}. We refer to the protocol obtained by fixing
these parameters as $\P$.

We can specify the $\P$ protocol using I/O automata
\cite{automata} As Follows. Each IS Object is specified as in 
Figure ~\ref{ISspec}, and each process $i$ is specified as in Figure
~\ref{fig: NIISprotocol}.  The protocol $\cP_{(n,\tau, \mu)}$ can then
be specified by composing the automata for the processes with the IS
object automata by matching up operations as follows. Assume that for
each process $i$, the $x$-th IS object, $IS_x$, is connected to the
$x$-th port on $i$, and for each IS object $IS_x$, the $i$-th process
is connected to the $i$-th port on $IS_x$.  For each processor $i$ and
IS object $IS_x$, we match up $i$'s and $IS_x$'s \inv and \ret
actions.  The resulting protocol automaton is denoted $\cP_{(n,k,
\mu)} =
\{0, 1, \ldots, n; IS_1, IS_2, \ldots, IS_k\}$.

The only difference between protocol $\P$ is the NIIS
model and a protocol in the IIS model is that after each complete
\writeread operation, each process checks whether it has reached a
final state by applying the predicate $\tau$ to the \ls variable. If
$\tau$ returns {\tt true}, the process executes a \finishi action and
halts. Otherwise, it accesses the next IS object as in the IIS model,
and so on. In fact, any protocol $\cP_{(n, k,\delta)}$ in the IIS model
is in fact equivalent to a protocol $\P$ in the NIIS
model, in which the predicate $\tau$ simply checks whether or not the
\ls variable is of type $\vartheta^k(D)$ or not.

A stylized interconnection diagram of the NIIS model is given in
Figure ~\ref{IISexample}. The diagram does not show any internal
actions, nor does it show the \start and \decide actions of the
processes

\input{NIISprotocol.tex}

\input{NIISexample.tex}

%The motivation behind introducing non-uniformity to the IIS model is
%to give a more accurate description of the complexity of solving
%decision tasks. The required number of steps taken by each
%participating process in order to solve a given decision task will not
%necessarily always be the same. It may well be that the necessary
%amount of computation will vary from process to process, from input
%value to input value, and indeed from execution to execution. In a
%uniform model such as the IIS model, every execution of a given
%protocol will involve the same number of steps.  


% For instance, it may be the case that only a proper subset of the
%processes need to do substantial work, while the rest do
%not. Similarly, it may be that some sets of inputs are harder to solve
%than others, thereby requiring more computation by all or some of the
%processes. 

%In a uniform model, the complexity of a given wait-free
%protocol on any input would be equal to the complexity of the worst
%possible execution on the worst possible set of inputs. For this
%reason, a uniform model would make a complexity theorem useless, since
%for example, in the case of a protocol solving the approximate
%agreement problem, Aspnes and Herlihy \cite{AH} have shown that, for
%any real number $t$, one can find a set of inputs that will require
%time $t$.

\subsection{Solvability of Decision Tasks}
\label{subsection: solvability}
In this subsection we specify more precisely what it means to solve a
decision task in the NIIS model. Since the IS and IIS models are
equivalent to special cases of the NIIS model, the definitions below
also apply directly to these models.

\begin{definition}
\label{def: execution solvability}
Suppose we are given a decision task $\dt2$, and an execution $\alpha$
of a protocol $\P$ in the NIIS model, with
corresponding input and output vectors $\vI$ and $\vO$,
respectively. Then $\P$ solves $\cD$ in $\alpha$ if
the following two conditions hold:

\begin{itemize}
\item No process takes an infinite number of steps in $\alpha$.
%\item $\vO$ is a prefix of some vector in $\gamma(\vI)$.
\item $\vO$ is a vector in $\gamma(\vI)$.
\end{itemize}
\end{definition}

Note that $\gamma(\vI)$ is prefix-closed by assumption, so the vector
$\vO$ does not necessarily contain an output value for each non-$\bot$
$i$ in $\vI$. Informally, this means that if $\P$ solves a task in an
execution $\alpha$, its partial outputs in any prefix $\alpha'$ of
$\alpha$ are also a valid solution to the task.

\begin{definition}
\label{def: protocol solvability}
A protocol $\P$ {\em solves} a decision task $\dt2$ if it solves it in
every execution $\alpha$.
\end{definition}

We are particularly interested in protocols that guarantee strong
fault-tolerance conditions. The failure model model we shall be
concerned with only involves stopping failures, that is, we assume
that processes may simply stop without warning. We do not consider
other, more complicated models, such as the Byzantine failure model,
in which processes may exhibit arbitrary behaviour.  In this paper,
we will focus on protocols with the property that any non-failing
process will eventually decide, independent of the progress of the
other processes;

\begin{definition}
\label{def: wait-free solvability}
A protocol $\P$ {\em solves} a decision task $\dt2$
{\em wait-free} if it solves it in every execution where up to $n$
processes can fail.
\end{definition}

\subsection{Complexity Measures for the IIS and NIIS Models}
\label{subsection: complexity}
We now define the complexity measures to be used for analyzing the
performance of protocols in the NIIS model. Since the IIS model is
equivalent to a special case of the NIIS model, these measures also
apply directly to the IIS model.

Let $\P$ be a protocol in the NIIS model solving a
given decision task $\cD$, let $I$ be an input vector, and let
$\alpha$ be any execution of $\P$ that starts with the
inputs in $I$. For all $i$, let $t_i$ be the number
of IS objects accessed by process $i$ in $\alpha$. Clearly, $t_i$ is
an integer. We first define the time complexity of the execution
$\alpha$.

\begin{definition}
\label{def: execution complexity}
The time complexity of $\alpha$, denoted $t_{\alpha}$, is $\max_i
t_i$, the maximum number of IS objects accessed by any process.
\end{definition}

We note that $t_{\alpha}$ is well-defined, since the number of
processes $n+1$ is finite. Moreover, by definition of the $\max$
function, $t_{\alpha}$ is an integer value. We use the definition
given above to define the time complexity of the protocol $\cP$ on the
input vector $\vI$.

\begin{definition}
\label{def: vector complexity}
The time complexity of $\P$ on $\vI$, denoted $t_{\vI}$, is
the supremum of the set {\mbox{{\it \{$t_{\alpha} \mid t_{\alpha}$ is
an execution starting from $\vI$\}\/}}}.
\end{definition}

%The complexity measure $t_I$ is well-defined, since, by Lemma
%~\ref{finite}, there are only finitely many executions that are
%possible for any given input vector $I$. Moreover, by definition of
%the $\max$ function, $t_I$ is always an integer value.

Finally, we define the complexity of a protocol $\P$ on a set of input
vectors $I$.

\begin{definition}
\label{def: vector set complexity}
The time complexity of $\P$ on $I$, denoted $t_I$, is
the supremum of the set {\mbox{{\it \{$t_{\alpha} \mid t_{\vI} \in I$\}\/}}}.
\end{definition}

The reason for preferring these simple, discrete complexity measures
over other, more elaborate measures such as real time, for instance,
is the highly regular structure of the NIIS model. We make the
assumption that each access to an IS object takes the same amount of
time, and do not worry about breaking up the time required to complete
each access to an IS object into subparts. Instead, we group the time
spent on invocation, response, and on local computation at the IS
object. This assumption is somewhat strong, as the presence of
asynchrony in our model will tend to introduce varying delays for each
access to an object. However, we believe that, as a first step towards
a complexity theory, this assumption is justifiable, as it allows for
complexity measures that are simple and easy to apply, and that have a
particularly nice topological representation, as we will see in
Section 3.

The motivation behind introducing non-uniformity to the IIS model is
to give a more accurate description of the complexity of solving
decision tasks. The required amount of computation in order to solve a
given decision task may vary from process to process, from input value
to input value, and indeed from execution to execution. In a uniform
model such as the IIS model, however, all processes will always take
the same number of steps in a given execution, and any process will
take the same number of steps in all executions in which it
participates. This property makes it impossible to construct a
satisfactory complexity theory in such a model. Thus, the introduction
of non-uniformity allows us to more accurately capture the complexity
of solving decision tasks.


% For instance, it may be the case that only a proper subset of the
%processes need to do substantial work, while the rest do
%not. Similarly, it may be that some sets of inputs are harder to solve
%than others, thereby requiring more computation by all or some of the
%processes. 

%In a uniform model, the complexity of a given wait-free
%protocol on any input would be equal to the complexity of the worst
%possible execution on the worst possible set of inputs. For this
%reason, a uniform model would make a complexity theorem useless, since
%for example, in the case of a protocol solving the approximate
%agreement problem, Aspnes and Herlihy \cite{AH} have shown that, for
%any real number $t$, one can find a set of inputs that will require
%time $t$.
%









