%> do tex %F -l -l -l -d -p

\def\TOPO{{\sc topo}}
\def\LOTOS{{\sc lotos}}
\def\LBM{$\Lambda\beta$-machine}

\documentstyle{article}

\textwidth=16cm
\oddsidemargin=1cm
\evensidemargin=1cm
\textheight=22cm
\topmargin=0cm
\parindent=0mm
\parskip=4mm
\unitlength=1mm

\title{The \LBM\ in TOPO}

\author{Jos\'e A. Ma\~nas                       \\
        Joaqu\'{\i}n Salvachua                  \\[1ex]
        Dpt. Ingenier\'{\i}a Telem\'atica       \\
        E.T.S.I. de Telecomunicaci\'on          \\
        Univ. Polit\'ecnica de Madrid           \\
        E-28040 Madrid, SPAIN                   \\
                                                \\
        {\tt <lotos@dit.upm.es>}
        }

\date{January 15, 1991}

\begin{document}
\maketitle

\begin{abstract}
\TOPO\ is a \LOTOS\ compiler.
It is basically built up of a semantics analyzer,
a behaviour compiler,
and a data compiler.
This document deals with the behavioural part,
assuming but not presenting the others.
A \LBM\
(\LOTOS\ Behaviour Machine)
is presented as an intermediate stage between
specifier's \LOTOS\ text and the code generated for a systems
programming language.
The conception and detailed design of this virtual machine is
presented by describing the abstract model,
and its language.
Some examples are used to show the details,
and lastly some hints are provided for the implementation of
this virtual machine into {\tt C} code,
as currently performed in \TOPO.
\LBM\ definition makes very few assumptions about final implementation
details,
and therefore very many implementation designs may be derived from it.
\end{abstract}

\newpage
\tableofcontents
%\listoffigures
\newpage

\section{Introduction}
\LOTOS\ is a very complicated language both syntactically and
semantically.
Generation of executable code out of a \LOTOS\ specification is a task
that must be tackled in several stages to keep complexity under
control.
It is composed of two clearly distinguishible parts:
data and behaviour.

The data part is pretty complex due to the overloading and structuring
facilities,
and scope (or visibility) laws.
These conditions make a serious business of compiling the data part.
In this paper it is assumed that some kind of {\em library} exists
that provides the functions to perform operations on data types,
and most notably there is available a function to check for equality
of value expressions.

For the behaviour part,
a clear operational semantics is provided in IS-8807,
strongly based on the n-way symmetrical rendez-vous paradigm.
But it is complicated and itself,
and any complete implementation of the language
will have to deal with complex run-time synchronization facilities.

\LOTOS\ is able to specify highly concurrent systems,
where very many activities may be involved at any moment.

In this framework,
code generation is an enormous task,
and plenty of implementation decisions have to be taken
to move from very high level \LOTOS\ 
to very low level machine code.
Furthermore,
as experience is gained on the understanding of the language,
and implementation issues,
these decisions may be subject to severe changes.
In order to keep complexity under control,
and permit easy maintenence,
it is of paramount importance to identify intermediate stages,
and keep them clearly isolated.
If this isolation is achieved,
each one of the stages may be kept under control,
and may be easily replaced without disturbing the others.

In \TOPO\ two such intermediate stages are identified and used.
First stage is the \LBM\ presented below,
where the syntatic and semantic complexity of \LOTOS\ has been
resolved by the semantics analyzer,
and an abstract model to implement \LOTOS\ has been chosen.
Still it is open to several concrete implementations.
\LBM\ stands for \LOTOS\ Behaviour Machine.

The second stage is a systems programming language.
Currently, \TOPO\ relays on the widely available {\tt C} language.
The existence of this stage takes benefit from the very many {\tt C}
compilers in the world,
providing portability of code to many target machines.
Some hints about the decisions taken in \TOPO\ with respect to
deriving {\tt C} code are shown in this document,
but it is not presented to the last detail.

\begin{center}
\begin{picture}(0,70)
  \put(  0,60){\makebox(0,0){\LOTOS}}
  \put(  0,40){\makebox(0,0){\LBM}}
  \put(-20,20){\makebox(0,0){Ada}}
  \put(  0,20){\makebox(0,0){{\tt C}}}
  \put( 20,20){\makebox(0,0)[l]{prog. lang.}}
  \put(-20, 0){\makebox(0,0){3100}}
  \put(  0, 0){\makebox(0,0){Sun-4}}
  \put( 20, 0){\makebox(0,0)[l]{target machine}}

  \put(  0, 57){\vector(0,-1){14}}
  \put(  0, 37){\vector(0,-1){14}}
  \put(  0, 17){\vector(0,-1){14}}
  \put( -3, 37){\vector(-1,-1){14}}
  \put( -3, 17){\vector(-1,-1){14}}
  \put(  3, 37){\vector(1,-1){14}}
  \put(  3, 17){\vector(1,-1){14}}
\end{picture}
\end{center}

\LBM\ has been designed to permit other approaches.
Still,
it has not yet been tried to derive code for any other language than
{\tt C},
nor any other concrete implementation than the one in \TOPO,
that is under the UNIX Operating System.

\TOPO\ accepts \LOTOS\ specifications that may be extended with
annotations.
These annotations are, syntactically,
an identifiable class of comments.
There contents are expressions or statements in some 
systems programming language.
They may appear in a few predefined productions of the language,
thus becoming a syntactically fixed extension of \LOTOS.
Semantically,
annotations go unprocessed through the \LBM,
and are only interpreted when code
for a systems programming language is produced,
and passed to an appropriate compiler.

Currently,
these annotations contain expressions and statements
for the {\tt C} programming language.
If annotations were written for any other language,
\LBM\ would not notice the difference.
For instance,
annotations could be written in Ada,
and just be handled to an Ada compiler without \LBM\ distrurbing the
process.

\medskip

