% -*- Mode: LaTeX -*-

\section{Parallel Evaluation Order}
\label{sec:eager}

pH follows an \ibx{eager} evaluation strategy: all tasks execute in
parallel, restricted only by the data dependencies among them. This
strategy automatically exposes large amounts of parallelism both
within and across procedures. This is in contrast with a \ibx{lazy}
evaluation strategy followed by Haskell: only those tasks are
evaluated which are required to produce the result. This strategy
imposes a sequential constraint on the overall computation,
although the exact ordering of tasks is decided dynamically.

In this section we describe the eager evaluation model of pH by giving
a parallel interpreter for the kernel language of pH. Our interpreter
is based on a parallel abstract machine, which is in the spirit of
the G-machine and its later variants
\cite{Johnsson84,Augustsson89,PeyJones92}. We first describe the kernel
language (\sec{lang}) and then our parallel abstract machine
(\sec{machine}) and its instruction set (\sec{inst}). It is followed
by a description of the interpreter (\sec{eval}).

\subsection{The Kernel pH Language}
\label{sec:lang}

\begin{myfig}{fig:lang}{The kernel pH 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} \\
\ibx{PF}^{n}      & \in & \bx{Primitive Fn. with $n$ arguments}\\
\ibx{CF}^{n}      & \in & \bx{Data Constructor with $n$ arguments}\\
S                 & \in & \bx{Statement} \\[.1in]

\bx{Constant} & ::= & \ibx{Integer} \mid \ibx{Float} \mid \ibx{Boolean} \mid \tbx{Nil} \\
\ibx{SE}      & ::= & \bx{Identifier} \mid \bx{Constant} \\
\ibx{PF}^{1}  & ::= & \tbx{hd} \mid \tbx{tl} \mid \tbx{select\_}k \\
\ibx{PF}^{2}  & ::= & + \mid - \mid \cdots \mid < \mid > \mid \cdots \\
\ibx{CF}^{2}  & ::= & \tbx{Cons} \\
\ibx{CF}^{n}  & ::= & \tbx{make\_$n$\_tuple} \\
E             & ::= & \ibx{SE} \mid \ibx{PF}^{n}(x_{1},\ldots,x_{n})
                      \mid \ibx{CF}^{n}(x_{1},\ldots,x_{n}) \\
              &     & \mid \lambda x.\; E \mid \tbx{case}(x,E_{1},\ldots,E_{n}) \\
              &     & \mid \tbx{ap}(f,z) \mid \tbx{sap}(f,z) \mid \bx{Block} \\
\bx{Block}    & ::= & \{\;S\;\tbx{in}\;x\;\} \\
S             & ::= & \epsilon \mid x = E \mid S_{1};\ldots;S_{n} \\
\bx{Program}  & ::= & \bx{Block}
\end{array}$
\end{myfig}

The abstract syntax of the kernel pH language is shown in \fig{lang}.
The kernel language ensures that every intermediate result of a
complex expression is explicitly named using an identifier. This is
convenient for expressing and preserving the sharing of subexpressions
within a computation \cite{Ariola94}.  In order to simplify the
description of the evaluation rules in this paper, we do not
allow constants to appear as arguments to primitive functions.

Aside from the usual arithmetic primitives, the kernel language
provides functions for constructing and selecting elements of lists
and $n$-ary tuples. The language also provides $n$-ary \tbx{case}
expressions which select one of the branches based on the value of the
dispatch identifier, nested $\lambda$-expressions which may contain
free identifiers, a general function application operator \tbx{ap},
and a parallel block construct that controls lexical scoping and
enables precise sharing of subexpression values.  The order of
bindings in a block is not significant. The identifier following the
\tbx{in} keyword in a block expression denotes the result of the
block.

\subsection{A Parallel Abstract Machine}
\label{sec:machine}

