%--> do tex %F -l -l -d
% > do TEX -x -latex %F
% > do  TEX -latex %F

\documentstyle[12pt]{article}
\setlength{\parindent}{0mm}
\setlength{\textwidth}{168mm}
\setlength{\textheight}{260mm}
\setlength{\parskip}{4.33mm}
\setlength{\oddsidemargin}{0mm}
\setlength{\topmargin}{-10mm}
\setlength{\headheight}{0mm}
\setlength{\headsep}{0mm}
\setlength{\topskip}{0mm}
\setlength{\footheight}{0mm}
\setlength{\footskip}{0mm}
\renewcommand{\thefootnote}{\alph{footnote}}
\renewcommand{\baselinestretch}{0.833}
\flushbottom
\newcounter{secno}\setcounter{secno}{1}
\renewcommand{\thepage}{}

\begin{document}
\bibliographystyle{plain}
%\maketitle
\ \\
\vspace*{8mm}
\ \\
\hspace*{21mm}\parbox[t]{146.5mm}
     {\LARGE From {\sc lotos} to {\sc c}}
\vspace*{4.33mm}\\
\hspace*{21mm}\parbox[t]{146.5mm}
	{\bf
	J.A. Ma\~nas	\\
	T. de Miguel
	}
\vspace*{0mm}\\
\hspace*{21mm}\parbox[t]{146.5mm}
     {
     Dpt. Ingenier\'{\i}a Telem\'atica	\\
     E.T.S.I. Telecomunicaci\'on	\\
     Univ. Polit\'ecnica de Madrid	\\
     E-28040  Madrid, Espa\~na
	}
\vspace*{0mm}\\
\hspace*{21mm}\parbox[t]{146.5mm}
     {
     {\tt jmanas@dit.upm.es}		\\
     {\tt tmiguel@dit.upm.es}
     }
\vspace*{4.33mm}\\
%\begin{abstract}
\hspace*{21mm}\parbox[t]{146.5mm}
  {
  {\sc Lotos} is a very high level language,
  too high level to allow direct implementation,
  although a development system would be very appreciated,
  and would greatly help to the acceptance of the language
  as a practical specification technique.
  Our system permits the implementer to refine a very abstract specification
  until it becomes a running piece of code.
  The output are portable C programs.
  This paper focuses on the functionality
  and features of the {\sc lotos} compiler
  currently under development at Madrid.
  }
%\end{abstract}
\vspace*{4.33mm}

\thesecno.\ \ \ {INTRODUCTION}.\addtocounter{secno}{1}
%\section{Introduction}

Although there may be different definitions of the concept of
implementation,
our understanding is that implementing means
derivig a real or physical system,
able to intercat with its environment.
More concretely,
we are mainly interested on getting programs that run on computers
and behave according to a {\sc lotos} specification.

Implementation may mean prototyping in many practical situations.
It is a mean of providing a working module
that is limited to demonstrating the functionality of the
specification.
The purpose of such a prototype is to ascertain
that the functional requirements reflect and solve the user needs,
and that the functional requirements can be implemented,
that is,
no impossible functions are required.
Sometimes the prototype is much enough for what is needed,
and no further implementation is required,
but if time or space are critical,
manual implementation may be required to tune the system.

Thus,
a practical compiling tool must be able to produce fast prototypes,
and must foresee the need to be part of a bigger system,
or even to rely on hand coded submodules.
It is expected that an application will use modules generated by this
compiler and other modules provided by the user.
The generated module may be "called" from other modules
and the other way round,
and collaborate with them in a flexible manner.

Due to the semantic gap between specification and implementation,
the users of the tools are expected to provide information to the
compiler covering implementation decisions.
This extra information shall be integrated in the compiler input in
order to keep a consistent specification of the implementation.
After providing this extra information,
the process will run automatically.

Output code shall be source code in a standard programming language in
order to permit readability and portability.
Readability is required both for checking the correct generation of code
(a very important item for experimental prototypes that require
extensive and careful debugging),
and for allowing hand tuning to meet efficiency requirements
after module profiling.
Portability is required for obvious reasons of usefulnes in general,
and in particular because it is extremely frequent that a protocol
will run between different computers.

Language C was chosen as the target language for being readable,
portable, widely available, close to machine details, efficient,
widely experienced as target language, and has a big pool of tools
that can be used without licensing problems.

\thesecno.\ \ \ {DESIGN PROCESS}.\addtocounter{secno}{1}
%\section{Design Process}

Compiling means merging a specification of behaviour
with implementation decisions
in order to produce a module
able to fit a real application
that runs on some computer.

