The Sisal 1.2 compiler, OSC, has proved remarkably successful through exploitation of a variety of sophisticated optimizations. A precise definition of the transformations rules used in the compiler will give confidence in their correctness and provide us with the ability to reason about and extend the optimizations used, and successfully incorporate them into any Sisal 2.0 compiler development.
An important development of Sisal is to provide implementations for recent multiprocessor architectures, such as the TMC CM-5 which, to some extent, offers a choice between SPMD and MIMD programming models; in the case of a very high-level language such as Sisal, it is up to the compiler to make that choice. To increase our understanding of those aspects of Sisal most amenable to translation to data parallelism, we intend to first build a suite of formal translations. In addition, we would need to develop at least an intuition for, and perhaps a more formal model of, those situations where data parallelism is best used in order to measure and evaluate the performances of the transformations. Also, we will analyze individual Sisal constructs in a given program, and determine the best method of translation, to data parallelism, message passing or barrier style MIMD parallelism, or a combination of both. These are problems applicable not only to Sisal translation but also providing a basis for generalization to FORTRAN 90 and other high-level languages [90].
Program transformations achieved in Eiffel// consist of the following:
The wait-by-necessity automatically triggers a wait when an object attempts to use the result of an asynchronous call which has not been returned yet. This feature, by automatically adding some synchronization, tends to maintain the same behavior when doing the parallelization. However, not all the objects can be transformed into an asynchronous process with no effect on the system observable behavior. Therefore, one difficulty lies in selecting the objects which can be mutated without changing the semantics. The other challenge is to find the objects that will bring a significant parallelism into the application.
We aim at specifying all intermediate forms and semantics manipulations using Centaur and the Typol formalism. This includes the translations from Sisal, Eiffel, Eiffel// into the intermediate formats, the transformations themselves, and the proofs (possibly interfaced with other tools if needed).
We believe that the formalization tools provided by Centaur are well-suited to these tasks. Natural Semantics [64] is not only used for language descriptions but also to define translators (ML-CAM [14]). Inference rules have been used to give the dynamic semantics of parallel languages [13][85][74], for describing compiler optimizations [57][102], and for a complete semantic description of the language Standard ML [77]. Moreover, this style of definition has been used to formalize the semantics of dependency flow graphs [31][83]. This approach is adaptable to the context of the graphical intermediate forms IF1 and IF2. Based on these examples and our own preliminary work, we are confident that logics defined using inference rules, especially as embodied in Centaur, are powerful enough to describe the semantics of Eiffel//, Sisal, the intermediate languages, and the transformations.