\begin{myfig}{fig:dynamic}{Dynamic entities used by the abstract machine.}
\centering
$\begin{array}{lclcl}
\inst       & \in & \bx{Instruction} \\
\loc        & \in & \bx{Location} & & \\
\val        & \in & \bx{Value} & ::= & \bx{Constant} \mid \bx{Location}
\mid \gval{\lambda x.\;E, \env} \\
\env        & \in & \bx{Environment Frame} & = & \bx{Identifier} \rightarrow \bx{Location}\\
\store      & \in & \bx{Store} & = & \bx{Location} \rightarrow \{\ftag{\val}\mid\dtag{\susps}\} \\
\work       & \in & \bx{Thread} & = & \bx{Code} \times \bx{Environments}\\ 
\susp       & \in & \bx{Suspension} & = & \bx{Thread} \\
\susps      & \in & \bx{Suspensions} & = & \fn{List}{\bx{Thread}} \\
\works      & \in & \bx{Work Queue} & = & \fn{List}{\bx{Thread}} \\[.1in]
            &     & \bx{Accumulator} & = & \bx{Value} \\
\insts      & \in & \bx{Code} & = & \fn{List}{\bx{Instruction}} \\
\envs       & \in & \bx{Environment} & = & \fn{List}{\bx{Environment Frame}} \\
            &     & \bx{Processor} & = & \bx{Accumulator} \times
\bx{Code} \times \bx{Environment} \\
            &     & \bx{Machine} & = & \fn{List}{\bx{Processor}}
\times \bx{Work Queue} \times \bx{Store}
\end{array}$ \\[.1in]
\centering
$\begin{array}{l|ccc|cc}
 & \multicolumn{3}{c|}{\bx{Processor}} & \multicolumn{2}{c}{\bx{Global Memory}}\\
\bx{State} & \bx{Accumulator} & \bx{Code} & \bx{Environment} &
\bx{Work Queue} & \bx{Store} \\ \hline
\bx{Initial (starting proc.)} & \_ & \insts_{0} & [\;] & [\;] & \{\} \\
\bx{Initial (other proc.)} & \_ & [\;] & [\;] & [\;] & \{\} \\
\bx{Final (all proc.)} & \_ & [\;] & [\;] & [\;] & \store \\
\bx{Error (any proc.)} & \tbx{storerr} & \insts & \envs & \works & \store
\end{array}$ \\[.1in] 
\raggedright
Where $\insts_{0} = [\eval{\bx{Program}},\print,\sched]$ \\
\end{myfig}

Our parallel abstract machine consists of a number of sequential
processors connected to a global shared memory. The important features
of our machine are described in \fig{dynamic}.  Each memory location
can hold a value or a list of suspended threads, and is tagged with
its status. A \fbx{full} location contains a value.  A newly allocated
location is tagged with \fbx{defer} and it is initialized to be empty.
A \ibx{value} is either a constant, an allocated store location, or a
function closure. The global memory holds three types of entities:
heap storage, activation frames and a \ibx{work queue} which is a
list of \ibx{threads}, that is, (\ibx{code}, \ibx{environment}) pairs.

The processor state consists of code, environment, and an
\ibx{accumulator} which can hold a value.  Any idle processor can get
work by dequeuing a thread from the work queue and loading its code
and environment space from the thread.  Initially, it is assumed that
the whole machine is empty.  A program $E$ is started by executing the
following code on some processor in the empty environment.

\[[\eval{E}, \print, \sched]\]

The \fbx{eval} instruction interprets an expression by structural
decomposition in a given environment.  Environments map program
identifiers to frame locations, and are structured in a stack like
manner. \fbx{eval} of a block allocates a new \ibx{activation frame}
in the global memory to store the values of the bound identifiers of
the block. It also creates a new \ibx{environment frame} for these
identifiers and pushes it on the processor environment. The bound
identifiers of the block point to locations in the newly allocated
activation frame.  New environment frames (but not activation frames)
are also created in case of $\lambda$-expressions and function
applications.  The sharing of computations is achieved entirely
through the activation frame locations: all references to an
identifier within the scope of its definition lead to the same frame
location.  The separation of environment frames and activation frames
permits environments to be copied freely and therefore allows us to
treat function closures in the same way as simple values.

