% -*- Mode: LaTeX -*-

\section{A Kernel Language}
\label{sec:kernel}

In this section we provide a framework for discussing the semantics
of barriers. We present a small parallel language and its rewrite rule
semantics.

\subsection{Language Syntax}

\begin{myfig}{fig:lang}{The Syntax of Kernel Expression Language.}
\centering
$\begin{array}{lcl}
c                 & \in & \bx{Constant} \\
{F,t,x,y,z\ldots} & \in & \bx{Identifier} \\
{\ibx{SE},X,Y,Z,\ldots} & \in & \bx{Simple Expression} \\
E                 & \in & \bx{Expression} \\
S                 & \in & \bx{Statement} \\
\ibx{PF}^{n}      & \in & \bx{Primitive Fn. with $n$ arguments}\\[.1in]


\bx{Constant} & ::= & \ibx{Integer} \mid \ibx{Float} \mid \ibx{Boolean} \\
\ibx{SE}      & ::= & \bx{Identifier} \mid \bx{Constant} \\
\ibx{PF}      & ::= & + \mid - \mid \cdots \mid \tbx{hd} \mid \tbx{tl}
                      \mid \tbx{Cons} \mid \cdots \\
              &     & \mid \tbx{Alloc} \mid \tbx{I-fetch} \mid \tbx{M-take} \mid \cdots \\
E             & ::= & \ibx{SE} \mid \ibx{PF}^{n}(X_{1},\ldots,X_{n}) \\
              &     & \mid \tbx{Cond} \;(X,E_{1},E_{2}) \mid \lambda x_{1} \cdots x_{n}.\; E \\
              &     & \mid \tbx{Ap}(F,X) \mid \tbx{Fap}^{n}(F^{n},X_{1},\ldots,X_{n}) \\
              &     & \mid \tbx{Sap}^{n}(F^{n},X_{1},\ldots,X_{n}) \\
              &     & \mid \tbx{Pap}^{i}(F^{n},\ul{n-i},X_{1},\ldots,X_{i}) \mid \bx{Block} \\
\bx{Block}    & ::= & \{\;S^{\sibx{par}}\;\tbx{in}\;(X_{1},\ldots,X_{n})\;\} \\[.1in]

S^{\sibx{par}} & ::= & S_{1};\ldots;S_{n} \mid \epsilon \\
S^{\sibx{seq}} & ::= & (S^{\sibx{par}}_{1} \;\tbx{---}\; S^{\sibx{par}}_{2}) \\
S              & ::= & \bx{Binding} \mid \bx{Command} \mid S^{\sibx{seq}} \\
\bx{Binding}   & ::= & x_{1},\ldots,x_{n} = E \\
\bx{Command}   & ::= & \tbx{I-store}(X,I,Z) \mid \tbx{M-put}(X,I,Z)
\end{array}$
\end{myfig} 

\fig{lang} shows the grammar of our kernel expression language. The
grammar ensures that every sub-expression of a computation is named
with an identifier. This is extremely desirable in order to be able to
express and preserve sharing constraints among data-structures. 

Aside from the usual arithmetic primitives, the strict primitives
\tbx{hd} and \tbx{tl} are used to manipulate lists. \tbx{Cons} is the
only non-strict primitive function: it returns the allocated
\tbx{Cons}-cell before it is completely filled. The primitive function
\tbx{Alloc} is used to allocate either I-Structure or M-Structure
memory block of size $n$.  The type-checker ensures that this memory
is used consistently.

There are several forms of application expressions in \fig{lang}.
\tbx{Ap} is the general apply operation, $\tbx{Fap}^{n}$ is a
full-arity application of a known function to $n$ arguments,
$\tbx{Sap}^{n}$ denotes strict application, and $\tbx{Pap}^{i}$
denotes a partial application of a function to $i$ arguments
accumulated within the closure.\footnote{We will omit the arity
superscripts when they are obvious.} The latter three forms are
generated during compiler optimizations or as intermediate results
during rewriting.  The language also provides nested
$\lambda$-expressions that may contain free identifiers, and a block
construct that controls lexical scoping and enables precise sharing of
sub-expression values.

The kernel language allows several identifiers to be bound at once in
a multiple-value binding. The number of multiple-values being returned
from the right-hand-side expression must match the number of
identifiers being bound on the left-hand-side.  Finally, a group of
statements separated by semi-colons forms a parallel control region.
Two parallel control regions may be sequentialized using a barrier.

\subsection{Weak Head-Normal Forms}