Some errors are frequently found when speaking about \LOTOS\
implementations.
It is far too easy to identify \LOTOS\ processes and Operating System
processes,
and make a one to one mapping.
That would be nice, but may be completely unrealistic,
and it must be clear that the \LBM\ presented in this paper
leaves that path open to future considerations.
There are two basic reasons to take into account before taken such a
mapping for given.
\begin{itemize}
\item
  Tail recursive process instantiation just models conventional loops
  ({\em for, while, until, \ldots} loops in structured programming).
  It may be implemented as real processes, 
  but the overhead is too high to be worth.
\item
  There is ``real'' paralellism in \LOTOS\ expressions built out of the
  {\em parallel} operators.
  These parallel threads of control do not get a name in the user's
  specification,
  it is not necessarily a {\tt process}.
  And the other way round,
  a single name,
  a \LOTOS\ {\tt process} may well be behaving as a couple of unnamed actual
  processes at run-time.
\end{itemize}

\LBM\ carefully avoids taking any compromising decision on this
critical issue of mapping to real machine processes.
Concurrent threads of control exist,
but its mapping is delayed to the code derivation stages.

\section{The Abstract Model}
This section deals with the conceptual design of the virtual code that is
generated by \TOPO\ out of an abstract \LOTOS\ specification.
The main problems or issues to consider are 
\begin{itemize}
\item
  n-way concurrency,
  where $n$ is dynamically decided.
\item
  n-way symmetrical rendez--vous,
  where $n$ is dynamically decided.
\item
  dynamic relabelling of gates
\item
  non-determinism
\end{itemize}

These issues prevents the generation of ``linear code'' as in more
conventional compilers.
In those,
the code generated by the compiler is usually put under control of the
Operating System that exercises some scheduler to allocate resource
slots to each program: space and time.

The complexity of \LOTOS\ specifications requires a synchronization
model largely more powerful than the models usually coded into O.S.
(e.g. in UNIX).
But still the fundamental design of an O.S. may be resused to
implement \LOTOS,
taking advantage of large experience in the design of these pieces of
system programming,
and furthermore,
benefitting from CPU design oriented towards O.S. programming.

The run time abstract model of the code generated by \TOPO\
will consist of a centralized {\em Kernel}
and a number of processes around,
processes that will be named {\em Behaviour Units},
or just {\em BUTs} for simplicity.

The mapping of the Kernel and the collection of BUTs to O.S. processes
is an implementation decision to be taken later on.

The Kernel plays a similar role to {\tt init} in UNIX systems:
it is always running,
it is the first running entity,
it starts a number of BUTs,
takes care of further instantiations of BUTs upon older BUT request,
taken care of BUT cleanup upon termination,
and lastly but not least,
it is expected to orderly shut down when activity terminates.

BUTs are satellites with respect to the Kernel.
They are eventually instantiated to start activity under a concrete
context or environment selected by the Kernel.

BUTs may eventually require coordination with other BUTs,
in \LOTOS\ terms: need to synchronize.
The request for coordination is sent to the Kernel,
and it waits until it is fulfilled.

BUTs may eventually instantiate other BUTs.
This activity strictly corresponds to UNIX {\tt fork-}ing.
At every moment there may be several instantiations of a certain BUT,
each one acting in its own context (or environment),
with its own, private, internal state.

\section{The Language}
The \LBM\ is defined by its (programming) language.

The \LBM\ in \TOPO\ is a stack machine driven via a number of
instructions that may be classified into three major groups:
\begin{description}
\item[stack]
  The stack will be basically used to perform data evaluation,
  and as intermediate stage to store data for other instructions.
\item[automata]
  The activity of the BUT is described by means of a state machine
  that moves between states upon successful synchronizations.
\item[kernel]
  Eventually, the BUT will block waiting for some synchronization to
  take place.
  The BUT will make a {\em kernel call} to offer a rendez--vous.
\end{description}

\subsection{Stack Manipulation Instructions}
The \LBM\ has a polymorphic stack.
It may hold
booleans,
integers,
data, and
experiments.

There is a simple instruction to remove one item from the stack:
\begin{itemize}
\item[]
  \verb/POP/	\\
  removes top item from stack.
\end{itemize}

Then,
there a number of instructions for data,
and another set for gates.

Before coming to the details,
let us point out to a critical concept:
the distinction of contents and container.
For data there is a clear distinttion between a {\em variable}
that is a buck ready to contain a {\em value}.
Variables are local to BUTs,
but values may be exchanged.
Within a BUT a variable is uniquely identified (or denoted)
by its {\bf index}.
Values may exist either on the stack or on in some variable.

Just the same concepts apply to {\em gates},
but here there are no conventional names to refer to the container and
the content.
Still gate values may be shared between BUTs,
and each BUT will have an indexed set of gate containers.
Gate values may exist either on the stack
or on in some gate variable.

\subsubsection{Data Evaluation}
For data, values and variables, there is a collection of instructions:
\begin{itemize}
\item[]
  \verb/P_VAR variable_index/		\\
  push the index of a variable
\item[]
  \verb/P_VAL variable_index/		\\
  push a data value
\item[]
  \verb/L_VAR variable_index/		\\
  load a variable taking a value from the stack.
  The stack is not modified at all.
\item[]
  \verb/A_VAR variable_index variable_name/			\\
  associates a symbolic (external) name to an index.
  This instruction is intended for debugging.
\item[]
  \verb/I_VAR total_number_of_variables variable_parameters/	\\
  initialize.
  Makes room for a number of variables,
  and loads a number of them with initial data.
\end{itemize}
\verb/I_VAR/ is intended for BUT instantiation.
At that moment,
room is made for all the variables in the BUT.
Those coming as actual parameters are directly loaded.
The others, internal variables,
will be loaded as their values are known.

Usually,
data are evaluated on the stack
(as it will be shown below),
and eventually loaded into some indexed position by means of \verb/L_VAR/,
or directly used in the stack.
\begin{itemize}
\item[]
  \verb/EVAL operation number_of_arguments/	\\
  It takes $N$ operands from stack,
  and calls the {\tt operation} with so many arguments,
  pushing the result back to the stack.
  Arguments to \verb/EVAL/ are removed from the stack.
