\section{Definition of Partitioning}
\label{section:partitioning}
\begin{myfig*}{figure:partition}{Figure (a) shows a fragment of a dataflow graph with 
a partition \{4,5,6\}. Figure (b) shows the reduced graph obtained
by coalescing the nodes in a partition to a single node. Figure (c)
shows the transformed graph corresponding to the partition. Two $S$
operators have been introduced to model the behavior of a thread.}
\illustration{fig6}[\hsize]
\vspace{-4ex}
\end{myfig*}

In section~\ref{section:introduction}, we informally defined the
partitioning problem as compiling a non-strict program into 
sequential threads. In this section, we formalize that intuition, by
defining partitioning as 
a transformation from a program in SP-TAC to another program in SP-TAC. 

\begin{definition} [Partitioning]
A partitioning of a block $b$ is a set of partitions $Q=\{q_1,\ldots,q_k\}$.
Each partition $q_j$ is a set of primitive operator nodes $n_1,\ldots,n_r$
of $b$.
\end{definition}
Note that the execution of a thread is very similar
to the execution of a primitive operator. The thread waits for
all its inputs to become available, performs some computation and
produces its outputs when all the computation in the thread
has terminated. Thus, executing a partitioned block
is similar to executing a block where the primitive nodes
in a partition are merged into a single node. Such
a graph is called the {\em reduced graph} corresponding to a partitioning.
Figure~\ref{figure:partition} shows a dataflow graph and its reduced
graph corresponding to a partitioning.


How can we
capture the semantics of merging primitive operators into a single 
node? We use a new primitive operator
(called {\em synchronization} or $S$ operator) to achieve this.
There is actually a {\em family} of such operators; each
operator in the family differs in the number of operands it accepts.
\begin{definition} [Synchronization Operator]
A synchronization operator $S_k$ is a primitive operator with
the following behavior.  For each $k \geq 1$,
\begin{eqnarray*}
S_k(v_1,\ldots,\bot,\ldots,v_k) & = & (\bot,\ldots,\bot) \\
S_k(v_1,\ldots,v_k) & = & (v_1,\ldots,v_k)
\end{eqnarray*}
\end{definition}
Intuitively, the operator ``waits'' for all its operands to become
values. Once this happens, the $S$ operator ``fires'' and acts
as an identity operator on each of its operands.

Using this operator, it is possible to express the behavior
of executing a partitioned block. We achieve this by defining a
{\em transformed block} that models the behavior of a partitioned
block. The formal definition is given  below.
\begin{definition} [Partitioning Transformation]
Given a block $b$ and a partitioning $Q$, the partitioned block $b_Q$ is
defined as follows. For each partition $q \in Q$ define:
\begin{enumerate}
\item{$I_q = \{n | (n \notin q) \wedge (m \in q) \wedge \: \mbox{edge} \: (n,m) \in b \}$}
\item{$O_q = \{m | (n \notin q) \wedge (m \in q) \wedge \: \mbox{edge} \: (m,n) \in b\}$}
\item{Add two synchronization operators $S_{|I_q|}$ and $S_{|O_q|}$ with inputs $I_q$ and $O_q$
respectively. Connect outputs of $S_{|I_q|}$ to nodes in $q$ that 
were connected to $I_q$, and outputs of $S_{|O_q|}$ to nodes not in $q$
that were connected to $O_q$.}
\end{enumerate}
\end{definition}
The idea behind the transformation is to use two synchronization operators to model the execution of a thread. One ``waits'' for all the inputs of a 
thread to become available. The other makes sure that all the computation
in a thread is fully performed before any other thread can use values
computed by this thread. This transformation ensures that the set of
primitive operators in a partition behave as though they are a single 
primitive operator. A compile-time ordering can now be generated
for each partition by a topological sort of the operators in
it. Our algorithms only produce the partitions for a block -- they
do not produce the actual threads. Figure~\ref{figure:partition} 
also shows a transformed dataflow graph using $S$ operators.

\subsection{Correctness of Partitioning}
When can we say that a partitioning of a block is {\em correct}? 
Informally, we would like partitioning to behave 
as any other compiler optimization. That is, it should not change
the ``meaning'' of the input program. As we are partitioning 
at the level of blocks, we say that a partitioning is correct
if the meaning of the block (given by its denotational semantics)
is preserved. Formally,
\begin{definition} [Correctness of Partitioning]
A partitioning $Q$ of a block $b$ in a program $pr$ is correct iff the 
partitioned block $b_Q$ satisfies the following property. For all $bve$:
\[{\cal E}^{pr}\ld b_Q \rd \: bve = {\cal E}^{pr} \ld b \rd \: bve \]
\end{definition}
This definition guarantees that we can use the partitioned block anywhere
in the program where the original block was used. However, this definition
is not directly verifiable at compile-time, it requires knowledge
of run-time values of the variables in a block. Later, we will show
a simpler syntactic criterion that guarantees the semantic correctness
of partitioning, and make use of the simpler criterion to design
our partitioning algorithms.

How can the partitioning of a block be incorrect? By the above
definition, a partitioning is incorrect if it returns values that
are different from those returned by the original block. Can 
the partitioning change the behavior of the block such that it
returns a different fully defined value (say 4) instead of 
the value 3? Intuitively, this
is not possible, as partitioning introduces only additional
synchronization constraints -- it does not change the value semantics
of the block. The only change that could happen is that a block,
instead of computing a value (say 3) on some set of inputs now computes
$\bot$ (\ie, deadlocks). It is possible to formalize this into the following theorem.
\begin{theorem} [Effect of Partitioning]
Let $b$ be a block in a program $pr$ and $b_Q$ its partitioned version of a partitioning $Q$. Then, for all $bve$:
\[{\cal E}^{pr}\ld b_Q \rd \: bve \sqsubseteq {\cal E}^{pr} \ld b \rd \: bve\]
\end{theorem}
The proof of this theorem involves establishing a correspondence between
the variables in $b$ with the variables in $b_Q$ and showing by fix-point
induction that the value of a variable in $b_Q$ is $\sqsubseteq$
the value of the corresponding variable in $b$.

In designing our algorithms in later sections, we assume 
that there is no cycle consisting
of primitive operators in our input blocks. If such a cycle exists, it is easy to show that all the nodes in the cycle will have undefined values, and 
hence these nodes do not affect the correctness of a partitioning.



