% -*- Mode: LaTeX -*-

\section{Semantics of Barriers}
\label{sec:dataflow}

We define the semantics of barriers by translating a kernel
program with barriers into another kernel program without barriers
where the termination of each control region is represented explicitly
as a signal.  To achieve this, we must precisely define the meaning of
termination for each construct in our kernel language and provide a
way of combining it in order to produce a joint termination signal.

\subsection{What is Termination?}

Let us consider the termination semantics of a simple parallel block.
We translate it into another block as follows:

\[\begin{array}{l}
\{\;x_{1}=E_{1}; \\
\;\;\cdots \\
\;\;x_{n}=E_{n}; \\
\;\tbx{in}\;x\;\}
\end{array} \Longrightarrow \begin{array}{lcl}
\{\;x_{1},s_{1} & = & \te{E_{1}}; \\
\;\;s'_{1} & = & s_{1}+\whnf{x_{1}}; \\
\;\;\cdots & & \\
\;\;x_{n},s_{n} & = & \te{E_{n}}; \\
\;\;s'_{n} & = & s_{n}+\whnf{x_{n}}; \\
\multicolumn{3}{l}{\;\tbx{in}\;x,s'_{1}+\cdots+s'_{n}\;\}}
\end{array}\]

An expression $E$ is translated as \te{E} which dynamically returns a
value along with an explicit termination signal defined over the range
$\{\bot,0\}$.  We use the weak head-normal form operator (\lbx{W}) to
wait for the arrival of the dynamic value and combine it with the
signal using the strict arithmetic operator $+$. The resulting signal
is again defined over the range $\{\bot,0\}$. All signals in a given
block are similarly combined into a single signal for the whole block.

Since every sub-expression is explicitly named in the kernel language,
the signal produced in the above manner ensures the termination of the
actual computation taking place within the block. But what about
references to free identifiers of the block? Some of these references
are used within the actual block computation and hence are
automatically included in its termination signal, but others are not.
For example, free identifiers present in a non-strict data constructor
or the free identifiers of a conditional branch that is not taken do
not directly contribute towards the result of the computation. 
Should we nonetheless explicitly include all such references as part
of the overall termination of the block?

There are two choices before us at this point, leading to two
different versions of the termination semantics.  Under
``data-driven'' semantics, we account for all the syntactically free
identifiers of a block as part of its computation, and hence always
include them in the block's overall termination.  Under
``demand-driven'' semantics, only those identifiers are included in a
block's termination which are demanded by the actual computation
taking place within the block.  Correspondingly, we obtain two
different translations for barriers that are described below and in
\sec{alter} respectively.

\subsection{Data-Driven Barrier Translation}

\begin{myfig*}{fig:dfbar}{Barrier Translation Rules based on
Data-Driven Eager Evaluation.}
\centering
$\begin{array}{lcl}
\multicolumn{3}{c}{\cbx{Expressions}} \\
\bbx{TE} & :: & \bx{Expression} \rightarrow
\bx{Expression}\times\bx{Signal Expression}\\[.1in]