\item[]
  \verb/EVALC expression/			\\
  Evaluates the {\tt expression},
  pushing the result to the stack.
  It will be used for annotations.
  The expression may be in any programming language,
  and it will be just passed to the appropriate compiler.
  \LBM\ is not involved in its analysis at all;
  it just assumes that a data value will come out from the evaluation
  of such {\tt expression}.
\item[]
  \verb/EQUAL sort/				\\
  Takes $2$ arguments from the stack,
  that must be of sort {\tt sort},
  checks them for equality,
  and pushes the result (a {\tt boolean}) back to the stack.
\end{itemize}

Let's show a brief example on how it works.
Let it be the following \LOTOS\ value expression
\[ s (0 + s (x)) \]
where the semantics analyzer has assigned the following
(cryptic, but unique) identifiers to user operations:
\begin{center}
  \begin{tabular}{r l}
    $0$	& g431	\\
    $s$	& g437	\\
    $+$	& g501	\\
  \end{tabular}
\end{center}
and variable $x$ is at index $34$.

The generated code will look as follows
\begin{verbatim}
        EVAL g431 0           -- 0
          P_VAL 34            -- x
        EVAL g437 1           -- s (x)
      EVAL g501 2             -- 0 + s(x)
    EVAL g437 1               -- s(0 + s(x))
\end{verbatim}
and its overall effect is to load value $x+1$ onto the stack.

\subsubsection{Gate Manipulation}
Gate values are shared between BUTs,
and therefore thay may not be locally declared.
Furthermore,
each BUT instantiation may have different actual values for its formal
gates.
Therefore,
automata instructions will refer to gates indirectly through an index,
and an index to value translation must be dynamically provided.

Gates are using the stack to simplify kernel calls.
\begin{itemize}
\item[]
  \verb/P_GTE gate_index/		\\
  pushes the value
\item[]
  \verb/L_GTE gate_index gate_value/		\\
  loads a value at an indexed position.
  It is not using the stack.
\item[]
  \verb/A_GTE gate_index gate_name/		\\
  associates a symbolic (external) name to a gate variable.
  It is intended for debugging only.
\item[]
  \verb/I_GTE number_of_gates gate_parameters/		\\
  initialization.
  Makes room for so many gates,
  and loads a few of them.
\end{itemize}
\verb/I_GTE/ is intended for BUT instantiation.
If no new gate is declared within it,
the total number of gates is just the number of gate parameters,
and all of them are loaded upon instantiation.
There may be more gates
(e.g. created via the {\tt hide} operator)
for which room is made at instantiation time,
but there value is loaded later on,
by means of the \verb/L_GTE/ instruction.

\subsection{Automata Description Instructions}
This set of instructions is organized as pairs of instructions:
\begin{verbatim}
    B_xxx < argument > ...
      < body >
    E_xxx
\end{verbatim}
denoting the Beginning and End of some description.
This model has been chosen to easily match parenthesitation in
most programming languages.
Easy code generation out of this is a must.

These instruction pairs do not make any sense by themselves,
but strictly organized in a certain context.
Therefore,
we shall use a bit of BNF
(Backus--Naur Form)
to denote their relationship,
but still more information will be provided later on,
when dealing with the mapping from \LOTOS\ to \LBM.

The following conventions are followed:
\begin{center}
  \begin{tabular}{l l}
    \hline
    ITEM		& constant				\\
    item		& to be further refined			\\
    $[$ it $]$	& 0 or 1 instances of it		\\
    $[$ it $]*$	& 0 or more instances of it		\\
    $[$ it $]+$	& 1 or more instances of it		\\
    \hline
  \end{tabular}
\end{center}

\subsubsection{Comments}
This is the simplest pair
\begin{verbatim}
    B_CMT any_text
    E_CMT
\end{verbatim}
It may show up anywhere,
and no code is produced out of it\footnote{
  Nevertheless,
  for debugging purposes,
  a comment may be issued.
  For instance, current implementation in \TOPO\
  emits {\tt /* any text */}
  }.

\subsubsection{\LBM\ Code}
This is the start production or,
in other words,
the most external instruction pair in a \LBM\ description:
\begin{verbatim}
lbc ::
    B_LBC specification_name
      [ statement_annotation ]
      [ BUT_definition ]+
      [ predicate ]*
    E_LBC
\end{verbatim}
At the very beginning,
a number of statements may be introduced for some systems programming language.
It is done via the {\tt lbc} annotation.
These lines are copied unmodified to the output,
when code is being generated.
These lines will usually contain some small auxiliary function,
or some reference to external items,
for instance, via \verb/#include "some_file"/.

The code for \LBM\ will describe 1 or more BUTs.
There is always at list one,
corresponding to the {\em main} behaviour in a \LOTOS\ specification.
This main BUT is always labelled as $0$.
There are as many more as {\tt process} definitions in the source
specification.
Therefore there is a one to one mapping of processes to BUTs,
and BUTs may be identified by the name of their corresponding
{\tt process identifier}.

\LOTOS\ {\tt predicates} on {\tt action preffix expressions}
are translated into boolean valued functions.
Other predicates may be introduced via annotations.
These are boolean expressions for some programming language
that is unkown to \LBM.
This {\em external} predicates are just wrapped into a boolean valued
function and passed untouched to an appropriate compiler.

There may be no predicate at all in a \LOTOS\ specification.

The argument to \verb/B_LBC/ is just for debugging purposes.

\subsubsection{Behaviour Units}
\begin{verbatim}
BUT_definition ::
    B_CRT BUT_# process_name
      initial_state
      [ state ]*
    E_CRT
\end{verbatim}
Each \LOTOS\ {\tt process} is mapped to a \LBM\ behaviour unit.
It is modelled as a state machine.
There is at least an initial state,
and there may be more.

The second argument to \verb/B_CRT/ is just for debugging purposes.

