Modularity is advocated as the ultimate solution for the design of large
systems, and this holds in particular for embedded systems, and their
software and architecture. Modularity allows the designer to scale down
design problems, and facilitate reuse of predefined modules.
Task 4.1 of the project is devoted to address this issue for code
generation.
The mathematical translation of the concept of modularity is often that
of compositionality. Paying attention to the composition of
specifications is central to any system model involving concurrency or
parallelism. More recently, significant effort has been devoted toward
introducing compositionality in verification with aiming at deriving
proofs of large programs from partial proofs involving (abstractions of)
components. Compilation and code generation has been given less
attention from the same point of view, however. This is unfortunate, as
it is critical for the designer to scale down the design of large
systems by
storing modules like black-box ``procedures'' or
``processes'' with minimal interface description, and
generating code
only using these interface descriptions, while still guaranteing that
final encapsulation of actual code within these black-boxes together
with their composition, will maintain correctness of the design w.r.t.
specification.
This paper is devoted the issues of compositionality aiming at modular
code generation, for dataflow synchronous languages. As dataflow
synchronous is rather a paradigm more than a few concrete languages or
visual formalisms, it was desirable to abstract from such and such
particular language. Thus we have chosen to work with a formalism
proposed by Amir Pnueli, that of Symbolic Transition Systems (STS),
which is at the same time very lightweight, and fully general to capture
the essence of synchronous paradigm.
Achieved Results:
First, we study composition of specifications, a very
trivial topic indeed.
Most of our effort is then devoted to issues of
compositionality that are critical to code generation. As careless
storing of object code for further reuse in systems design fails to
work, we first concentrate on what are the additional features needed to
abstract programs for the purpose of code generation: we show that a
central notion is that of scheduling specification as resulting from a
causality analysis of the given program. We pay strong
attention to this notion, a whole appendix is devoted to its
mathematical analysis, using a technique not unlike the one for the
causality analysis of Esterel. Related issues of compositionality are
investigated.
Then we show that
there is some appropriate level of ``intermediate code'', which at the
same time allows us to scale down code generation for large systems, and
still maintains correctness at the system integration phase.
Finally we
discuss the side issue of distributed implementation using an
asynchronous medium of communication.
Corresponding algorithms are currently under development in the
framework of the DC+ common format for synchronous languages.
Publications:
A. Benveniste, P. Le Guernic, and P. Aubry
Compositionality in dataflow synchronous languages: specification and code
generation Malente Workshop on Compositionality, W.P. de Roever, A.
Pnueli Eds., September 1997