A mechanism of annotations has been devised that permits the
integration of both kinds of information into the same file,
thus simplifying maintenance.
Annotations are a special class of {\sc lotos} comments
that are interpreted by the compiler.
The main ideas for annotations design are as follows

\begin{enumerate}
\item
  They do not modify the transition system that is specified in {\sc lotos}.
  Such modifications shall be done by editing the source specification
  itself.
  A support tool for assessing some kind of observational equivalence
  would be advisable.
\item
  They have some recognizable effect on the interface of the implemented
  system,
  that is,
  they perform some observable action associated to state transitions
  specified in {\sc lotos}.
\item
  Environment state may be accessed and allowed to delay possible
  synchronizations until a certain state is reached,
  e.g. waiting for 5 seconds or
  waiting until a peripheral warms up.
\end{enumerate}

Many of the annotations are in fact program fragments that are included in
the output of the compiler.
Those fragments are executed when the state
machine makes the transition to which they are associated.
If there are several fragments associated to a transition,
then they are executed in parallel
(or in a random order,
over which the user has no control).

On a properly annotated specification,
the different parts of the compiler work unattended.
There is a neat difference between the behaviour and the data part.
In fact,
the {\sc lotos} compiler is the result of the close cooperation of a
behaviour compiler {\em lbc},
and a data compiler {\em ldc}.
Surely the first steps,
syntax and semantics,
are shared.
The front end terminates providing a collection of processes on one hand,
and a single data type on the other one.

\thesecno.\ \ \ {BEHAVIOUR COMPILER}.\addtocounter{secno}{1}
%\section{Behaviour Compiler}

Leaving out the data types,
a {\sc lotos} specification can be seen as a collection of behaviour
units,
{\em processes},
that interact.
Each behaviour unit can be modelled as a finite automaton
that synchronizes with the rest.
In terms of C language,
the {\sc lotos} compiler generates reentrant code,
organized as one C function per {\sc lotos} process.
These pieces of code behave as processes in conventional O.S.,
that is,
relay on {\em system calls} to interactuate.
The Run Time Support organizes the cooperation between units.
The kind of information held in the Kernel
is quite similar to the standard frames used in O.S.,
obviously adapted to the very sophisticated synchronization mechanism
of {\sc lotos}:
{\em n-way symmetrical rendez-vous}.

Without annotations,
the output of {\em lbc}
is an automaton that moves according to the {\sc lotos} specification,
but isn't able to interactuate with the environment.
The following annotations are available

\begin{enumerate}
\item
  {\bf Output actions}

  Associated to {\em action denotations} there may be specified
  actions to be performed.
  The automaton will perform it upon successful synchronization.
  For example,

  {\tt send !m (*| C {\em send message m} |*); REST}

  The body of the action is plain C code.

\item
  {\bf Delays}

  The offer of an action may be delayed by a specified number of seconds.
  For example,

  {\tt (*| delay 5 |*) timeout !recv; REST}

  where the {\tt timeout} action is not offered till 5 seconds are
  over.
  Of course,
  in the meanwhile another action may disable the delayed one,
  for instance by means of a choice $[]$ operator,
  thus giving up any opportunity for any timeout to happen.

\item
  {\bf Synchronize with the world}

  The offer of an action may be delayed till a user provided predicate
  becomes true.

  {\tt (*| wait isdata() |*) read ?d: data; REST}

  Where an active wait is carried on by repeatedly checking the predicate.
  As previously,
  a ``choice'' action may overtake the wait.

\item
  {\bf Provide defaults for value negotiation}

  {\sc Lotos} permits synchronization between gates with a collection
  of requirements.
  For example,

  {\tt g ?m: int [P1(m)]; M |[ g ]| g ?n: int [P2(n)]; N}

  The compiler permits to associate to the offer {\em default values}
  that are checked to fulfill the predicates.
  If no defaults were provided,
  no action would be carried on,
  since ad-hoc heuristics would be needed to generate values.
  Better let the implementer to state the heuristics directly.

  Defauls may be provided either as a list of values to try,
  and/or as a user function that is iteratively called to provide
  a collection of values,
  till someone succeeds.
\end{enumerate}

We are currently evaluating the opportunity of an effective {\em cut
off} annotation,
something that actualy prunes the synchronization tree upon user
provided data.
This effect can be achieved by means of tricky {\em waits} or {\em delays},
but the situation happens so often that an explicit annotation seems
adequete. 

\thesecno.\ \ \ {DATA COMPILER}.\addtocounter{secno}{1}
%\section{DATA COMPILER}

The data part of {\sc lotos} is much more complex to implement.
First,
there are plenty of constructions to combine types,
and derive new types,
and cope with scope of declarations.
One of the very first steps in compiling is removing all this user
oriented machinery.
The process is known as {\em flattening}
and the output is having just one,
{\em canonical}, type for the whole specification.