\subsubsection{Automata States}
\begin{verbatim}
initial_state ::
    B_ENT 0
      BUT_initialization
      state_description
    E_ENT

state ::
    B_ENT state_#
      [ statement_annotation ]
      state_description
    E_ENT
\end{verbatim}

BUTs must be initialized upon instantiation.
It is just initializing gates and variables:
\begin{verbatim}
BUT_initialization ::
    [ I_GTE number_of_gates parameter_gates ]
    [ A_GTE gate_index gate_name ]*
    [ I_VAR number_of_variables parameter_variables ]
    [ A_VAR variable_index variable_name ]*
\end{verbatim}

Some activities may be carried on per state.
Local variables may be introduced via {\tt let expressions} in
\LOTOS.
These variables do exist from the initialization stage of the BUT
instantiation,
when all the variables in the BUT were created
(where creation just means making room for them).
But the value for a variable is not known at initialization time,
and it must be evaluated in a concrete state.

Furthermore,
guards may show up in certain states.
They must be evaluated,
and react to their result.

Once all the local variables are evaluated,
and guards are evaluated and found to be passed,
the automata may proceed to instruct the Kernel of the next
synchronization requirements.
\begin{verbatim}
state_description ::
    [ activity ]*
    kernel_call
\end{verbatim}

There may be zero or more {\tt let} expressions,
and/or zero or more guards to be evaluated:
\begin{verbatim}
activity ::
      local_definition
    | guard
\end{verbatim}

\subsubsection{LET Constructions}
{\tt let} constructs load a data value in one or more BUT variable(s).
\begin{verbatim}
local_definition ::
    B_LET
      [ load_variable ]*
    E_LET

load_variable ::
    value_expression
    [
      L_VAR var_index
      A_VAR var_index var_name
    ]+
    POP
\end{verbatim}
\verb/value_expression/ will evaluate a data expression onto the
stack.
This value is loaded into as many variables as required,
and removed.

\subsubsection{Guards}
\begin{verbatim}
guard ::
    B_GRD
      premiss
    E_GRD

premiss ::
      equation
    | boolean_value

equation ::
      value_expression
      value_expression
    EQUAL sort

boolean_value ::
      value_expression
      EVAL "true" 0
    EQUAL "bool"
\end{verbatim}
Both \verb/equation/ and \verb/boolean_value/ leave a boolean on top
of the stack.
If it is {\tt false},
the automata stops.
Otherwise, it may resume.

\subsubsection{Predicates}
\LOTOS\ specification predicates,
and those introduced via annotations,
are transformed into boolean valued functions.

For \LOTOS\ predicates the stack is used as for guard evaluation:
\begin{verbatim}
predicate ::
    B_PRD predicate_#
      premiss
    E_PRD
\end{verbatim}

For predicates introduced via annotations,
an expression
(in some programming language)
is evaluated and its value is interpreted as boolean:
\begin{verbatim}
predicate ::
    B_PRD predicate_# expression
    E_PRD
\end{verbatim}

\subsubsection{Statement Annotations}
Lastly,
statements may be introduced to be executed upon synchronization success.
These statements belong to some programming language,
and just go thru untouched towards an appropriate compiler to generate
machine code for them.
\begin{verbatim}
statement_annotation ::
    B_ANT
      statements
    E_ANT
\end{verbatim}

\subsection{Kernel Call Instructions}
State transition is performed upon successful synchronizations.
Since more partners may be involved in sysnchronizations,
each BUT will just inform the kernel of its synchronization
requirements,
both architecture and offers,
and wait for the kernel to inform of success.

There are actually two different roles of states.
Some of the states are visited autonomously,
while others are just visited as a consequence of a successful
synchronization.
The first ones are selected for convenience since thay permit easier
code generation,
but as far as the environment is concerned,
these are invisible.

The second subset of states is directly related to external
activities,
mostly to synchronization results.
\begin{verbatim}
kernel_call ::
      synchronization_pattern
    | synchronization_offer

synchronization_pattern ::
      hiding_expression
    | enable_expression
    | disable_expression
    | parallel_expression
    | choice_expression
    | BUT_instantiation

synchronization_offer ::
      stop_expression
    | internal_action
    | external_offer
    | exit_expression
    | delay_annotation
    | wait_annotation
\end{verbatim}

For most of these kernel calls,
with the exceptions of {\tt stop} and {\tt BUT instantiation},
the following state(s) is(are) indicated to the kernel.

\subsubsection{Hiding}
This instruction informs the kernel of the creation of new gate on
which synchronization may take place.
\begin{verbatim}
hiding_expression ::
      [ gate_to_hide ]+
    MK_HD next_state number_of_gates

gate_to_hide ::
    L_GTE gate_index gate_value
    A_GTE gate_index gate_name
    P_GTE gate_index
\end{verbatim}
The stack is used as intermediate storage for the values of the new
gate(s).

\subsubsection{Enabling}
The automaton may split into two automata related by a
\LOTOS\ {\tt enable} operator.
A few variables may be used to capture {\tt exit} values.
\begin{verbatim}
enable_expression ::
      [ return_variable ]*
    MK_EN enabling_state enabled_state number_of_variables

return_variable ::
    P_VAR variable_index
    A_VAR variable_index variable_name
\end{verbatim}
The stack is used as intermediate storage for the indexes of the
variables to be used in capturing {\tt exit} values.

\subsubsection{Disabling}
The automaton may split into two automata related by a
\LOTOS\ {\tt disable} operator.
\begin{verbatim}
disable_expression ::
    MK_DIS normal_state disabling_state
\end{verbatim}

\subsubsection{Parallel Combination}
The automaton may split into two automata related by a
\LOTOS\ {\tt disable} operator.
There are three posibilities,
corresponding to full synchronization, interleaving,
and synchronization limited to some explicit gates
\begin{verbatim}
parallel_expression ::
      parallel_explicit
    | parallel_interleaving
    | parallel_full_synchronization

parallel_explicit ::
      [ gate_to_synchronize_on ]*
    MK_PE state state number_ gates