\te{c}          & = & c,\hm 0 \\
\te{x}          & = & x,\hm \whnf{x} \\
\te{\ibx{PF}^{n}(X_{1},\ldots,X_{n})} & = &
\ibx{PF}^{n}(X_{1},\ldots,X_{n}),\hm
\whnf{X_{1}}+\cdots+\whnf{X_{n}} \\
\te{\tbx{Cond} \;(X, E_{1}, E_{2})} & = & 
\{\; y,s = \tbx{Cond} \;(X, \te{E_{1}}, \te{E_{2}}); \\
&   & \;\tbx{in}\; y,s+\whnf{z_{1}}+\cdots+\whnf{z_{n}} \;\} \\
\multicolumn{3}{l}{\bx{where}\hm z_{1},\ldots,z_{n} =
\fn{FV}{E_{1}}\cup\fn{FV}{E_{2}}} \\
\te{\lambda x_{1} \cdots x_{n}.\; E} & = & 
\lambda x_{1} \cdots x_{n}.\; \{\; y,s = \te{E} \\
&   & \hmmmm\hm\tbx{in}\;y,s+\whnf{x_{1}}+\cdots+\whnf{x_{n}}\;\}, 
\hm \whnf{z_{1}}+\cdots+\whnf{z_{n}} \\
\multicolumn{3}{l}{\bx{where}\hm z_{1},\ldots,z_{n} =
\fn{FV}{\lambda x_{1} \cdots x_{n}.\; E}} \\
\te{\tbx{Ap}(F,X)} & = & 
\{\; y,s = \tbx{Ap}(F,X) \;\tbx{in}\; y,s+\whnf{F}+\whnf{X} \;\} \\
\te{\{\;S^{\sibx{par}}\;\tbx{in}\;(X_{1},\ldots,X_{n})\;\}} & = &
\{\;S'^{\sibx{par}}\;\tbx{in}\;(X_{1},\ldots,X_{n},s)\;\} \\
\multicolumn{3}{l}{\bx{where}\hm S'^{\sibx{par}},s = \ts{S^{\sibx{par}}}} \\[.1in]
\multicolumn{3}{c}{\cbx{Statements}} \\
\bbx{TS} & :: & \bx{Statement} \rightarrow \bx{Statement}\times\bx{Signal Identifier}\\[.1in]
\ts{x_{1},\ldots,x_{n} = E} & = & (x_{1},\ldots,x_{n},s_{1} = \te{E}; \\
&   & s = s_{1}+\whnf{x_{1}}+\cdots+\whnf{x_{n}}),\hm s \\
\ts{\epsilon} & = & (s=0),\hm s \\
\ts{S_{1};\ldots;S_{n}} & = & (S'_{1};\ldots;S'_{n}; s=s_{1}+\cdots+s_{n}),\hm s \\
\multicolumn{3}{l}{\bx{where}\hm S'_{i},s_{i} = \ts{S_{i}} \hm 1\leq{}i\leq{}n} \\
\ts{S^{\sibx{par}}_{1} \;\tbx{---}\; S^{\sibx{par}}_{2}} & = & 
(S'^{\sibx{par}}_{1}; \\
&   & F = \lambda s.\{\;S'^{\sibx{par}}_{2} \;\tbx{in}\; y_{1},\ldots,y_{m},s_{2} \;\}; \\
&   & y_{1},\ldots,y_{m},s'_{2} = \tbx{Sap}(F,s_{1})),\hm s'_{2} \\
\multicolumn{3}{l}{\bx{where}\hm \begin{array}[t]{lcl}
S'^{\sibx{par}}_{i}, s_{i} & = & \ts{S^{\sibx{par}}} \hm 1\leq{}i\leq{}2 \\
y_{1},\ldots,y_{m} & = & \fn{BV}{S^{\sibx{par}}_{2}} \end{array}} \\
\ts{\tbx{I-store}(X_{0},X_{1},X_{2})} & = & 
(\tbx{I-store}(X_{0},X_{1},X_{2}); \\
&  & s = \whnf{X_{0}}+\whnf{X_{1}}+\whnf{X_{2}}),\hm s \\
\ts{\tbx{M-store}(X_{0},X_{1},X_{2})} & = & 
(\tbx{M-store}(X_{0},X_{1},X_{2}); \\
&  & s = \whnf{X_{0}}+\whnf{X_{1}}+\whnf{X_{2}}),\hm s
\end{array}$
\end{myfig*}

The data-driven identifier referencing scheme uses {\em Dynamic
Dataflow Graphs\/} as its compilation and execution model
\cite{Arvind86}. We may view a Kernel Id control region as a dataflow
graph, where each node represents a primitive operation and arcs
represent data-dependencies among them (see \fig{scope} (a)).  During
execution, \ibx{tokens} or \ibx{messages} carry run-time data values
along the arcs to their appropriate destinations.  The values of all
the free identifiers of a control region are explicitly sent as input
tokens to its dataflow graph, and it computes the values of its bound
identifiers as output tokens.  Note that in this data-driven model,
the values are either scalars or pointers to data objects residing in
the heap --- unevaluated expressions (\ibx{thunks}) are never treated
as values. Similarly, selecting components from heap objects directly
produces data values instead of thunks that would in lazy evaluation
remain unevaluated until their value is demanded.

\fig{dfbar} shows the rules for transforming Kernel Id language
constructs such that their termination events become explicit.  We
provide two sets of translation rules. \te{} translates a kernel
language expression $E$ into a new composite expression that computes
the termination signal of the original expression $E$ in addition to
its value. \ts{} translates a kernel language statement $S$ into a
parallel statement group $S'$ and a signal identifier $s$ that is
bound to a signal expression representing the termination of $S$.
Additional syntactic properties of the given expression or the
statement may also be used, such as the free identifiers ($\ibx{FV}$)
or the bound identifiers ($\ibx{BV}$) of an expression or a statement.

In all the rules shown in \fig{dfbar}, we maintain the invariant that
the weak head-normal forms of all the free identifiers statically
present within a construct are implicitly or explicitly collected into
its dynamic signal. This is reflected in the rules for identifiers,
primitive function applications, conditionals, $\lambda$-expressions,
and user-defined function applications. For strict primitives such as
$+$ this may be redundant, but it keeps the semantics intuitive and
{\em compositional\/}, \ie, termination of a program term (expression
or statement) depends solely on the termination of its sub-terms.

The translation rule for function application shows that we not only
wait for the arrival of the operator and the operand, but also the
dynamic termination signal from the function application itself. The
rule for $\lambda$-expressions correspondingly translates each
function body to return a signal upon its termination.  This body
signal waits for the arrival of all the arguments of the function,
thereby ensuring that unused or non-strict arguments are also
collected before signaling the termination of the function
application.

It may seem redundant to collect the weak head-normal form of a
function argument at the application site when we already collect it
within the body of the function. However, collection at the
application site is necessary because any of these sites could be a
partial application. In that case, the arrival of the argument
contributes towards building the partial application closure rather
than a executing a function body. Building a closure is a
resource-consuming computation and therefore its termination must be
tracked independently.

Finally, the translation of a barrier encloses its post-region in a
$\lambda$-expression which is applied to the accumulated termination
signal of its pre-region using the strict application primitive
\tbx{Sap}. This prevents the initiation of the computation below the
barrier until after the computation above the barrier has terminated.

It is easy to see that the data-driven termination semantics presented
above provides precise control over both resource management and
scheduling of side-effects, as discussed in \sec{uses}. The signal
generation and composition rules shown in \fig{dfbar} ensure that the
production of a termination signal from a control region implies that
all its input values have arrived and that the entire computation
within that region including side-effects has terminated.  Therefore,
any resources used during this computation may be safely released.