Typically, a non-strict program computes {\em Weak Head-Normal
Forms\/} as its answer. An expression is said to be in normal form if
it cannot be simplified any further, while an expression is said to be
in weak head-normal form as soon as its top-level structure becomes
``stable''. Under eager evaluation, an expression has to be in weak
head-normal form before it can be passed around as an argument, stored
into data-structures, or returned as a result from a function.
Thus weak head-normal forms provide an exact characterization of
the run-time \ibx{values} under eager evaluation.

\begin{myfig}{fig:whnf}{Definition of Weak Head-Normal Forms (Values).}
\centering
$\begin{array}{lcl}
\ibx{WHNF}  & \in & \bx{Weak Head-Normal Form} \\
\bx{Signal} & \in & \{\bot,0\} \\
\lbx{W}     & :: & \bx{Expression} \rightarrow \bx{Signal} \\[.1in]

\ibx{WHNF}  & ::= & \bx{Constant} \mid \tbx{Cons}(X,Y) \mid \tbx{Alloc}(\ul{n}) \\
            &     & \mid \lambda x_{1} \cdots x_{n}.\; E \\
            &     & \mid \tbx{Pap}(F^{n},\ul{n-i},X_{1},\ldots,X_{i}) \\[.1in]

\whnf{c}    & =  & 0 \\
\whnf{x} & = & \whnf{E} \hmm \bx{Where $x$ is bound to $E$} \\
\whnf{\tbx{Cons}(X,Y)} & = & 0 \\
\whnf{\tbx{Alloc}(E)} & = & \whnf{E} \\
\whnf{\lambda x_{1} \cdots x_{n}.\; E} & = & 0 \\
\multicolumn{3}{l}{\whnf{\tbx{Pap}(F^{n},\ul{n-i},X_{1},\ldots,X_{i})} = 0} \\
\whnf{E} & = & \bot \hmmmm \bx{Otherwise} 
\end{array}$
\end{myfig} 

The weak head-normal forms or values recognized in our language are
shown in \fig{whnf}. Constants like integers, floats, booleans and
underlined expressions (\eg, $\ul{n-i}$) constitute literal values. An
allocated data-structure such as a \tbx{Cons}-cell or an \tbx{Alloc}
memory block is also considered to be a value even if its components
are not yet filled. Note that the size of the memory block must be
known for the allocation to take place.  $\lambda$-expressions are
considered to be in weak head-normal form because we do not reduce
inside the body unless it is fully applied.  In addition, partial
applications (\tbx{Pap}) are also considered to be in weak head-normal
form because they also represent functions, albeit produced \via
currying.

It is not possible to test algorithmically within the language whether
a given expression is in weak head-normal form or not without
destroying the confluence property. An expression may not be in weak
head-normal form at one point, but may become so after some
evaluation. However, we can add to the language a monotonic primitive function
$\whnf{E}$ defined over the range $\{\bot,0\}$ without
destroying confluence.  This function produces the signal 0 if the
given expression is in weak head-normal form and produces $\bot$
otherwise (see \fig{whnf}).  We use this primitive extensively in
defining both the value semantics of the kernel language discussed
below and the termination semantics of barriers described in
\sec{dataflow}.

\subsection{Rewriting Semantics}
\label{sec:rules}

\begin{myfig}{fig:rules}{Rewrite Rules for the Kernel Language.}
\centering
\begin{tabular}{@{}c}
\multicolumn{1}{@{}l}{\bbx{$\delta$ Rules:}} \\
\stmt{+(\ul{m},\ul{n})\longrightarrow\ul{+(m,n)}} \\
$\cdots$ \\ \\
\multicolumn{1}{@{}l}{\bbx{Cond Rules:}} \\
\stmt{\tbx{Cond}\;\tbx{True}\;(E_{1},E_{2})\longrightarrow{}E_{1}}\\
\stmt{\tbx{Cond}\;\tbx{False}\;(E_{1},E_{2})\longrightarrow{}E_{2}}\\ \\
\multicolumn{1}{@{}l}{\bbx{List Rules:}} \\
\inference{\stmt{X=\tbx{Cons}(Y,Z)}\hmm\stmt{\whnf{Y}=0}}%
          {\stmt{\tbx{hd}(X)\longrightarrow{}Y}}\\[.2in]
\inference{\stmt{X=\tbx{Cons}(Y,Z)}\hmm\stmt{\whnf{Z}=0}}%
          {\stmt{\tbx{tl}(X)\longrightarrow{}Z}}\\ \\
\multicolumn{1}{@{}l}{\bbx{Apply Rules:}} \\
\inference{\stmt{F=\lambda X_{1} \cdots X_{n}.\; E}}%
          {\stmt{\tbx{Ap}(F,X) \longrightarrow \tbx{Pap}(F,\ul{n-1},X)}}\\[.2in]