parallel implicit ::=
    MK_PI state state

parallel synchronization ::=
    MK_PS state state

gate_to_synchronize_on ::
    P_GTE gate_index
\end{verbatim}
The stack is used as intermediate storage for the values of the
gate(s) on which synchronization is required.

\subsubsection{Exclusive Choice Combination}
The automaton may offer a number of exclusive choices.
These are grouped in pairs to simplify the code.
Some states will just split into two choices.
By composition of states of this kind,
as many choices as needed may be ``simultaneously'' offered for
synchronization.
\begin{verbatim}
choice_expression ::
    MK_CH state state
\end{verbatim}

\subsubsection{BUT instantiation}
A BUT may eventually call another one.
In fact,
the old one does not exist any longer,
but is replaced by the new one.

The code is straightforward,
\begin{verbatim}
BUT_instantiation ::
      [ gate ]*
      [ value_expression ]*
    MK_PR BUT_# number_gates number_values

gate ::
    P_GTE gate_index
\end{verbatim}
The stack is used as an intermediate stage for actual gates and
values.

\subsubsection{Stop}
One of the most simple offers by a BUT is the no--offer:
\begin{verbatim}
stop_expression ::
    MK_ST
\end{verbatim}
There is no argument,
no next state,
no anything.

\subsubsection{Internal Event}
The next simplest transition is the {\tt internal} step:
\begin{verbatim}
internal_action ::
    MK_I next_state
\end{verbatim}
Notice that an internal action may happen or not,
depending on the context.
It is succeeds,
the automaton will move to the {\tt next state}.

\subsubsection{Offers}
This is perhaps the most complicated activity of BUTs.
A number of experiemnts are offered on a gate
for consideration by the environment.
If the pattern is accepted,
the BUT will move to the next state.

The complexite arises from the large (and variable) number of items to
consider in making such an offer
\begin{verbatim}
external_offer ::
      [ experiment ]*
    MK_AD  next_state  gate  number_exps  predicate

experiment ::
      single_offer
    | multiple_offer

single_offer ::
      value_expression
    MK_EXP "!" sort

multiple_offer ::
      [ EVALC default_value ]*
      P_VAR variable_index
      A_VAR variable_index variable_name
    MK_EXP  "?"  sort  number_defaults  [ iterate ]
\end{verbatim}
Notice that here we are considering \LOTOS\ extended with
{\tt default} and {\tt iterate} annotations.
These are optional, of course.

The {\tt default value} is a expression that evaluates to
a data value in internal notation.
It is written using some programming language.
{\tt Iterate} is a function that returns
a data value in internal notation.
It is called as many times as necessary until it returns a value that
permits a synchronization to take place.
The function to {\tt iterate} is written using some programming language.

For a multiple offer,
a variable must be identified that will hold the data value
that will be eventually used in the rendez-vous.
Some partner is expected to provide a single value
for synchronization to succeed.
This value is stored in the variable whose index is provided.

\verb/A_VAR/ is used only for debugging purposes.

\subsubsection{Exit}
It is quite similar to offer an {\tt exit}
since there may be concrete values offered as exit status,
or multiple values.
Single offers are handled as \verb/gate !value/,
while multiple offers are handled as \verb/gate ?fv: sort/,
where \verb/fv/ is just a funny variable
that is never used.
\begin{verbatim}
exit_expression ::
      [ exit_offer ]*
    MK_EX number_of_offers

exit_entry ::
      single offer
    | multiple_exit_offer

single_offer ::
      value_expression
    MK_EXP "!" sort

multiple_exit_offer ::
      P_VAR variable_index
    MK_EXP "?" sort 0
\end{verbatim}

\subsubsection{Delay Annotations}
{\tt Delays} are handled as waiting for a clock synchronization upon
certain clock value,
that is a determined position in time.
\begin{verbatim}
delay_annotation ::
    MK_DL next_entry delay
\end{verbatim}
where {\tt delay} is an expression that evaluates to an integer
and is the amount of time to wait for.
It is written for some programming language,
and will be evaluated later on.

\subsubsection{Wait Annotations}
It is quite similar to {\tt wait} for a predicate to be fulfilled
\begin{verbatim}
wait_annotation ::
    MK_WT next_entry function
\end{verbatim}
where {\tt function} is an expression that is repeatedly
evaluated till it yields a boolean {\tt true},
then the BUT moves to the {\tt next state}.
The function is written using any programming language,
and will be processed later on.
The boolean value used in this instruction is that of the target
programming language,
and it is interpreted according to that language.
There is no relation,
but the name,
with the Booleans that may be defined in the \LOTOS\ specification.

\section{Mapping LOTOS constructs to \LBM}
Most of the mapping should be evident from the previous description,
due to the close relationship between \LOTOS\ language,
and the \LBM.
Nevertheless,
to make this document complete,
some more information is needed about argument ordering.
This will be done by means of simple examples.

There is a difficulty in presenting these examples.
The semantic stages of \TOPO\ arbitrarily assign unique identifiers to
\LOTOS\ identifiers,
and arbitrarily allocates entities at BUT frames.
Let us use a couple of functions acting on identifiers
\begin{verbatim}
  uid: user_identifier -> unique_identifier
  idx: user_identifier -> index
\end{verbatim}

Furthermore,
{\tt processes} are mapped to BUTs,
and given a unique identification.
When no ambiguity arises,
we shall refer to this unique identifier as \verb/but_#/,
or for greater clarity as \verb/but_#(process_identifier)/.

Lastly, states are arbitrarily named.
An state name will be denoted by \verb/state_#/,
or \verb/next_#/.

\subsection{Hiding Expression}
\LOTOS\ expression:
\begin{verbatim}
  hide g1, g2, g3 in ...
\end{verbatim}

\LBM\ code:
\begin{verbatim}
    L_GTE idx(g1) uid(g1)
    A_GTE idx(g1) g1
    P_GTE idx(g1)
    L_GTE idx(g2) uid(g2)
    A_GTE idx(g2) g2
    P_GTE idx(g2)
    L_GTE idx(g3) uid(g3)
    A_GTE idx(g3) g3
    P_GTE idx(g3)
  MK_HD next_# 3