At each step, the processor executes the instruction at the head of
the current code sequence, modifying the processor state in the
process.  The instruction set of the processor has instructions to
load and store the accumulator, perform arithmetic and logic
operations on store locations, and suspend the current thread in case
of missing values. This is in contrast with lazy functional languages
where unevaluated locations contain \ibx{thunks} that compute its
value on-demand.  Typically an instruction is popped from the code
sequence after execution, but some instructions may also add new
instructions to the code sequence. This is the primary way to alter
the control flow. There are also instructions to push and pop
environment frames, and enqueue and dequeue threads from the work
queue. 

The work queue is maintained as a FIFO queue in order to guarantee
fair scheduling. This queue must be manipulated atomically. It is easy
to modify the machine so that each processor has its own work queue
which is maintained in a FIFO manner. In case a processor goes idle,
it can pick up a thread from the back of the work queue of any
other processor. As long as we do not arbitrarily suspend the currently
running thread on any processor, this strategy still implements a fair
schedule while considerably reducing the contention due to the atomic
manipulation of the work queue. 

The overall state of our parallel machine is described by the state of
all the processors and the global memory and the work queue. 
\fig{dynamic} also shows the initial, the final and the error states
of the processors of our machine. The machine starts by scheduling an
initial sequence of instructions on some processor that evaluates the
program, prints the result present in the accumulator\footnote{The
main thread is the only place where a \print instruction may appear.},
and then continues to schedule the remaining work present in the work
queue. This emphasizes the non-strict nature of this evaluation model:
the program may print a result before final termination. The machine
halts when both the code sequence and the work queue are empty. The
machine is said to be \ibx{deadlocked} when there are suspended
computations in the store but there is no work to be done. If there
are no suspended computations, then the machine is said to have {\em
terminated normally}. An error may be generated during execution due
to exceptional conditions such as a type mismatch, an arithmetic
overflow, or out of bounds access to data structures. However, if an
attempt is made to write into a memory location that is already
\fbx{full} then the whole machine is said to have reached an error
state as shown in \fig{dynamic}. 

\subsection{Instruction Set}
\label{sec:inst}

\begin{myfig}{fig:insts}{The instruction set of the parallel abstract machine.}
\centering
\begin{tabular}{@{}l@{\hm::\hm}p{4.5in}}
\eval{E} & Evaluate $E$ in the current environment and leave
the result in the accumulator \\
\multicolumn{2}{@{}l}{\rule[.05in]{\hsize}{.01in}} \\
\touch{\loc} & Check if the location $\loc$ is \fbx{full}, if not
suspend the current thread \\
\rtouch{\loc} & Check if the location $\loc$ is \fbx{full}, if not
suspend the current thread including the \fbx{rtouch}
instruction. (Thus, \fbx{rtouch} can be retried when the thread
is activated again). \\
\lda{\loc} & Load the accumulator with the value present in the
location $\loc$ (the location must be \fbx{full}) \\
\tka{\loc} & Load the accumulator with the value present in the
location $\loc$ and mark the location empty (the location must be
\fbx{full}) \\
\ldi{k}{\loc} & Load the accumulator with the value in the location
at an offset $k$ from the location pointed to by $\loc$, or suspend
the thread if the location is empty  \\
\sta{\loc} & Store the value in the accumulator in the location $\loc$
and reactivate any suspensions \\
\fullerr{\loc} & Generate an error if the location $\loc$ is \fbx{full} \\
\primapp{\fbx{PF}^{n}}{\loc_{1},\ldots,\loc_{n}} & Apply strict
primitive operator $\fbx{PF}^{n}$ (such as \fbx{+}) to
the values at locations $\loc_{1},\ldots,\loc_{n}$ (the locations must
be \fbx{full}) \\ 
\switch{\loc_{x}}{\insts_{1},\ldots{},\insts_{n}} & Switch to the
branch indexed by the value at location $\loc_{x}$ \\
\pushenv{\env} & Push the environment frame $\env$ onto the
environment stack \\
\popenv & Pop the top-level environment frame from the environment
stack \\ 
\sched & Schedule the next thread from the work queue \\
\print & Print the accumulator contents
\end{tabular}
\end{myfig}

