From blieb Thu Dec 12 14:07:04 1996
Received: by ressel.auto.tuwien.ac.at id AA08266
  (5.65c/IDA-1.4.4 for rlieger); Thu, 12 Dec 1996 14:06:59 +0100
Date: Thu, 12 Dec 1996 14:06:59 +0100
From: Johann Blieberger <blieb@auto.tuwien.ac.at>
Message-Id: <199612121306.AA08266@ressel.auto.tuwien.ac.at>
To: rlieger@auto.tuwien.ac.at
Status: R

\documentstyle[%
  slidesonly,%  Try notes or notesonly instead.
  %notes,%      Use instead of slidesonly to typeset the notes.
  %notesonly,%  Use instead of slidesonly to typeset notes and slides.
  %semcolor,%   Try me if using PSTricks.
  %semrot,%     Try me if using Rokicki's dvips.
  %semhelv,%    Try me if using a PostScript printer.
  %article,%    Try me.
  %portrait,%   Try me.
  a4,%
  %sem-a4,%     Try me if using A4 paper.
  semlayer,%     This must be included, but you need the semcolor option to
  verbatimfiles%
  ]{seminar}                                  % actually see the overlays.

\slidesmag{5}
\articlemag{1}

%\twoup                     % Try me for twoup printing.

%\portraitonly              % To print only portrait slides
%\landscapeonly             % To print only landscape slides

%\notslides{\ref{questions}-7,1}   %Try me: The slides are omitted.
%\onlyslides{\ref{questions}-7,1}  %Try me: Only these slides are included.
%\onlynotestoo                     %Try me: For selecting notes as well.

\colorlayers{red,blue}      % Try deleting this if using the semcolor option,
                            % to get \blue and \red to use PostScript color.

%\overlaysfalse             % Suppress overlays with semcolor option.
%\layersfalse               % Suppress color layers with semcolor option.

\rotateheaderstrue          % Try this out if using rotation macros.


\title{Augmenting Ada95 with Additional Real-Time Features}
\author{J. Blieberger, R. Lieger, and B. Burgstaller}
\date{}

\def\qed{}
\def\Bbb#1{\bf #1}
\def\ld#1{\text{ld}\ #1}
\def\frak#1{\cal #1}

\def\subsubsection{\par}
\def\endsubsubsection{}
%\newtheorem{th}{Theorem}[section]
\def\th#1#2{\begin{subsubsection}{\bf Theorem~#1.#2.}\sl}
\def\endth{\end{subsubsection}}
%\newtheorem{lem}{Lemma}[section]
%\def\lem#1#2{\begin{subsubsection}{\bf Lemma~#1.#2.}\sl}
%\def\endlem{\end{subsubsection}}

%\theoremstyle{definition}
%\newtheorem{defn}{Definition}[section]
%\def\defn#1#2{\begin{subsubsection}{\bf Definition~#1.#2.}\rm}
%\def\enddefn{\end{subsubsection}}
\def\cor#1{\begin{subsubsection}{\em Corollary~#1.}\rm}
\def\endcor{\end{subsubsection}}
%\newtheorem{example}{Example}
\def\example#1{\begin{subsubsection}{\bf Example~#1.}\rm}
\def\endexample{\end{subsubsection}}

%\theoremstyle{remark}
%\newtheorem{rem}{Remark}[section]
\def\rem#1#2{\begin{subsubsection}{\em Remark~#1.#2.}\rm}
\def\endrem{\end{subsubsection}}
\def\pf{\begin{subsubsection}{\em Proof.}\rm}
\def\endpf{\end{subsubsection}}