\end{verbatim}

\subsection{Local Definitions}
\LOTOS\ expression:
\begin{verbatim}
  let v1, v2: s1= 0, v3: s1= s(0) in ...
\end{verbatim}

\LBM\ code:
\begin{verbatim}
  B_LET
      EVAL uid(0) 0
      L_VAR idx(v1)
      A_VAR idx(v1) v1
      L_VAR idx(v2)
      A_VAR idx(v2) v2
    POP
      EVAL uid(0) 0
      EVAL s 1
      L_VAR idx(v3)
      A_VAR idx(v3) v3
    POP
  E_LET
\end{verbatim}

\subsection{Enabling Expression}
\LOTOS\ expression:
\begin{verbatim}
  ... >> accept x1, x2: s1, x3: s3 in ...
\end{verbatim}

\LBM\ code:
\begin{verbatim}
    P_VAR idx(x1)
    A_VAR idx(x1) x1
    P_VAR idx(x2)
    A_VAR idx(x2) x2
    P_VAR idx(x3)
    A_VAR idx(x3) x3
  MK_EN state_# state_# 3
\end{verbatim}

\subsection{Parallel Explicit Expression}
\LOTOS\ expression:
\begin{verbatim}
  ... |[ g1, g2, g3 ]| ...
\end{verbatim}

\LBM\ code:
\begin{verbatim}
      P_GTE idx(g1)
      P_GTE idx(g2)
      P_GTE idx(g3)
    MK_PE state_# state_# 3
\end{verbatim}

\subsection{Process Instantiation}
\LOTOS\ expression:
\begin{verbatim}
  proc_id [g1, g2] (v1, v2, v1+v2)
\end{verbatim}

\LBM\ code:
\begin{verbatim}
      P_GTE idx(g1)
      P_GTE idx(g2)
      P_VAL idx(v1)
      P_VAL idx(v2)
        P_VAL idx(v1)
        P_VAL idx(v2)
      EVAL uid(+) 2
    MK_PR but_#(proc_id)  2  3
\end{verbatim}

\subsection{Action Preffix Expression}
\LOTOS\ expression:
\begin{verbatim}
  g !v1 !v1+v2 ?x: s ; ...
\end{verbatim}

\LBM\ code:
\begin{verbatim}
      P_VAL idx(v1)
    MK_EXP ! sort(v1)
        P_VAL idx(v1)
        P_VAL idx(v2)
      EVAL uid(+) 2
    MK_EXP ! sort(+)
      P_VAR idx(x)
      A_VAR idx(x) x
    MK_EXP  ?  s  0
  MK_AD next_# uid(g) 3 -1
\end{verbatim}
The last $0$ in the last \verb/MK_EXP/
stands for the lack of {\tt default} values.

The $-1$ in \verb/MK_AD/ stands for the absence of any predicate.

\subsection{Action Preffix Expression with Predicate}
\LOTOS\ expression:
\begin{verbatim}
  g !v1 ?x1: s1 [ v1 + x1 = 0 ] ; ...
\end{verbatim}

\LBM\ code:
\begin{verbatim}
      P_VAL idx(v1)
    MK_EXP ! sort(v1)
      P_VAR idx(x1)
      A_VAR idx(x1) x1
    MK_EXP ? s1 0
  MK_AD next_# uid(g) 2 pred_#
  ...
  B_PRD pred_#
        P_VAL idx(v1)
        P_VAL idx(x1)
      EVAL uid(+) 2
      EVAL uid(0) 0
    EQUAL s1
  E_PRD
\end{verbatim}

\subsection{Exit Expression}
\LOTOS\ expression:
\begin{verbatim}
  exit (v1, v1+v2, any s)
\end{verbatim}

\LBM\ code:
\begin{verbatim}
      P_VAL idx(v1)
    MK_EXP ! sort(v1)
        P_VAL idx(v1)
        P_VAL idx(v2)
      EVAL uid(+) 2
    MK_EXP ! sort(+)
      P_VAR idx(?)
    MK_EXP  ?  s  0
    MK_EX 3
\end{verbatim}

\subsection{Complete Example}
To end this section,
let's present a complete example of a simple specification.
A few annotations for the case of {\tt C} language
are introduced to make the example more complete.

The example is presented in three steps.
First, the \LOTOS\ code is presented alone.
Second, the \LOTOS\ and \LBM\ are presented inerspersed,
to show relation between them.
Lastly,
the \LBM\ is presented alone.

Basically,
the text that folows is a verbatim copy of files,
but some editing has been done.
For the mixed presentation of \LOTOS\ and \LBM\ code,
some rearrangement of \LBM\ code was required.
Furthermore,
comments were removed
since proximity to \LOTOS\ text makes it redundant.
For the \LBM\ code,
some empty lines were inserted,
and the code was indented to help readers.

\newpage
\LOTOS\ specification:
\begin{verbatim}
specification sample : noexit
(*| lbc
# include <stdio.h>
|*)

  type Natural_numbers is
    sorts
      nat
    opns
      0: -> nat
      s: nat -> nat
    endtype

behaviour
  hide send, receive in
  ( producer [send] (0)
  |||
    consumer [receive]
  )
  |[ send, receive ]|
  buffer [send, receive]

where
  process producer [g] (n: nat) : noexit :=
    g !n ;
    producer [g] (s(n))
    endproc

  process consumer [g] : noexit :=
    g ?x: nat
    (*| C printf ("received\n"); |*) ;
    consumer [g]
    endproc

  process buffer [a, b] : noexit :=
    a ?d: nat ;
    (*| delay 1001 |*)
    b !d ;
    buffer [a, b]
    endproc
endspec
\end{verbatim}

\newpage
\LOTOS\ and \LBM\ code, mixed:
\begin{verbatim}
specification sample : noexit
                                B_LBC sample
