\subsubsection{Synchronizing switch correctness}
\label{correct-sect}

% Argue for correctness
From Section~\ref{patterns-sect}, we know that the routes of each
phase use all links of the machine once and only once. Therefore, one
phase uses all of the machine's network bandwidth.  If the AAPC phases
are separated by global synchronizations, we know that each 
phase uses the machine's network bandwidth optimally.
Given AAPC phases where each node starts in the same phase,
a sufficient condition for optimality is
\begin{condition}
A message from a later phase will not block progress of a message from
an earlier phase. 
\label{cond1}
\end{condition}
By Condition~\ref{cond1}, the lowest numbered active phase across the
machine is never blocked, so nodes participating in this
phase can send and receive data at the network rate. Therefore, 
Condition~\ref{cond1} is sufficient to ensure optimal performance.

Now we prove that replacing the global synchronization with the
synchronizing switch preserves Condition~\ref{cond1} and therefore
optimality.
\begin{lemma}
\label{sync-lem2}
In one iteration of the synchronizing switch, exactly one message passes over
each input link.
\end{lemma}
This is true by construction of the synchronizing switch. The
NotInMessage stop condition prevents more than one message from
passing over an input link in each phase.

The construction in Section~\ref{patterns-sect} shows that exactly one
message is sent over each link in each phase, and
Lemma~\ref{sync-lem2} says that each node processes exactly one
message over each input link in each phase.  Since all nodes start in
the same AAPC phase, each node must be processing messages from the
same phase over its four input links.  Since each node processes
messages from the phases in order, Condition~\ref{cond1} must hold.
Therefore, the synchronizing switch preserves optimality.

%\end{document}