\fig{insts} shows the instructions used by our interpreter. We will
describe the semantics of these instructions in terms of a state
transition involving a 5-tuple ($\val,\insts,\envs,\works,\store$).
The first three elements of the tuple refer to the accumulator
carrying a value \val, the code sequence \insts, and the environment
\envs on the processor where the instruction is executed.  The last
two elements of the tuple are the work queue \works, and the dynamic
store \store which are shared amongst all processors.

All the instructions that modify the global store must be executed
atomically. That is, while a processor reads and modifies a given
location within the store, no other processor should be allowed to
read or write that location. Transactions on different locations may
proceed in parallel. In case where an instruction sequence $\insts$
has to be executed atomically, we will indicate that by writing
$\fn{atomic}{\insts}$.

\subsubsection*{Touch Instructions}

%% \ibx{Discuss Atomicity !!}

The \fbx{touch} instruction tests the status of a location. If the status
is \fbx{full}, it does nothing.  Otherwise, (status is \fbx{defer})
the code sequence following the current instruction is suspended at
that location along with the current environment. The \fbx{rtouch}
instruction is similar except that the touch operation is retried.

\begin{evalrule}{\fbx{touch}:}
\inference{\state{\_}{\touch{\loc}:\insts}{\envs}{\works}{\store[\loc\mapsto\ftag{\val}]}{}}%
          {\state{\_}{\insts}{\envs}{\works}{\store}{}} \\ \\

\inference{\state{\_}{\touch{\loc}:\insts}{\envs}{\works}{\store[\loc\mapsto\dtag{\susps}]}{}}%
          {\state{\_}{[\sched]}{\envs}{\works}{\store[\loc\mapsto\dtag{(\insts,\envs):\susps}]}{}}
\end{evalrule}

\begin{evalrule}{\fbx{rtouch}:}
\inference{\state{\_}{\rtouch{\loc}:\insts}{\envs}{\works}{\store[\loc\mapsto\ftag{\val}]}{}}%
          {\state{\_}{\insts}{\envs}{\works}{\store}{}} \\ \\

\inference{\state{\_}{\rtouch{\loc}:\insts}{\envs}{\works}{\store[\loc\mapsto\dtag{\susps}]}{}}%
          {\state{\_}{[\sched]}{\envs}{\works}%
                 {\store[\loc\mapsto\dtag{(\rtouch{\loc}:\insts,\envs):\susps}]}{}}
\end{evalrule}

Note that these instructions do not start the evaluation of the
expression that will fill the location being touched. In lazy
evaluation this expression is always known and a thunk for it can be
stored in this location. In that case, the above instructions can be
easily generalized to enqueue the thunk into the work queue.

\subsubsection*{Load and Store Instructions}

The \fbx{load} instruction loads the contents of a given location into
the accumulator. The location must already be \fbx{full}. The
\fbx{take} instruction is similar to \fbx{load} except that it leaves
the location empty.  

\begin{evalrule}{\fbx{load}:}
\inference{\state{\_}{\lda{\loc}:\insts}{\envs}{\works}{\store[\loc\mapsto\ftag{\val}]}{}}%
          {\state{\val}{\insts}{\envs}{\works}{\store}{}}
\end{evalrule}

\begin{evalrule}{\fbx{take}:}
\inference{\state{\_}{\tka{\loc}:\insts}{\envs}{\works}{\store[\loc\mapsto\ftag{\val}]}{}}%
          {\state{\val}{\insts}{\envs}{\works}{\store[\loc\mapsto\dtag{[\;]}]}{}}
\end{evalrule}

\fbx{loadi\_$k$} is an indexed, indirect load instruction. It desugars
into touching an indexed location and then loading its value into the
accumulator.

\begin{evalrule}{\fbx{loadi\_$k$}:}
\inference{\state{\_}{\ldi{k}{\loc_{x}}:\insts}{\envs}%
                 {\works}{\store[\loc_{x}\mapsto\ftag{\loc}]}{}}%
          {\state{\_}{\touch{\loc+k}:\lda{\loc+k}:\insts}{\envs}{\works}{\store}{}}