Second,
users must be aware that they are specifying algebraically.
Thet means that standard equational reasoning must be applied to
derive conclusions about actual data.
That,
strictly speaking,
implies using theorem proving techniques,
what sounds far unreasonable for actual implementations.
The approach we use is to require the implementer to certify that the
canonical type may be understood as a liable rewrite system.
There are plenty of tools in the research community to check that fact,
and even to help the implementer in modifying the original
specification till the type may be securely implemented as a rewrite system.
It is our personal experience,
that 90\% of the specifications are directly executable as rewrite systems,
but it is advisable to check it.

Third,
the rewrite system itself must be produced.
The data part compiler provides a coded rewrite engine for the
concrete data.
For efficiency reasons,
it is not a generic rewrite engine working on some data base,
but a specific rewrite engine optimized for the user type.
It is enriched with memory management features,
and a drawing function to help debugging.

The default behaviour of the compiler may be easily overtaken in order
to introduce user coded data types.
This situation is rather usual since there are many types directly
implemented by the hardware
(as booleans or integers)
where the compiled versions would be highly inefficient.
In general,
it is usually the case that libraries of data types are used
despite its algebraic specification in {\sc lotos}.
For those situations,
a collection of annotations is provided.

\begin{enumerate}
\item
  {\bf name}.

  The implementation of {\sc lotos adt}s is based on unique identifiers.
  Those are numbers generated by the semantics analyzer.
  This is required to cope with overloading.
  C functions names are choosen after those unique identifiers,
  thus getting rather obscure codings
  (e.g. \verb/g12/).
  That's necessary,
  but makes the code extremely unconvenient for humans.
  The first approach to tackle with this problem is to keep user
  identifiers.
  There are two limits to this.
  (1) there may be overloaded identifiers in {\sc lotos},
  but C doesn't support overloaded names on functions.
  (2) there may be valid {\sc lotos} identifiers
  (e.g. \verb/+/)
  that are not valid C identifiers.
  The solution to both problems was to add an annotation to those
  identifiers that may cause trobles.

  \begin{verbatim}
      opns
        + (*| name plus |*): nats, nats -> nats
  \end{verbatim}

\item
  {\bf extern}.

  In order to improve the system efficiency,
  it is often the case that the basic types of C may be used
  (e.g. integers),
  or that efficient implementations may be directly coded in C
  (e.g. for sets).
  It is desirable that these ``optimizations'' interface smoothly with
  the code generated by {\em ldc}.
  There is an annotation for it,
  \verb/extern/.
  Either sorts and/or operations may be annotated as \verb/extern/,
  with the obvious implications
  (i.e. operations on \verb/extern/al sorts must be \verb/extern/al
  too).

\item
  {\bf equal}.

  For \verb/extern/al sorts,
  {\em ldc} must be instructed about the {\em equal} function,
  since data representation is up to the user.
  Code will be generated to refer to the function provided by the user
  to check equality of terms of that sort.

\item
  {\bf free}.

  For \verb/extern/al sorts,
  {\em ldc} must be instructed about how to free memory allocated for terms
  of this sort,
  since data representation is up to the user.
  Code will be generated to refer to the function provided by the user
  to free terms that involve subterms of this sort.

\item
  {\bf draw}.

  For debugging,
  there is an obvious need to be able to print the terms in a user
  friendly format.
  That's pretty easy for {\em ldc} data types
  (i.e. a classical tree traversal algorithm),
  but for user provided representations,
  the user must provide its printing function too.
  Of course,
  {\em ldc} keeps track of {\sc lotos}
  and/or \verb/name/ annotated identifiers.
\end{enumerate}

We are currently evaluating the opportunity to introduce an {\em
exception} machanism associated to operations.
The exception would be raised if a user provided predicate on input
arguments fails.
It would be a mechanism of coping with partial functions,
that are a very usual case,
despite the fact that {\sc lotos} doesn't support them.
Obviously,
this kind of annotations would severely affect the algebraic
interpretation of the data types,
but seems to be quite useful in actual practice.

\thesecno.\ \ \ {MODULE INTEGRATION}.\addtocounter{secno}{1}
%\section{Module Integration}

The {\sc lotos} compiler provides two pieces of code.
(1) A collection of C functions to implement the behaviour part,
named APP.lbc;
and (2) a collection of C functions to implement the data,
named APP.ldc.
These modules are to be loaded alltogether with the Kernel and the
modules provided by the user,
APP.ub for the user behaviour,
and APP.ud for the user provided data implementations.
The following picture shows the combination of modules.