\inference{\stmt{F=\tbx{Pap}(F',\ul{n},X_{1},\ldots,X_{i})\hmm n>1}}%
          {\stmt{\tbx{Ap}(F,X) \longrightarrow
                 \tbx{Pap}(F',\ul{n-1},X_{1},\ldots,X_{i},X)}}\\[.2in]
\inference{\stmt{F=\tbx{Pap}(F',1,X_{1},\ldots,X_{i})}}%
          {\stmt{\tbx{Ap}(F,X) \longrightarrow \tbx{Fap}(F',X_{1},\ldots,X_{i},X)}}\\[.2in]
\inference{\stmt{F=\lambda X_{1} \cdots X_{n}.\; E}}%
          {\stmt{\tbx{Fap}(F,Y_{1},\ldots,Y_{n}) \longrightarrow
                 (\rb{E})[Y_{1}/X_{1},\ldots,Y_{n}/X_{n}]}} \\ \\
\multicolumn{1}{@{}l}{\bbx{Strict Apply Rule:}} \\
\inference{\stmt{\whnf{X_{1}}+\cdots+\whnf{X_{n}}=0}}%
          {\stmt{\tbx{Sap}(F,X_{1},\ldots,X_{n}) 
                 \longrightarrow \tbx{Fap}(F,X_{1},\ldots,X_{n})}} \\[.2in]
\multicolumn{1}{@{}l}{\bbx{I-Structure Rules:}} \\
\inference{\stmt{\tbx{I-store}(X,\ul{i},Z)}\hmm\stmt{\whnf{X}=0\hm\whnf{Z}=0}}%
          {\stmt{\tbx{I-fetch}(X,\ul{i})\longrightarrow Z}} \\[.2in]
\inference{\stmt{\tbx{I-store}(X,\ul{i},Z)}\hmm\stmt{\whnf{X}=0\hm\whnf{Z}=0\hm\whnf{Z'}=0}}%
          {\stmt{\tbx{I-store}(X,\ul{i},Z')\longrightarrow \top}} \\ \\
\multicolumn{1}{@{}l}{\bbx{M-Structure Rules:}} \\
\inference{\stmt{\whnf{X}=0\hm\whnf{Z}=0}}%
          {\stmt{\tbx{M-put}(X,\ul{i},Z);\;Y=\tbx{M-take}(X,\ul{i})\longrightarrow Y=Z}}\\[.2in]
\inference{\stmt{\whnf{X}=0\hm\whnf{Z}=0\hm\whnf{Z'}=0}}%
          {\stmt{\tbx{M-put}(X,\ul{i},Z);\;\tbx{M-put}(X,\ul{i},Z')\longrightarrow \top}}
\end{tabular}
\end{myfig}

\fig{rules} shows the rewrite rules that apply to kernel language
terms without barriers. We make extensive use of intermediate
identifiers in order to preserve sharing of sub-expressions.
This system therefore represents a Graph Rewriting System
\cite{Ariola94}. 

We use the \lbx{W} operator to express additional conditions under
which a particular rewrite rule applies. For example, the \bbx{List}
rules (\tbx{hd} and \tbx{tl}) fire only when the \tbx{Cons}-cell is
available and the component being selected becomes a value. The latter
condition reflects the data-driven nature of eager evaluation. In
contrast, under lazy evaluation, selecting a component from a
\tbx{Cons}-cell would immediately return a \ibx{thunk} which is
subsequently evaluated to a value only if necessary. From
the point of view of
denotational semantics, these two evaluation strategies
are equivalent, but they yield very different dynamic resource
utilization and termination characteristics.

Note that all the \bbx{Apply} rules except the \tbx{Sap} rule are {\em
non-strict\/}: they fire even if the applied arguments
have not yet become a value.  In case of \tbx{Sap}, we use the \lbx{W}
operator to wait explicitly for the arrival of all the arguments
before proceeding with the application. In other cases, partial
applications are created whenever a function is applied to a number of
arguments that is less than its arity. Once all the arguments have
been syntactically applied, the function body is instantiated,
replacing $\lambda$-bound parameters by actual arguments.  The
operation \rb{E} simply creates a new copy of the $\lambda$-body by
renaming all its bound identifiers to new identifiers.

The rules for I-Structures and M-Structures implement their respective
protocols. The rules for I-Structures show that all \tbx{I-fetch}
operations to a known location must wait until an \tbx{I-store}
operation succeeds in storing a value to the same location. Two
\tbx{I-store} operations to the same location take the program into an
inconsistent state ($\top$). The M-Structure rules are similar, except
that each \tbx{M-put} operation non-deterministically matches up with
one \tbx{M-take} operation within the same control region. Two
simultaneous \tbx{M-put} operations take the program into an
inconsistent state.

\begin{myfig}{fig:canon}{Canonicalization Rules.}
\centering
\begin{tabular}{@{}c}
\multicolumn{1}{@{}l}{\bbx{Block Flattening Rule:}} \\
\stmt{\begin{array}{l}
\{\;x = \{\begin{array}[t]{l}
y_{1}=E'_{1}; \\
\cdots \\
y_{m}=E'_{m}; \\
\tbx{in}\;y\;\};\end{array} \\
\;\;x_{1}=E_{1}; \\
\;\;\cdots \\
\;\;x_{n}=E_{n}; \\
\;\tbx{in}\;z\;\}\end{array} \longrightarrow 
\begin{array}{l}
\{\;x = y; \\
\;\;y_{1}=E'_{1}; \\
\;\;\cdots \\
\;\;y_{m}=E'_{m}; \\
\;\;x_{1}=E_{1}; \\
\;\;\cdots \\
\;\;x_{n}=E_{n}; \\
\;\tbx{in}\;z\;\}\end{array}} \\ \\
\multicolumn{1}{@{}l}{\bbx{Substitution Rules:}} \\
\stmt{\begin{array}{@{}l}
\{\;x_{1}=E_{i};\cdots;x=c;\cdots;x_{n}=E_{n};\;\tbx{in}\;z\;\}
\longrightarrow \hmm(c\neq\odot)\\
\hm\{\;x_{1}=E_{i}[c/x];\cdots;x_{n}=E_{n}[c/x];\;\tbx{in}\;z[c/x]\;\} \\[.1in]
\{\;x_{1}=E_{i};\cdots;x=y;\cdots;x_{n}=E_{n};\;\tbx{in}\;z\;\} 
\longrightarrow \hmm(x\neq{}y)\\
\hm\{\;x_{1}=E_{i}[y/x];\cdots;x_{n}=E_{n}[y/x];\;\tbx{in}\;z[y/x]\;\}
\end{array}} \\ \\
\multicolumn{1}{@{}l}{\bbx{Degenerate Cycle Rule:}} \\
\stmt{\begin{array}{@{}l}
\{\;x_{1}=E_{i};\cdots;x=x;\cdots;x_{n}=E_{n};\;\tbx{in}\;z\;\} \longrightarrow \\
\hm\{\;x_{1}=E_{i}[\odot/x];\cdots;x=\odot;\cdots;x_{n}=E_{n}[\odot/x];\;\tbx{in}\;z[\odot/x]\;\}
\end{array}} \\ \\
\multicolumn{1}{@{}l}{\bbx{Blowup Rule:}} \\
\stmt{\{\;x_{1}=E_{i};\cdots;x=\top;\cdots;x_{n}=E_{n};\;\tbx{in}\;z\;\} \longrightarrow \top}
\end{tabular}
\end{myfig}

\fig{rules} shows only the reduction rules that perform useful
computations. In order to apply these rules properly, program terms
are brought into a canonical form after each reduction step, using the
canonicalization rules shown in \fig{canon}. Canonicalization rules
include block flattening, identifier and constant substitution,
elimination of redundant bindings, and propagation of $\top$. Nested
blocks are flattened by merging their sets of bindings.  This cannot
cause any name clashes since we always rename all bound identifiers of
a $\lambda$-expression on application.  Bindings of the form $x=y$ or
$x=c$ cause substitution of $[y/x]$ or $[c/x]$ respectively within
their entire lexical scope.\footnote{Blocks (delimited by $\{\;\}$)
determine the lexical scope of a binding. Lexical scope defines the
{\em visibility\/} of a binding and is unrelated to its control region
which defines the {\em control\/} of its initiation and termination.}
Only identifiers or constants are allowed to be substituted, in order
to preserve precise sharing of sub-expressions among terms.  After
substitution, all such simple bindings are eliminated from the program
term, leaving it in a unique canonical form.

It is also possible to encounter degenerate bindings of the form $x=x$
during reduction and substitution, because of circular dependencies present
within the program.  In this case, the semantic meaning of $x$ is
bottom ($\bot$), because such bindings represent deadlocked
computation.  Such bindings are canonicalized by
substituting a special constant $\odot$ for $x$ ($\whnf{\odot}=\bot$),
while retaining the binding $x=x$ as $x=\odot$. Finally, the blowup
rule shows that once an inconsistent state ($\top$) is created, the
whole program becomes inconsistent.