% definitions for defining syntactic and semantic parts
\newcommand{\syn}[1]{{\family{cmr}\shape{sl}\series{m}\selectfont #1}}
%\newcommand{\syn}[1]{{\textsl\textmd #1}}
\newcommand{\kw}[1]{{\family{cmr}\shape{n}\series{bx}\selectfont\/ #1}}   % for keywords
%\newcommand{\kw}[1]{{\textbf\/ #1}}   % for keywords
\newcommand{\opt}[1]{$[$#1\/$]$}          % for optional parts                         
\newcommand{\zeromore}[1]{$\{$#1\/$\}$}   % for parts that occur zero times or more
\newcommand{\bnfor}{$\mid$}
\newcommand{\tab}{$\qquad$}
\newcommand{\user}[1]{$<${\family{cmr}\shape{it}\series{m}\selectfont #1\/}$>$} % for parts to be defined by the user
%\newcommand{\user}[1]{$<${\textit #1\/}$>$} % for parts to be defined by the user
%{\family{cmr}\shape{sl}\series{m}\selectfont
\def\syntax{\begin{flushleft}\begin{tabular}{rcl}\family{cmr}\shape{sl}\series{m}\selectfont}
%\newenvironment{syntax}{\begin{flushleft}\begin{tabular}{rcl}\textsl}{\end{tabular}\end{flushleft}}
\def\endsyntax{\end{tabular}\end{flushleft}}

%\hyphenation{re-cur-sive}

%\theoremstyle{remark}
%\newtheorem{sem}{Semantic}
%\renewcommand{\thesem}{}

%\newcommand{\newblock}{}

%\newcommand{\ld}{\operatorname{ld}}

\newcommand{\Tr}{\frak T}
\newcommand{\T}{\cal T}
\renewcommand{\t}{\tau}
\newcommand{\Sr}{\frak S}
\renewcommand{\S}{\cal S}
\newcommand{\s}{\sigma}

\newcommand{\F}{\cal F}
\newcommand{\R}{\cal R}
\newcommand{\N}{\cal N}
\newcommand{\D}{\cal D}
\newcommand{\recdep}{\text{recdep}}

\newcommand{\of}{\overline f}
\newcommand{\og}{\overline g}

\newcommand{\A}{\cal A}
\newcommand{\G}{\cal G}
\newcommand{\M}{\cal M}

\newcommand{\sm}{\sqsubseteq}
\newcommand{\gt}{\sqsupseteq}

\renewcommand{\printlandscape}{\special{landscape}}


\newcommand{\sref}[1]{SLIDE \ref{#1}}
\newcommand{\heading}[1]{\begin{center}\large\bf #1\end{center}}

\newpagestyle{MH}%
  {Technical University Vienna, Project {\sf WOOP}\hfil\thepage}{}
\pagestyle{MH}

\newcounter{definition}
\setcounter{definition}{1}
\def\definition{{\bf Definition \thedefinition.\addtocounter{definition}{1}\/}\ }
\def\enddefinition{}
\def\lemma{{\em Lemma \thedefinition.\addtocounter{definition}{1}\/}\ }
\def\endlemma{}

\begin{document}

\maketitle          % This won't show up when \onlynotestoo is in effect.

\begin{slide}
  \ifslidesonly              % Title slide only for slidesonly selection.
    \maketitle
    \addtocounter{slide}{-1}
    \slidepagestyle{empty}
  \fi
\end{slide}

\begin{slide}\label{rt}%
{\bf Real-Time Systems:}
\begin{itemize}
\item system behavior must be correct
\item the result of a computation must be available within a predefined deadline
\end{itemize}

Timeliness can be achieved if the {\em scheduling problem\/} is solved properly.

Most scheduling algorithms assume that the runtime of a task is known a priori
({\em worst-case performance\/} of a task).
\end{slide}

\begin{slide}\label{wcp}
\begin{center}
{\bf Determining the Worst-Case Performance}
\end{center}
\vspace{0.5cm}
The most difficult tasks:
\begin{itemize}
\item number of iterations of a certain loop
\item recursion
\end{itemize}

%A solution to the first problem has been given in~\cite{bli:discloop},
%the second one will be treated in this paper.

\end{slide}

\begin{slide}
\begin{center}
{\bf Loops}
\end{center}
\vspace{0.5cm}
Ordinary programming languages:
\begin{itemize}
\item for-loops
\item general loops
\end{itemize}
\end{slide}

\begin{slide}
\begin{center}
{\bf Determining the number of iterations}
\end{center}
\vspace{0.5cm}
\begin{itemize}
\item
for-loop $\to$ trivial
\item
General loops $\to$ very difficult task
\end{itemize}
\end{slide}

\begin{slide}
\begin{center}
{\bf Real-Time Languages}
\end{center}
\vspace{0.5cm}
\begin{itemize}
\item
{\em forbid\/} general loops
\item
the programmer specifies a time bound
\end{itemize}
\end{slide}

%Our approach is different in that we define a new kind of loops,
%so-called discrete loops, which are described in detail in~\cite{bli:discloop}.
%In contrast to for-loops, discrete loops allow for a more complex
%dependency between two successive values of the loop-variable.
%
%Like for-loops discrete loops have a loop-variable and an integer
%range associated with them.
%The major difference to for-loops is that
%the loop-variable need not be assigned each value of the range.
%Which values are assigned to the loop-variable,
%is completely governed by the loop-body.
%The loop-header, however, contains a list of all those values
%that can possibly be assigned to the loop-variable during the
%next iteration.
%In fact each item of this list of values is a function of the loop-variable.
%
%An example for a discrete loop is depicted in Figure~\ref{complex_example}.
\begin{slide}
\begin{center}
{\bf A Discrete Loop}
\end{center}
\vspace{0.5cm}
\begin{quote}
\begin{verbatim}
discrete k in 1..N new k := 2*k | 2*k+1 loop
  -- loop body
end loop;
\end{verbatim}
\end{quote}
\vspace{0.5cm}
{\tt k}: $1, 2, 4, 9, 18, 37, 75, \dots$ \quad or \\
{\tt k}: $1, 3, 6, 13, 26, 52, 105, \dots$\\
\\
$\Rightarrow$ ``indeterminism''
\end{slide}
%In this example the loop-variable {\tt k} can assume the values
%$1, 2, 4, 9, 18, 37, 75, \dots$ until finally a value greater than {\tt N}
%would be reached. 
%But it is also possible that {\tt k} follows the sequence
%$1, 3, 6, 13, 26, 52, 105, \dots$.
%
%Another form of discrete loops are {\em discrete loops with a remainder function}.
%These loops are especially well-suited for
%algorithms designed to traverse binary trees and for {\em divide \& conquer algorithms}.
%A template showing such applications is given in Figure~\ref{traverse}.
\begin{slide}
\begin{center}
{\bf A Discrete Loop with a Remainder Function}
\end{center}
\vspace{0.5cm}
\begin{verbatim}
discrete node_pointer := root
    new node_pointer :=
      node_pointer.left | node_pointer.right
  with h := height
    new h = h-1 loop
  -- loop body
end loop;
\end{verbatim}
\end{slide}
%
%In this figure {\tt root} denotes a pointer to the root of the tree,
%{\tt height} denotes the maximum height of the tree, and
%{\tt node\_pointer} is a pointer to a node of the tree.
%The actual value of {\tt  height} depends on which kind of tree is used,
%e.g.~standard binary trees or AVL-trees.
%
%In any case the number of iterations of discrete loops can be determined at
%compile time
%if the iteration functions are monotonic.

\begin{slide}
\begin{center}
{\bf Properties of Discrete Loops}
\end{center}
\vspace{0.5cm}
\begin{enumerate}
\item
Compiler or runtime system checks if loop-variable does obtain
one of the possible values stated in the loop-header\\
$\Rightarrow$ {\em Programming error}, not a {\em timing error}.
\item
Determine the number of loop iterations
\end{enumerate}
\end{slide}

\begin{slide}
Some applications:
\begin{itemize}
\item
Heapsort
\item
Bottom-up Mergesort
\item
Divide and Conquer Algorithms, such as
\begin{itemize}
\item
Binary Search
\item
Balanced Tree Structures
\end{itemize}
\item
Euclid's algorithm
\end{itemize}
\end{slide}

\begin{slide}
\begin{center}
{\bf Real-Time Recursions}
\end{center}
\vspace{0.5cm}
many problems $\Rightarrow$
\begin{itemize}
\item
forbid recursions (e.g.~RT-Euclid, PEARL, Real-Time Concurrent~C, and the MARS-approach)
\item
allow recursions, but do not provide any help (e.g.~Ada)
\item
Our Approach: {\em constrain\/} recursions
\end{itemize}
\end{slide}

%Our approach is different in that we do not forbid recursion,
%but instead constrain recursive procedures such that their
%space and time behavior either can be determined at compile time
%or can be checked at runtime.
%Thus timing errors can be found either at compile time or
%are shifted to logical errors detected at runtime.
%
%The constraints mentioned above are more or less simple conditions.
%If they can be proved to hold, the space and time behavior of
%the recursive procedure can be estimated easily.
%
\begin{slide}
\begin{definition}\label{rec}
Essential properties of a recursive procedure:
\begin{itemize}
\item
the {\em parameter space\/} $\F$
\item
a set $\F_0\subseteq\F$, the {\em terminating values\/} of $\F$
\item 
its code
\end{itemize}
%If $p$ is called with actual parameters $f_0\in\F_0$,
%the code being executed must not contain a recursive call of $p$ to itself.
%If $p$ is called with actual parameters $f\in\F\setminus\F_0$,
%the code being executed must contain at least one recursive call of $p$ to itself.
\end{definition}
\end{slide}

\begin{slide}
\begin{definition}\label{R}
We define a set $\R(f)\subseteq\F$, ($f\in\F\setminus\F_0$) by $\of\in\R(f)$
iff $p(\of)$ is directly called in order to compute $p(f)$.
$\R(f)$ is called the set of {\em direct successors\/} of $f$.
%If $f\in\F_0$, the set $\R(f)=\emptyset$, i.e., it is empty.
\end{definition}
\end{slide}

\begin{slide}
\begin{definition}\\
%We denote by $f_1\prec f_2$ a binary relation,
%which implies that the recursion depth of the underlying
%recursive procedure applied to $f_1$ is smaller than if applied to $f_2$.
%If the recursion depth of $f_1$ is smaller than or equal to that of $f_2$,
%we write $f_1\preceq f_2$.
%
%The set $\F_i$ contains all $f\in\F$ with recursion depth $i$.
$f_1\prec f_2$ $\Leftrightarrow$ $\recdep(f_1) < \recdep(f_2)$\\
$f_1\preceq f_2$ $\Leftrightarrow$ $\recdep(f_1) \le \recdep(f_2)$
\end{definition}
\end{slide}

\begin{slide}
Denoting by $\t(f)$, $f\in\F$ the time used to perform $p(f)$ without
taking into account the recursive calls, we have for the overall
timing behavior of $p(f)$
$$
\T(f) = \t(f) + \sum_{\of\in\R(f)} \T(\of).
$$
\end{slide}

\begin{slide}
\begin{definition}
For all $f_1,f_2\in\F$ we write
$f_1 \sm f_2$ (or equivalently $f_2 \gt f_1$)
if $f_1 \preceq f_2$ and $\t(f_1) \leq \t(f_2)$.
\end{definition}
\begin{definition}
Let $f_1, f_2 \in \F$, $\R(f_i) = \{f_{i,1},\dots,f_{i,m_i}\}$, $i=1,2$,
such that $f_{i,1} \gt f_{i,2} \gt \dots \gt f_{i,m_i-1} \gt f_{i,m_i}$, $i=1,2$.

If for all $f_1 \sm f_2$,
we have $m_1 \leq m_2$ and $f_{1,r} \sm f_{2,r}$, $r=1,\dots,m_1$,
then the underlying recursive procedure is called {\em locally time-monotonical}.
\end{definition}
\end{slide}

\begin{slide}
\begin{lemma}\label{time_mono}
If a recursive procedure $p$ is locally time-monotonical,
then $f_1 \sm f_2$ implies $\T(f_1) \leq \T(f_2)$.\qed
\end{lemma}
\vspace{0.5cm}
$\Rightarrow$ upper bound $\approx$ largest value $(\sm)$
\end{slide}
%Thus if we can prove that a certain recursive procedure $p$ is locally
%time monotonical, then the timing behavior is monotonically distributed too.
%\begin{proof}
%Let $f_1\in\F_i$ and $f_2\in\F_j$, $i\leq j$.
%% error corrected 9.3.95: f_i -> f_1, f_j ->f_2
%We prove the theorem by double induction on the recursion depth.
%
%\begin{itemize}
%\item
%At first let $i=0$.
%We prove by induction on $j$ that our claim is correct.
%\begin{itemize}
%\item
%If $j=0$, we have
%$$
%\T(f_1) = \t(f_1) \leq \t(f_2) = \T(f_2).
%$$
%\item
%If $j>0$, we obtain
%$$
%\T(f_1) = \t(f_1) \leq \t(f_2) \leq \t(f_2) + \sum_{\of_2\in\R(f_2)} \T(\of_2) = \T(f_2).
%$$
%\end{itemize}
%\item
%Next we consider $i>0$.
%
%For $j\geq i$ we derive
%\begin{eqnarray}
%\T(f_1) &=& \t(f_1) + \sum_{\of_1\in\R(f_1)} \T(\of_1)\label{Tf1} \qquad\text{and}\\
%\T(f_2) &=& \t(f_2) + \sum_{\of_2\in\R(f_2)} \T(\of_2)\label{Tf2}.
%\end{eqnarray}
%By induction hypothesis the sum in~(\ref{Tf1}) is smaller than or equal to
%the sum in~(\ref{Tf2}).
%Since $\t(f_1)\leq\t(f_2)$, we get
%$$
%\T(f_1) \leq \T(f_2).
%$$
%\end{itemize}
%Hence the lemma is proved.\quad\qed
%\end{proof}

\begin{slide}
complex applications $\Rightarrow$
{\em parameter space morphisms\/}
\begin{itemize}
\item
concentrates on essential parts of the parameter space
\item
simplifies analysis
\end{itemize}
\end{slide}

As a practical application we present {\em balanced trees\/}
which are interesting since operations defined upon them can easily
be implemented by recursion and their recursion depth is usually bounded above
by $O(\ld n)$, where $n$ denotes the number of nodes in the tree.
We study BB$[\alpha]$-trees (cf.~\cite{meh:sort}) in some detail.
In Fig.~\ref{bb_alpha_spec} part of the specification of a BB$[\alpha]$-tree package
is given.
Figure~\ref{bb_alpha_imp} shows all additional functions to be given
by the programmer for implementing the recursive procedure {\tt insert}.
By applying the shown morphism, timing properties can be deduced
involving the current number of nodes in the tree.
\begin{slide}
\begin{center}
{\bf BB$[\alpha]$-trees}
\end{center}
\begin{verbatim}
generic
  size:  natural;
  alpha: float;
  type element is private;
  with function "<"(left,right:element)
    return boolean is <>;
package BB_alpha_tree is

  type tree is limited private;

  procedure insert(an: element; into: tree);
  -- other operations suppressed

private
  type tree is
    record
      current_size: natural;
      -- the current number of nodes in the tree
      -- other stuff representing the tree
      -- structure suppressed
    end record;
end BB_alpha_tree;
\end{verbatim}
\end{slide}

\begin{slide}
\begin{verbatim}
package body BB_alpha_tree is

  subtype node_number is natural range 0 .. size;
  
  recursive procedure insert(
      an: element; into: tree)

    with function morphism(t: tree)
        return node_number is
    begin
      return t.current_size;
    end morphism;

    with function recdep(
        current_size: node_number)
      return natural is
    begin
      return floor(1.0+(ld(current_size+1)-1.0)/
        ld(1.0/(1.0-alpha)));
    end recdep;

  is
  begin
    -- recursive implementation of insert
  end insert;
end BB_alpha_tree;
\end{verbatim}
\end{slide}

More details on real-time recursions can be found in~\cite{bli:eumirtrc}
and in~\cite{bli:rtrecurr}.
%\end{section}

\renewcommand{\O}{\cal O}
\newcommand{\WCP}{\text{\sf WCP}}
\newcommand{\gWCP}{\text{\sf gWCP}}
\newcommand{\aWCP}{\text{\sf aWCP}}
\newcommand{\WCS}{\text{\sf WCS}}
\newcommand{\gWCS}{\text{\sf gWCS}}
\newcommand{\aWCS}{\text{\sf aWCS}}

\begin{slide}
{\bf Examples of locally time-monotonical recursions}
\begin{itemize}
\item
Mergesort
\item
Balanced Tree Structures
\end{itemize}
\vspace{0.5cm}
{\bf Examples of not locally time-monotonical rec.}
\begin{itemize}
\item
Ackermann Function
\item
Quicksort
\end{itemize}
\end{slide}

\begin{slide}
{\bf Worst-Case Performance Estimates on the Specification Level of Classes}
\vspace{0.5cm}
\begin{itemize}
\item
the view from inside $\to$
WCP-tool
\item
the view from outside $\to$
information provided at the interface
of objects/classes
\end{itemize}
\end{slide}

Clearly, the WCP-tool mentioned above also has to check
whether the information specified at the object's interface conforms
to the values derived from its implementation.
In fact both timing and space estimates of the specification must always be
greater than or equal to
the values of the implementation, otherwise no executable program should be generated.
Of course, separating specification and implementation of timing information
greatly improves modularization and facilitates testing of the real-time system.

In the following, we will discriminate between two important cases:

\begin{slide}
\newcommand{\gWCP}{\text{\sf gWCP}}
\newcommand{\aWCP}{\text{\sf aWCP}}
\begin{center}
{\bf Outside view}
\end{center}
\vspace{0.5cm}
\begin{enumerate}
\item
internal state of object described by {\em generic parameters\/}
\begin{itemize}
\item
{\em constant\/} during life-time
\end{itemize}
$\to$ {\em generic worst-case performance\/} estimates ($\gWCP$)
\item
internal state of object reflected by a {\em state parameter\/}
\begin{itemize}
\item
may change if the internal state changes
due to a method call
\end{itemize}
$\to$ {\em actual worst-case performance\/} estimates ($\aWCP$)
\end{enumerate}
\end{slide}

In the following we investigate how $\gWCP$ and $\aWCP$ estimates can be
added to Ada95.

\begin{slide}
{\bf Generic Worst-Case Performance Estimates}
\vspace{0.5cm}
\begin{itemize}
\item
exploit generic packages and generic subprograms already present in Ada95
\item
generic parameter mechanism
\end{itemize}
\end{slide}
\end{subsection}

\begin{slide}
{\bf Actual Worst-Case Performance Estimates}\\
\\
{\bf State parameters}
\\
\begin{enumerate}
\item
{\em generic out parameters}\\
$-$ type managers\\
$+$ object managers
\item
{\em out discriminants}\\
$+$ readable parts even if (limited) private type\\
$+/-$ {\em not\/} constant\\
\\
$+$ type managers
\item
{\em implement an operation returning the state}
\begin{enumerate}
\item
fix a certain name\\
$-$ type of state parameter has to be known in advance
\item
extend a predefined abstract data type {\tt real\_time}\\
$-$ type of state parameter has to be known in advance
$\Rightarrow$ envelope it into a generic package\\
$-$ artificially increases the number of tagged types\\
$-$ late binding $\Rightarrow$ overestimating the performance\\
\newpage
$-$ {\em controlled\/} real-time type $\Rightarrow$ problems
\begin{itemize}
\item
multiple inheritance
\item
$\Rightarrow$ access discriminants, only allowed for limited\\
types\\
\end{itemize}
$\Rightarrow$
only {\em limited\/} controlled real-time types, no assignment\\
$+$ if tagged and limited controlled types and polymorphism are no problem
\end{enumerate}
\end{enumerate}
\end{slide}

%\begin{slide}
%all these problems $\Rightarrow$ justify proposed language extensions
%\end{slide}
\end{itemize}
%It is described in Section~\ref{tagged} in more detail.
\end{enumerate}

\begin{slide}
\begin{itemize}
\item
internal representation is a protected type\\
$\Rightarrow$ changing the state is an atomic action\\
\item
generic out parameters, discriminants $\to$ guaranteed by the language (extension)
\item
{\tt real\_time} type extension $\to$ programmer is responsible
\end{itemize}
\end{slide}

As already mentioned, we are implementing a precompiler which translates
Ada95 code augmented with our language extensions to pure Ada95 code.
Out discriminants are mapped to ordinary record components
which are enveloped in a protected type.
In addition, a primitive operation returning the enveloped record component
is added to the set of primitive operations.
Thus reading the out discriminant actually is a function call to this
primitive operation which internally is forwarded to the protected object.

Similarily, our precompiler envelops generic out parameters in protected objects just
as it does for out discriminants.
The generic out parameter itself is mapped to a function within the generic package.
Again, reading the generic out parameter actually is a function call
which internally is forwarded to the protected object.
\end{subsection}

\begin{slide}
\newcommand{\gWCP}{\text{\sf gWCP}}
\newcommand{\aWCP}{\text{\sf aWCP}}
{\bf Real-Time Methods}
\vspace{0.5cm}
\begin{itemize}
\item
Each method $\M_i$ augmented with
functions computing $\gWCP$ and $\aWCP$ estimates.
\item
In addition information has to be provided, how 
the state parameters change when the method is executed.
\end{itemize}
%Usually, there will be several possible cases.
\end{slide}

As an example we study again BB[$\alpha$]-trees.
In particular we are interested in inserting data into the tree.
Let the number of nodes present in the tree be denoted by $R$
and let an upper bound of the number of nodes be denoted by $N$.
Thus $N$ plays the role of a generic parameter and $R$ plays the role
of a state parameter.

Figure~\ref{tree_insert_spec} shows a specification of a corresponding
Ada95 package.
For didactic purposes we have assumed rather simple $\gWCP$ and $\aWCP$ estimates.
The state parameter is incremented if the item has been correctly inserted into the tree.
It is left unchanged if the item has already been present in the tree.
In this case the exception {\tt item\_already\_present} is raised.
\begin{figure}
\begin{quote}\small
%%
%% Creator: ada2latex tree_ins.ads
%% Date:    Thu Feb  1 14:54:53 1996
%%
\expandafter\ifx\csname indentation\endcsname\relax
\newlength{\indentation}\fi
\setlength{\indentation}{0.5em}
\begin{flushleft}
\mbox{}\\
{\bf generic\/}\mbox{}\\
\mbox{}\\
\hspace*{2\indentation}N: {\bf in\/}  natural;\mbox{}\\
{\em \hspace*{8\indentation}-{}-\hspace*{1\indentation}generic\hspace*{1\indentation}parameter}\mbox{}\\
\hspace*{2\indentation}R: {\bf out\/} natural;\mbox{}\\
{\em \hspace*{8\indentation}-{}-\hspace*{1\indentation}state\hspace*{1\indentation}parameter}\mbox{}\\
\hspace*{2\indentation}{\bf type\/} item\_type {\bf is\/} {\bf private\/};\mbox{}\\
\mbox{}\\
{\bf package\/} Balanced\_Tree {\bf is\/}\mbox{}\\
\mbox{}\\
\hspace*{2\indentation}item\_already\_present: {\bf exception\/};\mbox{}\\
\mbox{}\\
\hspace*{2\indentation}{\bf procedure\/} Insert(item: item\_type)\mbox{}\\
\hspace*{6\indentation}{\bf with\/} duration $\leq$ log(N) {\bf and\/}  \hfill{\em -{}-\hspace*{1\indentation}gWCP}\mbox{}\\
\hspace*{6\indentation}{\bf with\/} duration $\leq$ log(R)      \hfill{\em -{}-\hspace*{1\indentation}aWCP}\mbox{}\\
\hspace*{6\indentation}{\bf new\/} R := R+1 $\mid$ R (item\_already\_present);\mbox{}\\
{\em \hspace*{8\indentation}-{}-\hspace*{1\indentation}R$+$1\hspace*{1\indentation}...\hspace*{1\indentation}if\hspace*{1\indentation}item\hspace*{1\indentation}has\hspace*{1\indentation}been\hspace*{1\indentation}inserted}\mbox{}\\
{\em \hspace*{8\indentation}-{}-\hspace*{1\indentation}R\hspace*{3\indentation}...\hspace*{1\indentation}if\hspace*{1\indentation}item\hspace*{1\indentation}is\hspace*{1\indentation}already\hspace*{1\indentation}present\hspace*{1\indentation}(exception)}\mbox{}\\
\mbox{}\\
{\em \hspace*{2\indentation}-{}-\hspace*{1\indentation}other\hspace*{1\indentation}methods\hspace*{1\indentation}suppressed}\mbox{}\\
\mbox{}\\
{\bf end\/} Balanced\_Tree;\mbox{}\\
\end{flushleft}
\end{quote}
\caption{Specification of Balanced Tree Insertion\label{tree_insert_spec}}
\end{figure}

\begin{slide}
\begin{center}
{\bf BB$[\alpha]$-trees}
\end{center}
\begin{verbatim}
generic

  N: in  natural;
    -- generic parameter
  R: out natural;
    -- state parameter
  type item_type is private;

package Balanced_Tree is

  item_already_present: exception;

  procedure Insert(item: item_type)
      with duration <= log(N) and  -- gWCP
      with duration <= log(R)      -- aWCP
      new R := R+1 | R (item_already_present);
        -- R+1 ... if item has been inserted
        -- R   ... if item is already present
                   (exception)

  -- other methods suppressed

end Balanced_Tree;
\end{verbatim}
\end{slide}

%\begin{slide}
%compiler's task $\to$ validate these specifications
%\end{slide}
It is the task of the compiler to validate the $\gWCP$ and $\aWCP$ functions
when the corresponding bodies (implementation parts) are compiled.
In our example, if a discrete loop is used for
implementing procedure {\tt insert}, this can be done easily at compile time.
Of course the details will be more complicated because we have only used
simplified $\WCP$ estimates.
\end{subsection}

More details can be found in a forthcoming paper~(\cite{bli:oort}).
\end{section}

\begin{slide}
\begin{center}
{\bf Project {\sf WOOP}}
\end{center}
\vspace{0.5cm}
\begin{itemize}
\item
Build a precompiler for Ada95
\item
Output is Ada95
\item
Precompiler is built by modifying GNAT
\end{itemize}
\vspace{0.5cm}
http://www.auto.tuwien.ac.at $\to$ Projects $\to$ {\sf WOOP}\\
\\
mail -s wpp wpp@auto.tuwien.ac.at $<$ ada-file.wpb
\end{slide}

%\begin{section}{Building a Precompiler by Modifying GNAT}
\begin{slide}
\begin{center}
{\bf Building a Precompiler based on GNAT}
\end{center}
\vspace{0.5cm}
%\setcounter{footnote}{0}
%Although it has ever been seen as an integral part of Project WOOP\footnote{
%WOOP, as an acronym for {\em Worst Case Performance of Object-
%Oriented Programs,} is a research project at the Department of Automation
%that is aimed at the determination of the timing-behavior of software for
%real-time systems.}
%to implement a tool that incorporates the theoretical results gathered,
%it would have been a bold proposition to build a timing analysis tool
%and a compiler for extended Ada95 from scratch. Therefore and due to limited
%time and resources it was the availability of GNAT\footnote{
%GNAT has been developed at New York University and its
%source code is distributed under terms of the  GNU General Public License
%as published  by the Free Software Foundation.}
%that saved us a lot of work. To be specific,
%it prevented us from having to code a complete front-end for the whole Ada
%programming language while providing every facility we needed to build upon
%in order to incorporate {\em discrete loops}, {\em real-time recursions}
%and {\em real-time objects} into Ada95.
%
%To further ease the task of implementation we decided to build a
%precompiler at first.
%This precompiler would have to translate our constructs to
%standard Ada. Any Ada compiler could then be used for translating the
%resulting code.
%%This not only freed us from the burden of object code generation which
%%of course is
%%much more elaborate than the generation of plain Ada code, but it
%%also eased debugging and testing of our tool.
%%
%%
%\begin{subsection}{Extending the GNAT System}
%
%GNAT itself is a front-end and runtime system that uses the back-end of GCC as
%a retargetable code generator. The front-end uses an Abstract Syntax Tree
%as the underlying data structure and it comprises three phases\footnote{
%Details can be found in ~\cite{dew:gnat}} 
%:
%\begin{itemize}
%\item{Syntactic Analysis}
%\item{Semantic Analysis}
%\item{Transformation of the AST to a representation suitable for the back-end}
%\end{itemize}
%Since only a minor part of the third phase is coded in a language other than
%Ada, the strengths of the Ada programming language also come into play in 
%the source code of GNAT which properly reflects the structure of the
%corresponding chapters of the Reference Manual ~\cite{ada95}.
%%is structured exactly the same as the
%%definition of the language given in ~\cite{ada95}. Each of the
%%twelve sections of ~\cite{ada95} is implemented by means of
%%a {\em library unit} or {\em subsystem} for any of the previously
%%mentioned three phases.
%This leads to a very modular functional design with no coupling
%between unrelated units.
%
%Despite the fact that the current release of GNAT has already been validated,
%development of the compiler is not yet finished.
%This means that modifications of the
%current release of GNAT might have to be taken over to a future release.
%Therefore we have attempted to keep modifications
%of the original code as small as possible while providing 'extra'-
%functionality in separate units that are called where appropriate
%(e.g.~on encountering keyword '{\em discrete}' during syntactic or
%semantic analysis).
%Because of arising dependencies it was on the other hand necessary to properly
%integrate our extensions into the original code.
%
%Although these requirements seem to contradict each other, the hierarchical
%library mechanism of Ada95 actually made it possible to fulfill both of them
%in most cases.
%\end{subsection}
%%
%%
%\begin{subsection}{A Case-Study on the Implementation of Discrete Loops}
%In this section we discuss the implementation of WPP---the
%WOOP Pre-Pro\-ces\-sor---with help of GNAT.
%Due to space considerations we picked  the discrete loop construct to
%serve as an example.
%%
%%
%\begin{subsubsection}{
%The Abstract Syntax Tree} (or AST for short) is perhaps GNAT's single most
%important data structure. It is constructed by the recursive descent parser
%and represents the input-program in a tree-like form. Subsequent processing in
%the front-end traverses the tree,
%transforming it in various ways and adding semantic information.
%Therefore no separate symbol table structure is needed.
%Every single piece of the Ada programming language finds its reflection in
%the AST. It has got nodes for statements, expressions, declarations, tasks
%and so on. We chose to treat discrete loops as a special form of for-loops
%and augmented the node N\_Loop\_Parameter\_Specification (a descendant of
%N\_Iteration\_Scheme which is a descendant of N\_Loop\_Statement)
%with nodes for the  {\em initial\_value} and the
%{\em list\_of\_iteration\_functions}.
%
%AST-access is governed by a high-level interface that
%checks for the validity of the required access (you cannot convince GNAT to
%provide you with a loop-body out of a case-statement, for example).
%Since, for obvious reasons, GNAT is very pedantic about this, we created our own
%high-level interface for WOOP-specific parts of the AST. A tool that checks
%for the consistency of such modifications is provided with GNAT.  
%\end{subsubsection}
%%
%%
\begin{itemize}
\item
Modify GNAT's Scanner and Parser
%was a straight-forward task since GNAT is very well structured. All we had to
%do was to make GNAT call our own function which would then parse the complete
%loop, put together the results in a subtree of the AST and return it to GNAT.
%\end{subsubsection}
%%
%%
\item
Semantic Analysis
%in general performs name and type resolution, decorates the AST with
%various attributes and performs all static legality checks on the program.
%Type resolution is done using a two-pass algorithm. During the first
%(bottom-up) pass, each node within a complete context is labeled with its
%type, or if overloaded with the set of possible meanings of each overloaded
%reference. During the second (top-down) pass,
%the type of the complete context is used to resolve ambiguities and to choose
%a unique meaning for each identifier in an overloaded expression
%\cite{dew:gnat}. In the case of a loop statement, GNAT has to analyze the
%loop's {\em iteration\_scheme} and the body of the loop. Since the body of
%a discrete loop does not semantically differ from any other loop, we leave
%the latter task to GNAT. This of course does
%not prevent us from performing special checks on the body after semantic
%analysis has been completed.
%
%The sole purpose of the analysis of the {\em iteration\_scheme} of a
%discrete loop is to determine the type of the loop variable and to verify
%that this type is a {\em discrete} type. Please note that such an
%{\em iteration\_scheme} contains three entities that provide
%type-information:
%\begin{itemize}
%\item The expression providing the {\em initial\_value} for the loop variable.
%\item The {\em discrete\_range}.
%\item The iteration functions contained in the {\em list\_of\_iteration\_functions}.
%\end{itemize}
%\end{subsubsection}
%%
%% 
\item
Estimate the Number of Iterations of a Discrete Loop, Data flow analysis, \dots\\
$\to$ Mathematica

%Simple cases are solved by WPP itself.
%If things turn out to be more complex (e.g. complicated recurrence relations
%are involved), WPP passes this task over to Mathematica\footnote{
%Mathematica is a registered trademark of
%Wolfram Research Inc.},
%a commercial package for computer algebra.
%\end{subsubsection}
%%
%%
\item
Code Generation\\
$\to$ dump out
\end{itemize}
\end{slide}
%It is one of GNAT's built-in abilities to dump the source code from the
%generated tree. Although this feature was only meant for debugging purposes,
%it can be used for code generation too: as long as we
%are dealing with plain Ada95 code, GNAT can do all the work. On encountering
%a discrete loop, we take over to perform all transformations
%that are necessary in order to convert the loop to its equivalent in Ada95.
%The resulting code is then printed and control returned to GNAT.
%\end{subsubsection}
%
%More details concerning the implementation of WPP can be found in~\cite{bur:woop_gnat}.
%\end{subsection}
%\end{section}
%
\begin{slide}
\begin{center}
{\bf Concluding Remarks}
\end{center}
\vspace{0.5cm}
\begin{itemize}
\item
Augment Ada with additional real-time language features
$\Rightarrow$ improvements for {\sf WCP} estimates
\item
\begin{itemize}
\item
discrete loops
\item
real-time recursion
\item
augment interfaces of classes with timing information
\end{itemize}

\item
runtime checks
\item
compile time checks
\end{itemize}
\end{slide}
\end{section}

\end{document}

