% File:    sect5.tex
% Author:  Florian Matthes
% Date:    22-FEB-1994 
% Purpose: Paper on Persistent Threads

\section{On thread implementation and formalization}
\label{Sec:Semantics}

\input{declarations.sty}

Several important requirements on persistent thread implementations
differ substantially from volatile thread implementations, for example:

\begin{enumerate}

\item Thread state representations have to be made relocatable and
portable in the sense that states need to be abstractly interpretable
without reference to a specific machine architecture (e.g., SPARC
register files).

\item It is desirable to have automatic garbage collection that reclaims the 
storage of terminated or orphaned threads.

\item It is necessary to formalize in sufficient detail the effects of thread
execution on shared entities in the persistent store, in particular, if
these entities have a complex structure. Only then reliable support can
be provided for concurrency, recovery, or garbage collection.

\item Store access in distributed persistent memory has different 
performance figures than store access in centralized shared-memory 
architectures.
 
\item In data-intensive applications, the thread state can vary 
dramatically in size, for example, to accommodate the numerous temporary 
bindings that arise during query evaluation.  Clearly, simple thread 
implementations based on fixed-sized stacks are not acceptable.

\item Built-in schedulers have to be able to work with a number of 
persistent threads that may exceed the number of volatile threads by two to 
three numbers of magnitude.

\end{enumerate}

In this section, we first report on our implementation of persistent
threads focussing on the issues (1) through (4) since the remaining
investigations are beyond the scope of this paper.  We then sketch
thread formalization with a clear emphasis on abstract representations
of machine code (Tycoon Machine Language, TML), machine states and on
explicit modeling of machine-store interactions (Tycoon Store Protocol,
TSP).

In our experience, a formalization on an appropriate level of
abstraction and with an intensive flavor of ``constructivity'' is
absolutely essential for any good implementation of a conceptually rich
system abstraction, such as persistent threads.

\subsection{The Tycoon thread implementation}

The Tycoon thread implementation is divided into subtasks solved by
three distinct layers of the Tycoon system architecture:

\begin{enumerate}

\item The Tycoon compiler front end performs the type checking and code
generation of application programs. Due to the polymorphic nature of
Tycoon's type system, no extensions of the Tycoon compiler front end are
required to support user-defined type constructors like \p{thread.T(R)}
described in section~\ref{Sec:FC-Bindings}.

Tycoon uses a uniform (tagged) polymorphic data representation.
Therefore, no modifications to the Tycoon code generator are required to
support operations on first-class persistent threads. The binding of the
operations \p{thread.new}, \p{thread.run}, etc.\ to processor-specific
compiled C code implementing thread creation, thread execution etc.\ is
accomplished by standard Tycoon language mechanisms.

\item The Tycoon compiler generates abstract machine code
(TML). For every hardware architecture there is a separate Tycoon
evaluator, implemented as an interpreter or a pair of a target object
code generator and a runtime library that dynamically loads the target
code into the process address space. The execution of Tycoon threads is
performed by TML evaluators that read code held in the Tycoon object
store and that are able to store their evaluation state in a portable
format in the object store. Thereby, it is possible to exchange
suspended evaluator states between different hardware architectures and
to represent bindings to threads by standard object store identifiers
with the usual sharing semantics.

\item The Tycoon object store allows evaluators to abstract from
the lifetime and storage details of all computational entities (data,
code, threads). The store encapsulates buffer management, garbage
collection, cache coherence management and recovery management. Tycoon
evaluators access the Tycoon store via an abstract store protocol (TSP)
implemented as a collection of standardized C functions.

\end{enumerate}

\begin{figure}
\begin{center}\leavevmode
\epsfxsize=\textwidth
\epsfbox{Object-Store.ps}
\end{center}
\caption{Interaction between TML evaluators}
\label{Fig:Object-Store}
\end{figure}

Figure~\ref{Fig:Object-Store} shows the interaction between multiple
Tycoon threads accessing a shared persistent object store (possibly
partitioned into disjoint repositories). It shows two operating-system
processes, each executing a TML evaluator that manages a set of Tycoon
threads. Thread states consist of a machine state (a register set) and a
dynamic context of variable size. Active threads are cached in local
process memory. Furthermore, the object store permits TML evaluators to
fix (pin) persistent objects in local process memory.  It is the object
store's responsibility to ensure the coherence between thread states and
other persistent objects cached in multiple process address spaces.

\subsection{On thread formalization}

\begin{figure}\small
\begin{tabular}{rll}
$c ::=$ 
   & $\tmlnop                            $ & no operation \\
$|$& $\tmlimmediate{b}                   $ & base value access \\
$|$& $\tmlliteral{i}                     $ & literal value access \\
$|$& $\tmlgetlocal{i}                    $ & local variable access \\
$|$& $\tmlgetparam{i}                    $ & parameter value access \\
$|$& $\tmlgetglobal{i}                   $ & function closure value access \\
$|$& $\tmlgetindexed{c_1}{c_2}           $ & object store variable acess \\
$|$& $\tmlsetlocal{i}{c_1}               $ & local variable assignment \\
$|$& $\tmlsetglobal{c_1}{i}{c_2}         $ & function closure initialization \\
$|$& $\tmlsetindexed{c_1}{c_2}{c_3}      $ & object store assignment \\
$|$& $\tmlabstract{n}{c_1}{c_2}{c_3}     $ & function closure allocation \\
$|$& $\tmllambda{c_1}{n}                 $ & local variable allocation \\
$|$& $\tmlapply{c_0}{c_1 \ldots c_n}     $ & function application \\
$|$& $\tmlseq{c_1}{c_2}                  $ & sequential evaluation \\
$|$& $\tmlloop{c_1}                      $ & repeated evaluation \\
$|$& $\tmlexit{c_1}                      $ & loop termination \\
$|$& $\tmltrap{c_1}{i}{c_2}              $ & exception handling \\
$|$& $\tmlraise{c_1}                     $ & exception generation \\
$|$& $\tmlapplybuiltin{op}{c_1 \ldots c_n} $ & builtin function application \\
$|$& $\k{alt}\,c_0\,\k{of}\,tags\,\k{do}\,c_1 \ldots, c_n\,\k{else}\,c_{n+1}$
                                           & multi-way case analysis \\
$tags ::=$ & $\tmltags{n}                $ & case labels \\
\end{tabular}
\caption{Abstract TML syntax}
\label{Fig:TML-Syntax}
\end{figure}

A thread formalization has to define invariants maintained by the
scheduling operations exported by the interface \p{Thread} (see
section~\ref{Sec:Programming}) and it has to specify the semantics of
individual threads by an inductive definition of the bindings and store
side-effects performed for each instruction executed by a thread. The
first issue has been treated already in the literature, for example,
chapter~5 of \cite{Nels91} gives a complete Larch specification of the
Modula-3 thread package that is very similar to Tycoon's \p{Thread}
interface.  Here, we concentrate on the second issue. The TML/TSP
specification sketched in the remainder of this section not only affects
the granularity level on which thread operations (e.g. \p{run, join})
are performed, but also the degree to which further requirements on
threads as enumerated at the beginning of section~\ref{Sec:Semantics}
can be supported.

Tycoon's RISC-style TML code representation is shown in
figure~\ref{Fig:TML-Syntax}. This instruction set suffices to implement
the full Tycoon language as defined in \cite{MaSc92a} (and similar
higher-order programming languages like Fibonacci or Napier88).  We are
currently moving to an even more reduced, continuation-passing style
(CPS) \cite{App92} code representation that simplifies the static and
dynamic program analysis and optimization tasks that are performed by
the compiler, run-time query optimizer and thread scheduler (side-effect
analysis, sharing analysis, inlining, dead code elimination, etc.)
\cite{GMM94}. However, CPS code needs to be normalized (closure
converted, exception converted) prior to execution to achieve good
executions on standard hardware architectures.

The semantics of TML programs involves syntactic entities that are
denoted by indexed ($i, j, k, n, m$) variable names as follows:

\begin{center}
\begin{tabular}{ll}
$c \in Code$                             & TML instructions
					(see Fig.~\ref{Fig:TML-Syntax}) \\
$b,lit,g,p,l \in BVal = \NAT \cup \{\tmlnil\}$     & base values \\
$\tmlenv = \tmlframe{n}{m} \in Env$      & dynamic environments \\
$\tmllocals = [l_0 \ldots l_k] \in Loc$  & local environments \\
$v \in Val = SVal \cup \{\tmlok, 
\tmlexceptionpack{p}, \tmlexitpack{p}\}$ & evaluation results \\
\end{tabular}
\end{center}

The semantics of a Tycoon object store is defined as a partial mapping
from a domain of (tagged) object identifiers $\Ref$ (disjoint from the set of
base values $BVal$) to fixed-sized arrays of state values. A state value
is either an object identifier or a base value.
\begin{center}
\begin{tabular}{rll}
$r, lit \in\Ref$       &                                       & object identifiers \\
$sv, l, p, g \in SVal$ & =$BVal \cup \Ref $                    & state values \\
$S \in Store$        & $=(\finitemap{\Ref \times \NAT}{SVal})$ & object store \\
                        & $\times (\finitemap{\Ref}{Code})$      &  \\
                        & $\times (\finitemap{\Ref}{\NAT})$      &  \\
\end{tabular}
\end{center}

For example, the operation \p{init} returns the store value
$\makestore{\makemap{}}{\makemap{}}{\makemap{}}$ while the store
operation \p{new} is defined by
\[ \storenew{\makestore{StV}{StC}{StS}}{n} = \makestore{StV'}{StC}{StS'}
\]
where
\begin{eqnarray*}
r    & \not\in & \mapdomain{StV} \\
StV' & =       & StV + \makemap{\mapelement{(r,0)}{\tmlnil}}
                     + \makemap{\mapelement{(r,1)}{\tmlnil}} + \ldots
                     + \makemap{\mapelement{(r,n-1)}{\tmlnil}} \\