\end{evalrule}

The \fbx{store} instruction stores the contents of the accumulator
into the given location.  It also reactivates any suspensions waiting
in the location by enqueuing them in the work queue.

%% \ibx{Discuss Atomicity !!}

\begin{evalrule}{\fbx{store}:}
\inference{\state{\val}{\sta{\loc}:\insts}{\envs}{\works}{\store[\loc\mapsto\dtag{\susps}]}{}}%
          {\state{\val}{\insts}{\envs}{\works\append\susps}{\store[\loc\mapsto\ftag{\val}]}{}}
\end{evalrule}

Storing in a location that is already full is regarded as an error.
The \fbx{storerr} instruction tests the status of a location and
produces an error if it is already full. This instruction can precede
a \fbx{store} instruction to avoid multiple stores to the same
location. 

\begin{evalrule}{\fbx{storerr}:}
\inference{\state{\_}{\fullerr{\loc}:\insts}{\envs}{\works}{\store[\loc\mapsto\ftag{\val}]}{}}%
          {\state{\tbx{storerr}}{\insts}{\envs}{\works}{\store}{}} \\ \\

\inference{\state{\_}{\fullerr{\loc}:\insts}{\envs}{\works}{\store[\loc\mapsto\dtag{\susps}]}{}}%
          {\state{\_}{\insts}{\envs}{\works}{\store}{}}
\end{evalrule}

\subsubsection*{Arithmetic and Logic Instructions}

The standard arithmetic and logic primitives are straightforward.
All of them leave the result in the accumulator. 

\begin{evalrule}{\fbx{+}:}
\inference{\state{\_}{\primapp{\fbx{+}}{\loc_{1},\loc_{2}}:\insts}{\envs}{\works}%
                 {\store[\loc_{1}\mapsto\ftag{\ul{m}},\loc_{2}\mapsto\ftag{\ul{n}}]}{}}%
          {\state{\ul{m+n}}{\insts}{\envs}{\works}{\store}{}}
\end{evalrule}

\subsubsection*{Switch Instruction}

The \fbx{switch} instruction selects one of its branches based on
the value present in the location being dispatched upon. 

\begin{evalrule}{\fbx{switch} ($1\leq{}m\leq{}n$):}
\inference{\state{\_}{\switch{\loc_{x}}{\insts_{1},\ldots,\insts_{n}}:\insts}%
                 {\envs}{\works}{\store[\loc_{x}\mapsto\ftag{\ul{m}}]}{}}%
          {\state{\_}{\insts_{m}\append\insts}{\envs}{\works}{\store}{}}
\end{evalrule}

\subsubsection*{Environment Manipulation Instructions}

The \fbx{pushenv} instructions pushes the given environment frame onto
the local environment stack of a processor, while the \fbx{popenv}
instruction pops one frame from the top. The contents of the
accumulator are not disturbed while popping. 

\begin{evalrule}{\fbx{pushenv}:}
\inference{\state{\_}{\pushenv{\env}:\insts}{\envs}{\works}{\store}{}}%
          {\state{\_}{\insts}{\env:\envs}{\works}{\store}{}}
\end{evalrule}

\begin{evalrule}{\fbx{popenv}:}
\inference{\state{\val}{\popenv:\insts}{\env:\envs}{\works}{\store}{}}%
          {\state{\val}{\insts}{\envs}{\works}{\store}{}}
\end{evalrule}

\subsubsection*{Thread Scheduling Instruction}

%% \ibx{Discuss Atomicity !!}

The execution of a \sched instruction on a processor signifies either
the termination or the suspension of a thread. The processor schedules
a new thread from the head of the work queue or starts \ibx{idling} if
the work queue is empty.  The machine halts when all processors are
idling.

\begin{evalrule}{\sched:}
\inference{\state{\_}{[\sched]}{\envs}{(\insts',\envs'):\works}{\store}{}}%
          {\state{\_}{\insts'}{\envs'}{\works}{\store}{}} \\ \\

\inference{\state{\_}{[\sched]}{\envs}{[\;]}{\store}{}}%
          {\state{\_}{[\;]}{\envs}{[\;]}{\store}{}}