%\begin{center}
%  \begin{picture}
%
%  \end{picture}
%\end{center}

There are basically two mechanism to interactuate with other modules.
Either the embedded scheduler of the Kernel is used,
or an external scheduler steers the generated code.
In the first,
and most usual case,
external modules are called upon internal decissions.
In the second case,
the code is required to execute in a slave mode,
upon external request.
In this second case,
the compiled module ``executes'' one step and returns control to the
calling module.
A ``step'' is defined as one action synchronization
or nothing to do but {\em waits} and/or {\em delays}.

\thesecno.\ \ \ {STATUS}.\addtocounter{secno}{1}
%\section{Status}

There is currently a prototype compiler running on Sun-3 machines with
BSD 4.2 UNIX.
It is been used in Madrid to develop non trivial implementations of
protocols.
It cannot be so far regarded as a production tool,
but under experimentation and debugging.
The collection of annotations required keeps growing,
as the need arises,
but its rate is coming down.
That means that the current offer is quite enough for actual protocols.
Compiling time is not trivial,
but reasonable.
Execution time is quite acceptable,
but for critical timeouts.
Space requirements are too big,
and further work is being carried on to decrease it.
Certainly,
there is plenty of self-test code embedded in the output,
code that could be removed
when we become more confident with its behaviour.

To give some figures,
people at the department are currently developing a medium size
protocol that is able to transfer data in a connection mode,
with a data segmentation feature.
The data types are coded in ASN.1.
The protocol is more or less equivalent to a class 0 transport
protocol.
The {\sc lotos} specification is 1000 lines long,
were only signatures are provided for the data types,
since the whole implementation is external.
User written code (bahaviour $+$ data) is about 7000 lines.
The time required by the compiler to process the {\sc lotos}
specification is $~30$ seconds,
where $~40$ seconds must be added to run the C compiler and load
together the pieces.
The generated module uses 500K.
It must be noted that a big portion of the code is not actually used
(it should be organized as a library of data types rather than a huge
collection of types and operations).
If only actually used data were loaded,
the size would come down to some 350K.
A hand coded implementation is been developed at the same time by a
parallel team.
This seconf team shares the data types,
but has recoded in plain C the {\sc lotos} specification.
The resulting module has a lower size, 370K.
These data are not definite,
since the product is currently under development.
We plan to carefully evaluate both implementations when both of them
are running,
after clipping out redundant code and so.

%\section{BIBLIOGRAPHY}
\addtocounter{secno}{1}\thesecno. \ \ \ {BIBLIOGRAPHY}.

\begin{enumerate}

\item
  ISO IS 8807,
  {\em Information Processing Systems, Open System Interconnection,
  {\sc lotos}, A Formal Description Technique Based on the Temporal Ordering
  of Observational Behavior}.
  ISO, July, 1988.

\item
  D.E. Knuth and P.B. Bendix.
  {\em Simple Word Problems in Universal Algebras}.
  Computational Problems in Abstract Algebra,
  J. Leech (ed.),
  Pergamon Press, 1969.

\item
  P. Lescanne.
  {\em Computer Experiments with the REVE term Rewriting System Generator}.
  10th POPL Conf. Austin, Texas, 1983.

\item
  J.A. Ma\~nas.
  {Dining Philosophers: a Constrained Oriented Specification}.
  {\sc sedos/c3/wp/40/m}, E.T.S.I. Telecomunicaci\'on, Madrid,
  July, 1987.

\item
  J.A. Ma\~nas.
  {\em A Tutorial on {\sc adt} semantics for {\sc lotos} users.
  Part I: Fundamental Concepts.
  Part II: Operations on Types}.
  Dpt. Telem\'atica, May, 1988.

\item
  J.A. Ma\~nas,
  T. de Miguel
  and H. van Thienen.
  {The Implementation of a Specification Language for OSI Systems}.
  Intnl. Zurich Seminar on Digital Communications.
  March 1988, pp. 103-107.

\item
  J.A. Ma\~nas
  and T. Robles.
  {\em The experience of Compiling an {\sc adt} language}.
  Submitted to CIL'89, Barcelona, March 1989.

\item
  J. de Meer.
  {\em Tutorial on {\sc lotos} Data Types}.
  Hahn-Meitner-Institut Berlin Gmbh. March 1986.
  Vol. 92, Lecture Notes in Computer Science, Springer Verlag, 1980.

\end{enumerate}

\end{document}

% Local Variables:
% mode: indented-text
% comment-column: 32
% comment-end: ""
% comment-multi-line: nil
% comment-start: "%"
% comment-start-skip: "[^\\]\\(\\\\\\\\\\)*%+ *"
% End:
