
%\documentstyle[11pt,zed]{csart}
\documentstyle{csart}

\begin{document}

\sloppy

\def\dotdot{\mathinner{\ldotp\ldotp}}

\def\parallel{\mathinner{\,\|\,}}

\def\cho#1#2#3{{\vcenter{\vbox{\hrule height.#3pt
		\hbox{\vrule width.#3pt height#2pt \kern#1pt
		\vrule width.#3pt}
		\hrule height.#3pt}}}}
\def\choi{\mathchoice\cho5{15}{48}\cho4{12}{45}\cho39{25}\cho26{21}}
\def\Choice{\mathop{\smash\choi\vphantom\sum}}

\def\choice{{\scriptstyle \Choice }}

\def\righti#1#2{{\mathclose>\llap{$#2\kern#1pt$}}}
\def\rightif{\mathchoice\righti{3}{\displaystyle|}\righti3{\textstyle|}\righti{2}{\scriptstyle|}\righti{2}{\scriptscriptstyle|}}
\def\lefti#1#2{{\mathopen<\llap{$#2\kern#1pt$}}}
\def\leftif{\mathchoice\lefti{2}{\displaystyle|}\lefti{2}{\textstyle|}\lefti{2}{\scriptstyle|}\lefti{1.5}{\scriptscriptstyle|}}

\newcommand{\proc}[1]{\mbox{\bf {#1}}}
\newcommand{\symbol}[1]{\mbox{\it {#1}}}
\newcommand{\function}[1]{\mbox{\it {#1}} \,}

\def\satisfies{\, \, \mbox {\bf sat}\, \,}

\def\lbag{[[}
\def\rbag{]]}

\def\ndchoice{\sqcap}
\def\suchthat{\, | \,}
\def\concat{\hat{\mbox{ }}}

\def\bif{\mbox{\bf if}\, \,}
\def\bthen{\, \, \mbox{\bf then}\, \,}
\def\belse{\, \, \mbox{\bf else}\, \,}

\section{Packet Delivery Systems}

     Let $M$ be a set of message types.  For any $m \in M$ the event
$m^O$ represents output of a message of type $m$, and $m^I$ represents
input of such a message.  $M^O$ denotes $\{m^O \suchthat m \in M\}$ and
$M^I$ denotes $\{m^I \suchthat m \in M\}$.  The process
\begin{eqnarray*}
\proc{T} (b) & = & \quad \quad \left( \Choice_{m \in M} \quad \, \, \, m^O \rightarrow
  \proc{T} (b \oplus \{m \mapsto b (m) + 1\}) \right) \quad \choice \\
             &   & \left( \begin{array}{c}
			    \ndchoice \\
			   {\scriptstyle m \in M \land b (m) \neq 0}
			  \end{array} m^I \rightarrow
  \proc{T} (b \oplus \{m \mapsto b (m) - 1\}) \right)
\end{eqnarray*}
represents a packet delivery system.
$b$ is a bag of items from $M$, and $\oplus$ is the overriding
operator (in {\em Z} style).  The alphabet of $\proc{T}$ is $M^O \cup M^I$.

     Define the set-valued functions
\begin{eqnarray*}
\function{pending-ins} (b, \symbol{tr}) & = &
  \left\{ m^I \suchthat m \in M \land
  (b (m) + \symbol{tr} \downarrow \{m^O\}) >
  \symbol{tr} \downarrow \{m^I\} \right\} \\
\function{pending-outs} (b, \symbol{tr}) & = &
  \left\{ m^I \suchthat m \in M \land
  (b (m) + \symbol{tr} \downarrow \{m^O\}) <
  \symbol{tr} \downarrow \{m^I\} \right\}
\end{eqnarray*}
on traces.

\subsection*{Theorem:}
\begin{eqnarray*}
\proc{T} (b) & \satisfies & S (b) (\symbol{tr}, \symbol{ref})
\end{eqnarray*}
where
\begin{eqnarray*}
S (b) (\symbol{tr}, \symbol{ref}) & = &
		     (M^O \cap \symbol{ref}) = \emptyset \land \\ & &
 \left( (\function{pending-ins}  (b, tr) \neq \emptyset ) \Rightarrow
 (\function{pending-ins}  (b, tr) \not\subset \symbol{ref}) \right) \land \\ & &
		    \function{pending-outs} (b, tr) = \emptyset
\end{eqnarray*}

\subsection*{Proof:}

Write
\begin{eqnarray*}
S^n (b) (\symbol{tr}, \symbol{ref}) & = &
  (\#\symbol{tr} < n) \Rightarrow S (b) (\symbol{tr}, \symbol{ref}).
\end{eqnarray*}
Noting $S^0 (b) (\symbol{tr}, \symbol{ref}) = \symbol{true}$,
the proof depends on showing that for any set of processes $\proc{X} (b)$
\begin{equation}
\left( \forall b \cdot \proc{X} (b) \satisfies S^n (b) \right) \Rightarrow
\left( \forall b \cdot \proc{F} (\proc{X}) (b) \satisfies
		S^{n + 1} (b) \right) \label{ftheorem}
\end{equation}
where $\proc{F}$ is the function whose fixed-point defines $\proc{T}$
according to the recursive equations above.  So
\begin{eqnarray*}
\proc{F} (\proc{X}) (b) & = &
\proc{F}^O (\proc{X}) (b) \quad \choice \quad \proc{F}^I (\proc{X}) (b)
\end{eqnarray*}
where
\begin{eqnarray*}
\proc{F}^O (\proc{X}) (b) & = &
  \Choice_{m \in M} \proc{F}_m^O (\proc{X}) (b) \\
\proc{F}^I (\proc{X}) (b) & = &
  \begin{array}{c}
    \ndchoice \\
   {\scriptstyle m \in M \land b (m) \neq 0}
  \end{array} \proc{F}_m^I (\proc{X}) (b)
\end{eqnarray*}
and
\begin{eqnarray*}
\proc{F}_m^O (\proc{X}) (b) & = &
  m^O \rightarrow \proc{X} (b \oplus \{m \mapsto b (m) + 1\}) \\
\proc{F}_m^I (\proc{X}) (b) & = &
  m^I \rightarrow \proc{X} (b \oplus \{m \mapsto b (m) - 1\})
\end{eqnarray*}
Providing equation \ref{ftheorem} obtains, the theorem follows from the
proof rule for recursion (CSP, pp125), because
\begin{eqnarray*}
S (b) (\symbol{tr}, \symbol{ref}) & = & 
\forall n \cdot S^n (b) (\symbol{tr}, \symbol{ref})
\end{eqnarray*}
Establishing equation \ref{ftheorem} requires the following algebraic
properties of the $\symbol{pending}$ functions
\begin{eqnarray}
\function{pending-ins} (b, \langle m^O \rangle \concat \symbol{tr}) & = &
  \function{pending-ins} (b \oplus \{m \mapsto b (m) + 1\}, tr) \label{prop1} \\
\function{pending-outs} (b, \langle m^O \rangle \concat \symbol{tr}) & = &
  \function{pending-outs} (b \oplus \{m \mapsto b (m) + 1\}, tr) \label{prop2}
\end{eqnarray}
and, if $b(m) \neq 0$,
\begin{eqnarray}
\function{pending-ins} (b, \langle m^I \rangle \concat \symbol{tr}) & = &
  \function{pending-ins} (b \oplus \{m \mapsto b (m) - 1\}, tr) \label{prop3} \\
\function{pending-outs} (b, \langle m^I \rangle \concat \symbol{tr}) & = &
  \function{pending-outs} (b \oplus \{m \mapsto b (m) - 1\}, tr) \label{prop4}
\end{eqnarray}
and
\begin{eqnarray}
\function{pending-ins} (b, \langle \rangle) & = & 
  \left\{ m^I \suchthat m \in M \land b (m) > 0 \right\} \label{prop5} \\
\function{pending-outs} (b, \langle \rangle) & = & \emptyset \label{prop6}.
\end{eqnarray}
Assuming the antecedent of \ref{ftheorem},
namely $\proc{X} (b) \satisfies S^n (b)$,
\begin{eqnarray*}
\proc{X} (b \oplus \{m \mapsto b (m) + 1\}) & \satisfies &
  S^{n + 1} (b) (\langle m^O \rangle \concat \symbol{tr}, \symbol{ref})
\end{eqnarray*}
follows directly from the definition of $S^n$ and properties
\ref{prop1} and \ref{prop2} above.  Hence, from the proof rule for
prefixing (CSP pp124)
\begin{eqnarray}
\proc{F}_m^O (\proc{X}) (b) & \satisfies &
\bif \symbol{tr} = \langle \rangle \bthen m^O \not\in \symbol{ref} \belse
S^{n + 1} (b) (\symbol{tr}, \symbol{ref}). \label{FOm}
\end{eqnarray}
Likewise, from properties \ref{prop3} and \ref{prop4}, if $b (m) \neq 0$
\begin{eqnarray}
\proc{F}_m^I (\proc{X}) (b) & \satisfies &
\bif \symbol{tr} = \langle \rangle \bthen m^I \not\in \symbol{ref} \belse
S^{n + 1} (b) (\symbol{tr}, \symbol{ref}). \label{FIm}
\end{eqnarray}
Equation \ref{FOm} and the proof rule for choice imply
\begin{eqnarray*}
\proc{F}^O (\proc{X}) (b) & \satisfies &
\bif \symbol{tr} = \langle \rangle \bthen
  \left( \forall m:M \cdot m^O \not\in \symbol{ref} \right) \belse
  S^{n + 1} (b) (\symbol{tr}, \symbol{ref}),
\end{eqnarray*}
or simply
\begin{eqnarray}
\proc{F}^O (\proc{X}) (b) & \satisfies &
\bif \symbol{tr} = \langle \rangle \bthen
  (M^O \cap \symbol{ref}) = \emptyset \belse
  S^{n + 1} (b) (\symbol{tr}, \symbol{ref}). \label{FO}
\end{eqnarray}
On the other hand, equation \ref{FIm} and the proof rule for
non-deterministic choice imply
\begin{eqnarray*}
\proc{F}^I (\proc{X}) (b) & \satisfies &
\bif \symbol{tr} = \langle \rangle \bthen \\ & &
  \left( \exists m:M \cdot b(M) > 0 \right) \Rightarrow
  \left( \exists m:M \cdot b(M) > 0 \land
    m^I \not\in \symbol{ref} \right) \belse \\ & &
  S^{n + 1} (b) (\symbol{tr}, \symbol{ref}).
\end{eqnarray*}
Using property \ref{prop5} of \symbol{pending-ins} this can be written as
\begin{eqnarray}
\proc{F}^I (\proc{X}) (b) & \satisfies &
\bif \symbol{tr} = \langle \rangle \bthen \nonumber \\ & &
  (\function{pending-ins} (b, \langle \rangle) \neq \emptyset) \Rightarrow
  (\function{pending-ins} (b, \langle \rangle) \not\subset \symbol{ref}) \belse
  \nonumber \\ & &
  S^{n + 1} (b) (\symbol{tr}, \symbol{ref}). \label{FI}
\end{eqnarray}
A final application of the proof rule for choice, combining \ref{FO} and
\ref{FI} and taking into account identity \ref{prop6}, establishes
equation \ref{ftheorem}.  This proves the theorem. $\Box$

\section{Eager Readers}

     Simplify the definitions of the previous section to eliminate
the references to $b$ (which is internal to the implementation of
the packet router):
\begin{eqnarray*}
\symbol{pending-ins} \, (\symbol{tr}) & = & \left\{ m^I \suchthat m \in M \land
  \symbol{tr} \downarrow \{m^O\} > \symbol{tr} \downarrow \{m^I\} \right\} \\
\symbol{pending-outs} \, (\symbol{tr}) & = & \left\{ m^O \suchthat m \in M \land
  \symbol{tr} \downarrow \{m^O\} < \symbol{tr} \downarrow \{m^I\} \right\}
\end{eqnarray*}
and put $\proc{T} = \proc{T} (\lbag \rbag)$.  So
\begin{eqnarray*}
\proc{T} & \satisfies & 
		     (M^O \cap \symbol{ref}) = \emptyset \land \\ & &
 \left( (\function{pending-ins}  (tr) \neq \emptyset ) \Rightarrow
 (\function{pending-ins}  (tr) \not\subset \symbol{ref}) \right) \land \\ & &
		    \function{pending-outs} (tr) = \emptyset
\end{eqnarray*}

      A process $\proc{C}$ for which $\alpha \proc{C} \supset \alpha \proc{T}$
is an {\em eager reader} if
\begin{eqnarray*}
\proc{C} &  \satisfies &
\left( (M^I \cup \symbol{ref}) = \alpha \proc{C} \land
\function{pending-outs} (\symbol{tr}) = \emptyset
\right) \Rightarrow \\
& & \left(\function{pending-ins} (\symbol{tr}) \neq \emptyset \land
(\function{pending-ins} (\symbol{tr}) \cap \, \symbol{ref}) = \emptyset \right).
\end{eqnarray*}
If an eager reader can't offer any events {\em other} than
inputs there must be at least one event in
$\function{pending-ins} (\symbol{tr})$,
and the process must be prepared to accept {\em any} event in
that set.  This requirement is weakened
slightly above---it need only apply if
no messages have been input before being output---a restriction
on traces which is imposed externally by a packet router.

\subsection*{Theorem:}

If \proc{C} is an eager reader
\begin{eqnarray*}
\proc{T} \parallel \proc{C} & \satisfies & \symbol{ref} \neq
  \alpha (\proc{T} \parallel \proc{C}).
\end{eqnarray*}
In other words, the combined process is deadlock-free.

\subsection*{Proof:}

     From the proof rule for parallel composition
\begin{eqnarray*}
\proc{T} \parallel \proc{C} & \satisfies & 
\exists X:\mbox{P}\alpha \proc{T} \cdot \exists Y:\mbox{P}\alpha \proc{C} \cdot
\symbol{ref} = X \cup Y \land \\ & &
  (M^O \cap X) = \emptyset \land
  \left( (P^I \neq \emptyset ) \Rightarrow
	  (P^I \not\subset X) \right) \land
  P^O = \emptyset \land \\ & &
  \left(
  \left( (M^I \cup Y) = \alpha{\proc{C}} \land
	  P^O = \emptyset \right) \Rightarrow
  \left( P^I \neq \emptyset \land
	 (P^I \cap Y) = \emptyset \right) \right)
\end{eqnarray*}
where 
\begin{eqnarray*}
P^I & = & \function{pending-ins} (\symbol{tr}) \\
P^O & = & \function{pending-outs} (\symbol{tr})
\end{eqnarray*}
Suppose $\proc{T} \parallel \proc{C}$ isn't deadlock free.
Then for some pair $(\symbol{tr}, \symbol{ref})$
we can find $X$ and $Y$ such that
$\symbol{ref} = X \cup Y = \alpha{\proc{C}}$ (because
$\alpha (\proc{T} \parallel \proc{C}) = \alpha \proc{C}$).
Since $X \subset (M^O \cup M^I)$ and $(M^O \cap X) = \emptyset $
we have $X \subset M^I$, so
$M^I \cup Y = \alpha{\proc{C}}$.  This means that the
antecedent of the final clause in the specification is satisfied, so
$ P^I \neq \emptyset \land (P^I \cap Y) = \emptyset $.
The first clause here implies, with an earlier clause, that
$P^I \not\subset X$, ie, there
is an element of $P^I$
which is not in $X$; but also, from the second clause, this
element can't be in $Y$.  This contradicts the assumption
that all events are in $X \cup Y$. $\Box$

\end{document}

