
\section{Discussion}

\subsection{Working with deterministic models}

     The example given in the previous section was sufficiently simple
that we could afford to simply combine the non-deterministic
delivery system with the IO buffer system in one step, then
immediately conceal internal events in the composite model
and verify a simulation from the result
to a model of the specification.

     In general it may be more convenient to go through intermediate
simulations (``refinements'') between the composition step and the
concealment (``abstraction'') step.  Moreover, in some of the steps it
may be possible to ignore the non-determinism in one or more of the original
components.  Note
\begin{displaymath}
 P = P \parallel P^{\scriptsym{det}}
\end{displaymath}
where $P^{\scriptsym{det}}$ is the deterministic process with the same
traces as $P$.  In terms of our transition models, it can be represented
by the TM obtained from any generalised transition model standing for $P$
by ignoring any $U$, $V$ or $W$ fields.  Evidently, life is simpler
if one can work with this system rather than the original non-deterministic
one.  Suppose $P$ is being composed with some system $Q$.  According to
the observation above, if we can show
\begin{displaymath}
P^{\scriptsym{det}} \parallel Q \sqsupseteq R
\end{displaymath}
then it follows by monotonicity of $\parallel$ that
\begin{displaymath}
P \parallel Q \sqsupseteq P \parallel R
\end{displaymath}
The value of this theorem is that $R$ may be more tractable than $Q$,
so that composing it with the full $P$ is simpler than direct use
of $R$.  On the other hand, the establishing the precondition
is simplified because $P^{\scriptsym{det}}$ is a deterministic process.
For example, in the virtual channel example of section \ref{sec:virtual},
composing the deterministic part of the delivery system with the
IO buffer system yields the TM $(A^{\scriptsym{IO}}, T^{\scriptsym{ROUT}})$.
Then, by a straightforward TM to TM simulation one can show equivalence
of this system to the more concise deterministic system
\begin{displaymath}
\begin{array}{l}
\begin{array}{c} \Parallel \\ c \in \symbol{Chans} \end{array} c:\symbol{IOBUF}
\end{array}
\end{displaymath}
where
\begin{displaymath}
\symbol{IOBUF} = \mu X \truethat \Choice_x p.x \rightarrow f^O.x \rightarrow
				\Choice_y f^I.y \rightarrow q.y
				\Choice_z r.z \rightarrow b^O.z
				\Choice_w b^I.w \rightarrow s.w \rightarrow X
\end{displaymath}
Now this system is combined with the full non-deterministic model
for the router, and the rest of the calculation can proceed essentially
as before.
In this case the simplification obtained in this way is not enormous
(which is why this logical step was skipped in the earlier presentation).
In general, there may be significant advantages to be gained
by organising the proof in this way
\footnote{ In passing, note that the clarity of the proof in section
\ref{sec:virtual} would also have
benefitted from inserting a further intermediate simulation between
composition with
the non-deterministic router and concealment of events---eliminating
many redundant states before rather than after concealment}.

\subsection{Eagerness}

     Low-level message delivery systems for multi-processors
often come with a guarantee that they are ``deadlock-free, provided the
user processes are eager readers''.  The intuitive idea
of a process being an ``eager reader'' is that it never refuses to
accept any message that has been sent to it (or, at least, it only
defers this acceptance for a bounded time, while it may be engaging
in some internal activity).

     Intuitively, eager readership seems to be an important concept.
In this section we will try to give a more precise characterisation of
eagerness.  In this analysis, the slightly mysterious promise about
deadlock freedom quoted in the previous paragraph could be
replaced by: ``the message delivery system is {\em effectively
deterministic} provided the system of user processes is an
eager reader''
\footnote {The replacement, here, of individual ``user processes''
by the system as a whole recognises the fact that eagerness
must be a global property---there is no
implication that an individual process should always be waiting
to accept notional messages which haven't actually been sent to it
(by one of the other user processes).}.
%The meaning of ``effective determinism'' will
%be explained below.  Here, ``deadlock-freedom''
%is regarded simply as a promise that the router meets the
%liveness specification of section \ref{routers}.  It is independent
%of the eagerness or otherwise of the user system.

     So, suppose $\function{pending} (\symbol{tr})$ is a function on
traces which returns the set of message-input events the delivery
system {\em may} engage in (according to its traces) after the
system as a whole has executed a trace $\symbol{tr}$.  In the bag model
this is just
\begin{displaymath}
\function{pending} (\symbol{tr}) = \{\setvar{m}^I \suchthat 
  \symbol{tr} \downarrow \{\setvar{m}^O\} >
  \symbol{tr} \downarrow \{\setvar{m}^I\} \}