\end{evalrule}

\subsection{Expression Evaluation}
\label{sec:eval}

In this section we describe the \fbx{eval} instruction which is used
to destructure and evaluate expressions. It leaves the value of the
expression in the accumulator. 

Evaluation of a constant simply loads that constant into the
accumulator.

\begin{evalrule}{\fbx{eval} constant:}
\inference{\state{\_}{\eval{c}:\insts}{\envs}{\works}{\store}{}}%
          {\state{c}{\insts}{\envs}{\works}{\store}{}}
\end{evalrule}

Evaluation of an identifier first touches it and then loads its value
in the accumulator. 

\begin{evalrule}{\fbx{eval} identifier:}
\inference{\state{\_}{\eval{x}:\insts}{\envs}{\works}{\store}{}}%
          {\state{\_}{\touch{\envs(x)}:\lda{\envs(x)}:\insts}{\envs}{\works}{\store}{}}
\end{evalrule}

In case of a strict primitive function, we touch all its arguments
before executing the primitive application.  

\begin{evalrule}{\fbx{eval} strict PF:}
\inference{\state{\_}{\eval{\ibx{PF}^{n}(x_{1},\ldots,x_{n})}:\insts}%
                 {\envs}{\works}{\store}{}}%
          {\state{\_}{\touch{\envs(x_{1})}:\ldots:\touch{\envs(x_{n})}:
                        \primapp{\fbx{PF}^{n}}{\envs(x_{1}),\ldots,\envs(x_{n})}:\insts}%
                 {\envs}{\works}{\store}{}}
\end{evalrule}

All data selector functions such as \fbx{hd}, \fbx{tl}, and
\fbx{select\_$k$} are directly implemented using the indexed, indirect
load instruction \fbx{loadi\_$k$}.

The non-strict constructor \tbx{Cons} allocates a pair of empty
locations in the store and immediately returns the pointer to the
first location as its value. It also pushes work into the work queue
to evaluate the arguments of \tbx{Cons} and to fill these locations
eagerly. The $n$-ary tuple constructor \tbx{make\_$n$\_tuple} operates in
the same fashion.  Note that under lazy evaluation we would have
stored thunks into these locations which would be evaluated on demand.

