The Esterel synchronous programming language: design, semantics, implementation

Abstract

We present the Esterel programming language which is especially designed to program reactive systems, that is systems which maintain a permanent interaction with their environment: real-time process controllers, communication protocols, man-machine interface drivers, etc. Esterel is a deterministic concurrent programming language. It differs from classical asynchronous languages by its synchrony hypothesis: the outputs of a system are conceptually synchronous with its inputs. The synchrony hypothesis permits a high-level modular programming style simpler and more rigorous than its asynchronous counterpart. We present the imperative primitives of Eesterel and the temporal manipulations they permit. We give a small programming example. We present two mathematical semantics of Eesterel, which are given by conditional rewrite rules and related by a correctness theorem. The behavioral semantics defines the behavior of programs in an uneffective way as the solution of fixpoint equations. The effective execution semantics computes actions to be performed by a conceptually infinitely fast execution machine. To relate the two semantics, we solve the causality problems that are inherent in synchronous formalisms. We show how the Eesterel v2 and Eesterel v3 compilers efficiently translate concurrent Eesterel programs into efficient equivalent sequential automata that can be implemented in conventional sequential languages. We discuss the quality of this object code and the practical adequacy of the synchrony hypothesis.

Résumé

Nous présentons le langage Eesterel, qui est spécifiquement adapté à la programmation des systèmes réatifs, c'est à dire des systèmes dont le rôle est de maintenir une interaction constante avec leur environment: contrôleurs de processus en temps-réel, protocoles de communications, interfaces homme-machine etc. Eesterel est un langage de programmation parallèle déterministe, qui diffère des langages classiques par son hypothèses de synchronisme: les sorties du système réactif sont supposées conceptuellement synchrones avec ses entrées. Cette hypothèse permet une programmation plus modulaire et plus simple que les techniques asynchrones classiques. Nous présentons les primitives impératives du langage et les manipulations temporelles qu'elles permettent. Nous donnons un exemple de programme typique. Nous présentons deux sémantiques mathématiques du langage: une sémantique comportementale qui définit de fao̧n non effective le comportement d'un programme, et une sémantique d'exécution qui permet de calculer effectivement ces comportements et de résoudre les problèmes de causalité inhérents aux systèmes synchrones. Ces deux sémantiques sont données par des règles de réécriture conditionnelles. Elles sont reliées par un théorème de correction. Nous montrons comment les compilateurs ESTEREL v2 et Eesterel v3 traduisent les programmes parallèles Eesterel en automates séquentiels équivalents et très efficaces. Nous discutons la qualité du code produit et la validité pratique de l'hypothèse de synchronisme.