\end{displaymath}
Now, if $P$ is the message delivery system,
and $Q$ is the system
of user processes, $Q$ is an eager-reading system if it satisfies
\begin{displaymath}
\forall s:\function{traces} (P \parallel Q) \truethat
\forall X:\function{refusals} (Q / s \rhd \alpha Q) \truethat
\function{pending} (s) \cap X = \emptyset
\end{displaymath}
This says that $Q$ never refuses any pending messages
(***remark on appearance of P || Q here***).  Now one
can easily proof the following quite striking theorem
\begin{theorem} If $P'$ is any process with the same traces as $P$ which
satisfies the liveness property in section \ref{sec:bag}, then
\begin{displaymath}
(P' \parallel Q) \setminus \{\setvar{m}^I \} =
(P \parallel Q) \setminus \{\setvar{m}^I \}
\end{displaymath}
\end{theorem}
In particular one can take $P' = P^{\scriptsym{det}}$.  So if $Q$
is an eager reader we can replace the message delivery system
by its deterministic counterpart, and after the abstraction
step of hiding message inputs, we end up with the same process
as if we had used the full non-deterministic definition of $P$.

     This appears to be a powerful result.  It seems obvious
that the system of independent $\symbol{IOBUF}$ processes is an eager-reading
system, so we can just hide inputs in that model
without ever worrying about
acceptances of the message delivery system, and get the proof
that the system meets it's specification that much more easily.

     In general, unfortunately, proving that a system has the
eager readership property may itself be non-trivial, and the
simplification implied here may be slightly illusory.  Still,
this is a proof technique which deserves investigation.

     Incidentally, we have only given the simplest possible definition
of eagerness here, in the context of a bag-like message router.
Needless to say, the idea can be generalised in several directions, and
similar theorems proved.

\subsection{More structured models of message-delivery systems}

     The ``bag'' model of a message delivery system is useful for
illustrative purposes, but it doesn't capture much of the structure
of a typical message delivery systems.  There is no inherent idea
of locality---messages are inserted into the system and removed from
it without any association with a point (in ``processor space'')
from which they are originating or to which they are being delivered.  Also,
many delivery systems provide guarantees on sequencing of messages
which are passed ``between the same points''---messages emerge
from the delivery system in order which they inserted.

     These shortcomings can be addressed by adding ``ports'' to
the delivery system.  Logical channels exist between any pair of
ports, and message delivery across any particular channel is
sequence-preserving.  Each port may be associated with a particular
processor (there may be one or many ports per processor)

     The alphabet of the new system is
\begin{displaymath}
\alpha{\symbol{Msys}} = \{\underline{M}^O.\underline{v} \suchthat \underline{M}
     \in \symbol{Ports}^2 \land \underline{v} \in \symbol{Messages}, \quad
		         \underline{M}^I.\underline{v} \suchthat \underline{M}
     \in \symbol{Ports}^2 \land \underline{v} \in \symbol{Messages}, \quad
\end{displaymath}
where $\symbol{Ports}$ is the space of ports.
The traces associated with the system now satisfy
\begin{displaymath}
\forall (P, Q) : \symbol{Ports}^2 \truethat
				 \symbol{tr} \downarrow \{ (P, Q)^O \} >
                                 \symbol{tr} \downarrow \{ (P, Q)^I \}
\end{displaymath}
In fact, so far as traces are concerned, this is the strongest
specification needed to yield a workable message delivery system.
One can also give a state transition model of this trace set.
The state space is
\begin{displaymath}
\symbol{Mstat} = \symbol{Ports}^2 \rightarrow \symbol{Values}^*
\end{displaymath}
A state $B$ in this space associates a non-negative value with each
message type---$B (v)$ is the number of messages of type $v$ presently
in transit.  The transition function is
\begin{eqnarray*}
T^{\scriptsym{Msys}} (M) & = &
    \{ ((\setvar{P}, \setvar{Q})^O.\setvar{v} \mapsto
	M \oplus ((\setvar{P}, \setvar{Q}) \mapsto 
	M (\setvar{P}, \setvar{Q}) \concat \langle \setvar{v} \rangle)),
	\\ && \,\,\,\,
       ((\setvar{P}, \setvar{Q})^I.\setvar{v} \mapsto
	M \oplus ((\setvar{P}, \setvar{Q}) \mapsto 
	M (\setvar{P}, \setvar{Q})'))
	M (\setvar{P}, \setvar{Q})') \not= \langle \rangle \land
	\setvar{v} = M (\setvar{P}, \setvar{Q})_0 \}.
\end{eqnarray*}