StS' & =       & \mapupdate{StS}{\makemap{\mapelement{r}{n}}} 
\end{eqnarray*}
It takes a store $(StV,StC,StS)$ and a size $n$ and returns a new store
that contains a new, \p{nil}-initialized store vector of size $n$ that can be
identified by its unique OID $r$. The remaining store operations
\p{get, set, newclosure, fixexecute} are defined analogously.

\begin{figure}
\begin{center}\leavevmode
\def\epsfsize#1#2{0.6#1}
\epsfbox{TML-State.ps}
\end{center}
\caption{The TML machine model}
\label{Fig:TML-State}
\end{figure}

The state of a TML thread executing a Tycoon function \p{f} consists of
a quadruple $E,S,L,c$ where $E$ aggregates a reference to an immutable
vector $lit$ (that holds the string, longreal, \ldots\ literals of
\p{f}), the immutable global bindings $g_0, \ldots, g_n$ of \p{f}, and
the immutable actual parameter $p_0, \ldots, p_m$ of \p{f}. $S$
describes the current state of the object store. $L$ describes those
bindings in \p{f} that are inaccessible to other threads, and $c$
describes the instruction of \p{f} that is currently being
executed. Figure~\ref{Fig:TML-State} depicts the relationship between
these thread components.

The precise semantics of each TML instruction can now be described by
its impact on TML thread states and by the operations executed on the
persistent object store \cite{Matt93} (structured operational semantics
\cite{Plot81}).  This semantic definition is ``constructive'' in the
sense that it provides a precise starting point for the implementation
of TML interpreters.

The evaluation of a TML instruction is described using the following
notation:
\[\tmleval{\tmlenv}{\tmlstore_1}{\tmllocals_1}{c}{\tmlstore_2}{\tmllocals_2}{v}
\] 
The execution of the (composite) instruction $c$ in a dynamic context
$\tmlenv$, an object store state $\tmlstore_1$ with local state
variables $\tmllocals_1$ leads to an object store state $\tmlstore_2$,
local state variables $\tmllocals_2$ and an evaluation result $v$. This
definition implies that an instruction cannot modify its dynamic context
$E$.

For example, the deduction rule \p{[Eval seq]} defines that the
execution of the sequential composition $\tmlseq{c_1}{c_2}$ in an
environment $E$, against a store $S_1$, with local state variables $L_1$
is equivalent to the evaluation of $c_1$ in this thread state returning
a (possibly modified) object store $S_2$, a (possibly modified) set of
local state variables $L_2$, and a value $v$, followed by the execution
of $c_2$ in this modified environment, again returning a (modified) object
store $S_3$, (modified) state variables $L_3$, and a value $v'$.

\begin{center}
\define{Eval seq}{\dedtwo
{\tmleval
  {\tmlenv}
  {\tmlstore_{1}}
  {\tmllocals_{1}}
  {c_1}
  {\tmlstore_{2}}
  {\tmllocals_{2}}
  {v}
}
{\tmleval
  {\tmlenv}
  {\tmlstore_{2}}
  {\tmllocals_{2}}
  {c_2}
  {\tmlstore_{3}}
  {\tmllocals_{3}}
  {v'}
}
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmlseq{c_1}{c_2}}
  {\tmlstore_3}
  {\tmllocals_3}
  {v'}
}}
\end{center}

Note that the evaluation result $v$ of the first instruction is
discarded and that the evaluation result of the instruction sequence is
the result $v'$ of the second instruction. This is typical for an
imperative programming style, where statements do not compute a result
but simply perform side-effects on the store.

The semantics of TML function applications is defined as follows: In a
first step, an object store reference $r$ is computed which identifies a
function closure in the object store $S_2$ with code $c'$, literals
$lit$ and global variable bindings $g_0 \ldots g_n$. In a next step, the
actual parameters $p_0 \ldots p_m$ are evaluated (strict left-to-right
evaluation order).  The code $c'$ is executed in a newly-allocated
dynamic context consisting of $lit, g_0 \ldots g_n$ and $p_0 \ldots
p_m$.  After $c'$ has been evaluated, the dynamic context of the calling
function is restored as it has been left behind by the evaluation of the
last argument.

\begin{center}
\define{Eval apply}{\dedfour
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {c}
  {\tmlstore_2}
  {\tmllocals_2}
  {r}
}
{\storefixexecute{\tmlstore_2}{r} = (c', lit, g_0, \ldots, g_n)
}
{{\tmleval
  {\tmlenv}
  {\tmlstore_{i+2}}
  {\tmllocals_{i+2}}
  {c_i}
  {\tmlstore_{i+3}}
  {\tmllocals_{i+3}}
  {p_i}
} \bigspc i = 0 \ldots m}
{\tmleval
  {\tmlframe{n}{m}}
  {\tmlstore_{m+3}}
  {\tmllocals_{m+3}}
  {c'}
  {\tmlstore}
  {\tmllocals_{m+4}}
  {v}
}
{\tmleval
  {\tmlenv}
  {\tmlstore_1}
  {\tmllocals_1}
  {\tmlapply{c}{c_0 \ldots c_m}}
  {\tmlstore}
  {\tmllocals_{m+3}}
  {v}
}}
\end{center}