(*| lbc
# include <stdio.h>
|*)
                                B_ANT
                                # include <stdio.h>
                                E_ANT

  type Natural_numbers is
    sorts
      nat
    opns
      0: -> nat
      s: nat -> nat
    endtype

behaviour
                                B_CRT 0 sample
                                B_ENT 0
                                I_GTE 2 0
                                I_VAR 0 0
  hide send, receive in
                                L_GTE 0 8
                                A_GTE 0 send
                                P_GTE 0
                                L_GTE 1 9
                                A_GTE 1 receive
                                P_GTE 1
                                MK_HD  1 2
                                E_ENT
    ( producer [send] (0)
                                B_ENT 3
                                P_GTE 0
                                EVAL 0 0
                                MK_PR 3 1 1
                                E_ENT
    |||
                                B_ENT 2
                                MK_PI 3 4
                                E_ENT
      consumer [receive]
                                B_ENT 4
                                P_GTE 1
                                MK_PR 2 1 0
                                E_ENT
    )
    |[ send, receive ]|
                                B_ENT 1
                                P_GTE 0
                                P_GTE 1
                                MK_PE 2 5 2
                                E_ENT
    buffer [send, receive]
                                B_ENT 5
                                P_GTE 0
                                P_GTE 1
                                MK_PR 1 2 0
                                E_ENT

                                E_CRT
where
  process producer [g] (n: nat) : noexit :=
                                B_CRT 3 producer
                                B_ENT 0
                                I_GTE 1 1
                                A_GTE 0 g
                                I_VAR 1 1
                                A_VAR 0 n
    g !n ;
                                P_VAL 0
                                MK_EXP ! 7
                                MK_AD 1 0 1 -1
                                E_ENT
    producer [g] (s(n))
                                B_ENT 1
                                P_GTE 0
                                P_VAL 0
                                EVAL s 1
                                MK_PR 3 1 1
                                E_ENT
    endproc
                                E_CRT

  process consumer [g] : noexit :=
                                B_CRT 2 consumer
                                B_ENT 0
                                I_GTE 1 1
                                A_GTE 0 g
                                I_VAR 1 0
    g ?x: nat
                                P_VAR 0
                                A_VAR 0 x
                                MK_EXP ? 7 0
                                MK_AD 1 0 1 -1
                                E_ENT
    (*| C printf ("received\n"); |*) ;
                                B_ENT 1
                                B_ANT
                                printf ("received\n"); 
                                E_ANT
    consumer [g]
                                P_GTE 0
                                MK_PR 2 1 0
                                E_ENT
    endproc
                                E_CRT

  process buffer [a, b] : noexit :=
                                B_CRT 1 buffer
                                B_ENT 0
                                I_GTE 2 2
                                A_GTE 0 a
                                A_GTE 1 b
                                I_VAR 1 0
    a ?d: nat ;
                                P_VAR 0
                                A_VAR 0 d
                                MK_EXP ? 7 0
                                MK_AD 1 0 1 -1
                                E_ENT
    (*| delay 1001 |*)
                                B_ENT 1
                                MK_DL  2 1001 
                                E_ENT
    b !d ;
                                B_ENT 2
                                P_VAL 0
                                MK_EXP ! 7
                                MK_AD 3 1 1 -1
                                E_ENT
    buffer [a, b]
                                B_ENT 3
                                P_GTE 0
                                P_GTE 1
                                MK_PR 1 2 0
                                E_ENT
    endproc
                                E_CRT
endspec
                                E_LBC
\end{verbatim}

\newpage
\LBM\ code:
\begin{verbatim}
B_LBC sample
  B_ANT
  # include <stdio.h>
  E_ANT

  B_CRT 3 producer
  B_ENT 0
    I_GTE 1 1
    A_GTE 0 g
    I_VAR 1 1
    A_VAR 0 n
    B_CMT [ action prefix expression ]
    E_CMT
        P_VAL 0
      MK_EXP ! 7
    MK_AD 1 0 1 -1
  E_ENT
  B_ENT 1
    B_CMT [ process instantiation ]
    E_CMT
    P_GTE 0
        P_VAL 0
      EVAL s 1
    MK_PR 3 1 1
  E_ENT
  E_CRT

  B_CRT 2 consumer
  B_ENT 0
    I_GTE 1 1
    A_GTE 0 g
    I_VAR 1 0
    B_CMT [ action prefix expression ]
    E_CMT
        P_VAR 0
        A_VAR 0 x
      MK_EXP ? 7 0
    MK_AD 1 0 1 -1
  E_ENT
  B_ENT 1
    B_ANT
    printf ("received\n"); 
    E_ANT
    B_CMT [ process instantiation ]
    E_CMT
      P_GTE 0
    MK_PR 2 1 0
  E_ENT
  E_CRT

  B_CRT 1 buffer
  B_ENT 0
    I_GTE 2 2
    A_GTE 0 a
    A_GTE 1 b
    I_VAR 1 0
    B_CMT [ action prefix expression ]
    E_CMT
        P_VAR 0
        A_VAR 0 d
      MK_EXP ? 7 0
    MK_AD 1 0 1 -1
  E_ENT
  B_ENT 1
    B_CMT [ action prefix expression ]
    E_CMT
    MK_DL  2 1001 
  E_ENT
  B_ENT 2
        P_VAL 0
      MK_EXP ! 7
    MK_AD 3 1 1 -1
  E_ENT
  B_ENT 3
    B_CMT [ process instantiation ]
    E_CMT
      P_GTE 0
      P_GTE 1
    MK_PR 1 2 0
  E_ENT
  E_CRT

  B_CRT 0 sample
  B_ENT 0
    I_GTE 2 0
    I_VAR 0 0
    B_CMT [ hiding expression ]
    E_CMT
      L_GTE 0 8
      A_GTE 0 send
      P_GTE 0
      L_GTE 1 9
      A_GTE 1 receive
      P_GTE 1
    MK_HD  1 2
  E_ENT
  B_ENT 1
    B_CMT [ parallel expression ]
    E_CMT
      P_GTE 0
      P_GTE 1
    MK_PE 2 5 2
  E_ENT
  B_ENT 2
    B_CMT [ parallel expression ]
    E_CMT
    MK_PI 3 4
  E_ENT
  B_ENT 3
    B_CMT [ process instantiation ]
    E_CMT
        P_GTE 0
      EVAL 0 0
    MK_PR 3 1 1
  E_ENT
  B_ENT 4
    B_CMT [ process instantiation ]
    E_CMT
      P_GTE 1
    MK_PR 2 1 0
  E_ENT
  B_ENT 5
    B_CMT [ process instantiation ]
    E_CMT
      P_GTE 0
      P_GTE 1
    MK_PR 1 2 0
  E_ENT
  E_CRT

  B_CMT empty predicates list
  E_CMT