\begin{evalrule}{\fbx{eval} \tbx{Cons}:}
\inference{\state{\_}{\eval{\tbx{Cons}(x_{1},x_{2})}:\insts}{\envs}{\works}{\store}{}}%
          {\state{\loc}{\insts}{\envs}{\works\append[\work_{1},\work_{2}]}{\store'}{}}\\ \\
\multicolumn{1}{l}{where $\begin{array}[t]{l}
\store'=\store+\{\;\loc\mapsto\dtag{[\;]},(\loc+1)\mapsto\dtag{[\;]}\;\} \\
\work_{1}=([\eval{x_{1}},\sta{\loc},\sched], \envs) \\
\work_{2}=([\eval{x_{2}},\sta{\loc+1},\sched], \envs)
\end{array}$}
\end{evalrule}

$\lambda$-expressions are evaluated to a closure value. The closure
records the locations for the free identifiers of the $\lambda$-body
in a new environment frame. 

\begin{evalrule}{\fbx{eval} $\lambda$-expression:}
\inference{\state{\_}{\eval{\lambda x.E}:\insts}{\envs}{\works}{\store}{}}%
          {\state{\gval{\lambda x.\;E, \env}}{\insts}{\envs}{\works}{\store}{}} \\ \\
\multicolumn{1}{l}{where $\begin{array}[t]{l}
y_{1},\ldots,y_{m} = \fn{FV}{\lambda x.E} \\
\env = \{\;y_{1}\mapsto\envs(y_{1}),\ldots,y_{m}\mapsto\envs(y_{m})\;\}
\end{array}$}
\end{evalrule}

Evaluation of a function application proceeds by first touching the
function and then applying the resulting closure to the argument. The
function argument is touched prior to application only if the function
application is strict (\tbx{sap}).

\begin{evalrule}{\fbx{eval} \tbx{ap}:}
\inference{\state{\_}{\eval{\tbx{ap}(f,z)}:\insts}{\envs}{\works}{\store}{}}%
          {\state{\_}{\touch{\envs(f)}:\intapp{\envs(f)}{\envs(z)}:\insts}%
                 {\envs}{\works}{\store}{}}
\end{evalrule}

\begin{evalrule}{\fbx{eval} \tbx{sap}:}
\inference{\state{\_}{\eval{\tbx{sap}(f,z)}:\insts}{\envs}{\works}{\store}{}}%
          {\state{\_}{\touch{\envs(f)}:\touch{\envs(z)}:\intapp{\envs(f)}{\envs(z)}:\insts}%
                 {\envs}{\works}{\store}{}}
\end{evalrule}

Given a closure, the \fbx{ap} instruction extends the closure
environment frame with the given argument location and starts the
evaluation of the function body after pushing the new environment
frame onto the current environment. The old environment is restored
after the evaluation of the body produces a result in the
accumulator\footnote{Note that restoring the environment does not
imply that the function environment can be deallocated because some
threads of the function body may not have terminated yet.}.

\begin{evalrule}{\fbx{ap}:}
\inference{\state{\_}{\intapp{\loc_{f}}{\loc_{z}}:\insts}{\envs}{\works}%
                 {\store[\loc_{f}\mapsto\ftag{\gval{\lambda x.\;E,\env}}]}{}}%
          {\state{\_}{\pushenv{\env'}:\eval{E}:\popenv:\insts}{\envs}{\works}{\store}{}}\\
\multicolumn{1}{l}{where $\env' = \env+\{\;x\mapsto\loc_{z}\;\}$}
\end{evalrule}

The evaluation of the \tbx{case} expression proceeds by first
touching the dispatch expression. This must yield an integer within
the range of the dispatch which is used to select the appropriate
branch. 

\begin{evalrule}{\fbx{eval} \tbx{case}:}
\inference{\state{\_}{\eval{\tbx{case}(x,E_{1},\ldots,E_{n})}:\insts}%
                 {\envs}{\works}{\store}{}}%
          {\state{\_}{\touch{\envs(x)}:\switch{\envs(x)}%
                      {[\eval{E_{1}}],\ldots,[\eval{E_{n}}]}:\insts}{\envs}{\works}{\store}{}}
\end{evalrule}

The evaluation of a block expression allocates a new activation frame
in the store with a fresh location for each bound identifier of the
block. It also allocates new environment frame which points to the
locations in the new activation frame. This environment frame is
pushed onto the current environment. Following eager evaluation,
auxiliary threads are added to the work queue to evaluate each of the
right-hand side expressions in the extended environment. The result
identifier is also evaluated under this extended environment.

\begin{evalrule}{\fbx{eval} block:}
\inference{\state{\_}{\eval{\{\;x_{1}=E_{1};\ldots;x_{n}=E_{n}\;\tbx{in}\;x\;\}}:\insts}%
                 {\envs}{\works}{\store}{}}%
          {\state{\_}{\pushenv{\env}:\eval{x}:\popenv:\insts}{\envs}%
                 {\works \append \works'}{\store'}{}}\\ \\
\multicolumn{1}{l}{where $\begin{array}[t]{l}
\env = \{\;x_{1}\mapsto\loc_{1},\ldots,x_{n}\mapsto\loc_{n}\;\}\\
\store' = \store+\{\;\loc_{1}\mapsto\dtag{[\;]},\ldots,\loc_{n}\mapsto\dtag{[\;]}\;\}\\
\works' = \begin{array}[t]{l}
          [([\eval{E_{1}},\sta{\loc_{1}},\sched], \env:\envs),\\
          \cdots \\
          ([\eval{E_{n}},\sta{\loc_{n}},\sched], \env:\envs)]
          \end{array}
\end{array}$}
\end{evalrule}

It is also possible to initialize the newly allocated block locations
with the thunks for their respective right-hand side expressions, and
not enqueue threads into the work queue. These thunks will be enqueued
when the locations are touched.
