Project description

This proposal describes a collaborative project between University of Southern California, INRIA Sophia Antipolis, and the I3S Laboratory (CNRS URA 1376). The goal of our project is to specify the semantics of parallel languages in order to formally define program transformations, namely parallelizations. Among a large collection of potential languages, two languages have been chosen for their particularities:

• Sisal [41], a functional parallel language with code generation for multi-processors architectures;
• Eiffel// [24], an imperative concurrent object-oriented programming language, a parallel extension of Eiffel [72].

The inspiration for the collaboration comes from three sources. The Sisal language is extensively used in the team of Jean-Luc Gaudiot, at USC. The Eiffel// language was designed and implemented by Denis Caromel. Finally, the Centaur system [17], designed and developed in the CROAP team at INRIA Sophia Antipolis, will be used to formulate the formal specifications. It is a generic programming environment: from formal specifications expressing syntax and semantics of a given language, one can generate a programming environment for this language, including a structure editor, type-checker, interpreter, translators, ...

In fact, this collaboration has already started on two separate axes: using the Centaur system, a formal definition of the Eiffel language has been expressed [8]; also using the Centaur system, the development of the same kind of semantics for Sisal has begun in summer 93, during a 4 week-visit of Isabelle Attali and Denis Caromel at USC.

The research plan for this proposal is scheduled on 3 years and includes the following objectives:

1. complete the formal definition of Sisal using Centaur
2. extend the formal definition of Eiffel to get the formal definition of Eiffel//;
3. define intermediate formats for the two languages, and investigate the possibility of common intermediate structures for both of them;
4. based on the intermediate structures, define and prove program transformations for Eiffel// and Sisal. The intended transformations are parallelizations, and transformations for specific parallel architecture targets.

All the transformations being formalized within the Centaur system, it will be possible to produce an integreted interactive environment for the parallelization of both Eiffel// and Sisal programs.

Topics: software systems, semantic-based program manipulation, proved software systems, parallel programming.

In the following, we give an overview of the Centaur system, the semantics of Eiffel we already have expressed in Natural Semantics, and the two languages we study, Eiffel// and Sisal. The next section describes the proposed work in more detail, the techniques we will use and the resulting tools we will produce.