E_LBC
\end{verbatim}

\section{Implementation}
There are very many ways to get an implementation of the \LBM\ as described
above.
The language is intended not to take any further implication on the
implementation that those stated above as {\em The Abstract Model}.

Here we shall briefly describe the current implementation in \TOPO,
but it must not be regarded as an specification of the \LBM\ at all.

Currently,
\TOPO\ generates {\tt C} code to implement the \LBM.
This approach has a number of advantages:
\begin{itemize}
\item
  Portatibility of C code.
\item
  Adequacy of C to be used as target for automatic code generation.
\item
  Efficiency of current C compilers.
\end{itemize}

In general it is much easier to generate code for a more or less high-end
language as C,
rather than for a low-end language as assembler,
and then rely on others' work to produce an executable program.
Within this philosophy,
C is an excellent language.

On the other hand,
C is a single-task language.
Although there are means to create and manage several tasks,
it greatly relays on the O.S. facilities to create,
communicate, and manage several processes.
For these reasons,
the current implementation is a single UNIX process.

Nevertheless,
it is internally a number of {\em processes}
under control of a local scheduler.
To go further with simmilarities to conventional O.S. concepts,
we shall distinguish between program and data segments,
where program segments are pieces of reentrant code
that may be shared by different instantiations.

The main program holds a {\em process table} where program and data
segment pairs define active instantiations.
Furthermore,
it holds information on synchronization requirements from each active
BUT,
classifying these ones into a number of queues:
ready to run, waiting for \ldots.
As synchronization conditions are met,
the successful BUTs are scheduled as ready,
and the failing ones are removed.

Details are rather complicated since in \LOTOS\ there are both
interleaving and exclusive (choice) behaviours,
that imply different actions on BUTs upon synchronization failure.
These details are not further developed in this document.

Organizationally,
the code is a collection of coroutines emulated in {\tt C}.
Pieces of code for the Kernel and the BUTs give control to each other
alternating their roles.
The status of each BUT instantiation is hold in its internal
variables.
BUT code is purely reentrant,
and the data segment is passed along with its call.

The generated {\tt C} code provides 3 public functions for the
automata to run.
There is a function to initialize the automaton, {\tt lbcinit()}.
Then there are two alternatives,
either to give control to the automaton for one step, {\tt step()},
or give control to the built-in scheduler, {\tt sch()}.
\begin{itemize}
\item
  \verb/void lbcinit (argc, argv) int argc; o_node* argv;/	\\
  It is intended to initialize the system.
  External arguments may be provided via a vector of arguments.
  The first parameter to {\tt lbcinit}
  is the number of arguments,
  while the second argument is a vector of so many arguments.
\item
  \verb/int step ()/						\\
  The automaton is instructed to advance one step.
  It returns an status code
  \begin{itemize}
  \item[$0$]
    The automaton terminates,
    executing {\tt stop}.
  \item[$1$]
    The automaton terminates with some error condition.
  \item[$2$]
    One step has been successfully performed.
  \item[$3$]
    All potential synchronizations are waiting for some {\tt delay}
    condition.
  \end{itemize}
\item
  \verb/int sch ()/						\\
  The built-in scheduler gets control.
  It will run the automaton as much as possible,
  and return an exit status code:
  \begin{itemize}
  \item[$0$]
    The automaton terminates,
    executing {\tt stop}.
  \item[$1$]
    The automaton terminates with some error condition.
  \end{itemize}
\end{itemize}

There are a large number of cases for synchronization.
This fact implies a large Kernel,
and inefficient code,
unless some heuristic is used to take drastic decissions.
Currently, \TOPO\ favours simple \LOTOS\ constructs
by optimizing the code for them.
Slight changes in the original \LOTOS\ specification
may imply big differences in execution resources.
\TOPO\ goes for the whole language,
but focusses on ``programming oriented'' specifications.

\section{Conclusions}
\LBM, an abstract machine for \LOTOS,
has been presented.
It is designed as an intermediate stage after the semantics analysis
of users' specification,
but before deriving code for some systems programming language.

All the syntactic richness of \LOTOS\ has been removed.
Therefore, \LBM\ is not intended for humans.
Deriving code for a programming language
must be an strightforward activity from \LBM\ code.
Still, a number of implementation decisions are open.
For instance, 
run--time data structures,
and mapping to O.S. processes are open options.
Very many implementations may be derived.

Currently there exists only one such code derivator,
{\tt m2c},
a tool to derive {\tt C} code.
{\tt M2c} is an integral part of \TOPO.
It is briefly sketched to demonstrate some of the open opportunities.

\LBM\ has been used in \TOPO\ for over two years.
During this period, it has suffered several changes.
In fact,
it is still subject to changes looking for a clear distinction of
roles between generating \LBM\ code, 
and deriving {\tt C} code from it.
Although designed to be independent of the target language,
experience in deriving code for any other language
(e.g. Ada)
will surely require some adjustment.

This specification of \LBM\ is in the public domain.

\end{document}

% Local Variables:
% mode: indented-text
% comment-column: 0
% comment-start: "% "
% comment-end: ""
% comment-start-skip: "% *"
