SCADE is an environment for developing critical embedded software that is used for more than twenty years in various application domains like avionics, nuclear plants, transportation, automotive. It comes with a language and a code generator which complies with the highest safety standards like DO-178C, IEC 61508, EN 50128, IEC 60880 and ISO 26262. The language has been founded on the pioneering work by Caspi and Halbwachs on Lustre. In 2008, a major revision of the language and compiler, named ‘Scade 6’, was released. One of its novelty was a smooth integration of the traditional dataflow style of Lustre with control-structures inspired from those of Esterel and SyncCharts, with static/dynamic semantics and a compilation inspired from Lucid Synchrone. In particular, it relies on four dedicated type systems - typing, clock calculus, causality analysis, initialization analysis - and a compilation through source-to-source transformations into a minimal clocked data-flow language, based on a Kahn semantics, that is translated to imperative code. One ongoing work is the generation of code for multi-core architectures. Because of the intrinsic deterministic parallelism of Scade, we propose a solution that relies on annotations that specify what must be executed concurrently but do not change the semantics. The paper is a survey of past to ongoing work on Scade 6 lanzuaze definition and implementation.
SCADE is an environment for developing critical embedded software that is used for more than twenty years in various application domains like avionics, nuclear plants, transportation, automotive. It comes with a language and a code generator which complies with the highest safety standards like DO-178C, IEC 61508, EN 50128, IEC 60880 and ISO 26262.The language has been founded on the pioneering work by Caspi and Halbwachs on Lustre. In 2008, a major revision of the language and compiler, named 'Scade 6', was released. One of its novelty was a smooth integration of the traditional data flow style of Lustre with control-structures inspired from those of Esterel and SyncCharts, with static/dynamic semantics and a compilation inspired from Lucid Synchrone. In particular, it relies on four dedicated type systems typing, clock calculus, causality analysis, initialization analysis and a compilation through source-to-source transformations into a minimal clocked data-flow language, based on a Kahn semantics, that is translated to imperative code.One ongoing work is the generation of code for multi-core architectures. Because of the intrinsic deterministic parallelism of Scade, we propose a solution that relies on annotations that specify what must be executed concurrently but do not change the semantics.The paper is a survey of past to ongoing work on Scade 6 language definition and implementation.
Hybrid systems modelers like Simulink come with a rich collection of discrete-time and continuous-time blocks. Most blocks are not defined in terms of more elementary ones—and some cannot be—but are instead written in imperative code and explained informally in a reference manual. This raises the question of defining a minimal set of orthogonal programming constructs such that most blocks can be programmed directly and thereby given a specification that is mathematically precise, and whose compiled version performs comparably to handwritten code. In this paper, we show that a fairly large set of blocks of a standard library like the one provided by Simulink can be programmed in a precise, purely functional language using stream equations, hierarchical automata, Ordinary Differential Equations (ODEs), and deterministic synchronous parallel composition. Some blocks cannot be expressed in our setting as they mix discrete-time and continuous-time signals in unprincipled ways that are statically forbidden by the type checker. The experiment is conducted in Zélus, a synchronous language that conservatively extends L ustre with ODEs to program systems that mix discrete-time and continuous-time signals.
Modeling languages for hybrid systems are cornerstones of embedded systems development in which software interacts with a physical environment. Sequential code generation from such languages is important for simulation efficiency and for producing code for embedded targets. Despite being routinely used in industrial compilers, code generation is rarely, if ever, described in full detail, much less formalized. Yet formalization is an essential step in building trustable compilers for critical embedded software development. This paper presents a novel approach for generating code from a hybrid systems modeling language. By building on top of an existing synchronous language and compiler, it reuses almost all the existing infrastructure with only a few modifications. Starting from an existing synchronous data-flow language conservatively extended with Ordinary Differential Equations (ODEs), this paper details the sequence of source-to-source transformations that ultimately yield sequential code. A generic intermediate language is introduced to represent transition functions. The versatility of this approach is exhibited by treating two classical simulation targets: code that complies with the FMI standard and code directly linked with an off-the-shelf numerical solver (Sundials CVODE). The presented material has been implemented in the Zélus compiler and the industrial Scade Suite KCG code generator of Scade 6.
Concurrent and reactive systems often exhibit multiple time scales. This situation occurs, for instance, in the discrete simulation of a sensor network where the time scale at which agents communicate is very different from the time scale used to model the internals of an agent.The paper presents reactive domains to simplify the programming of such systems. Reactive domains allow for several time scales to be defined and they enable time refinement, that is, the replacement of a system with a more detailed version, without changing its observed behavior.Our work applies to the ReactiveML language, which extends an ML language with synchronous programming constructs à la Esterel. We present an operational semantics for the extended language, a type system that ensures the soundness of programs, and a sequential implementation. We discuss how reactive domains can be used in a parallel implementation.
Ten years ago we introduced ReactiveML, an extension of a strict ML language with synchronous parallelism à la Esterel to program reactive applications. Our purpose was to demonstrate that synchronous language principles, originally invented and used for critical real-time control software, would integrate well with ML and prove useful in a wider context: reactive applications with complex data structures and sequential algorithms, organized as a dynamically evolving set of tightly synchronized parallel tasks. While all ReactiveML programs presented at PPDP'05 still compile, the language has evolved continuously to incorporate novel programming constructs, compilation techniques and dedicated static analyses. ReactiveML has been used for applications that we never anticipated: the simulation of large-scale ad-hoc and sensor networks, an interactive debugger, and interactive mixed music. These applications were only possible due to the efficient compilation of ReactiveML into sequential code, which we present here for the first time. We also present a parallel implementation that uses work-stealing techniques through shared memory. Finally, we give a retrospective view on ReactiveML over the past ten years.
Cooperative scheduling enables efficient sequential implementations of concurrency. It is widely used to provide lightweight threads facilities as libraries or programming constructs in many programming languages. However, it is up to programmers to actually cooperate to ensure the reactivity of their programs.We present a static analysis that checks the reactivity of programs by abstracting them into so-called behaviors using a type-and-effect system. Our objective is to find a good compromise between the complexity of the analysis and its precision for typical reactive programs. The simplicity of the analysis is mandatory for the programmer to be able to understand error messages and how to fix reactivity problems.Our work is applied and implemented in the functional synchronous language ReactiveML. It handles recursion, higher-order processes and first-class signals. We prove the soundness of our analysis with respect to the big-step semantics of the language: a well-typed program with reactive effects is reactive. The analysis is easy to implement and generic enough to be applicable to other models of concurrency such as coroutines.
Cooperative scheduling enables efficient sequential implementations of concurrency. It is widely used to provide lightweight threads facilities as libraries or programming constructs in many programming languages. However, it is up to programmers to actually cooperate to ensure the reactivity of their programs. We present a static analysis that checks the reactivity of programs by abstracting them into so-called behaviors using a type-and-effect system. Our objective is to find a good compromise between the complexity of the analysis and its precision for typical reactive programs. The simplicity of the analysis is mandatory for the programmer to be able to understand error messages and how to fix reactivity problems. Our work is applied and implemented in the functional synchronous language ReactiveML. It handles recursion, higher-order processes and first-class signals. We prove the soundness of our analysis with respect to the big-step semantics of the language: a well-typed program with reactive effects is reactive. The analysis is easy to implement and generic enough to be applicable to other models of concurrency such as coroutines. This research report is the extended version of the article published at the 21st International Static Analysis Symposium.
ReactiveML est un langage dedie a la programmation de systemes combinant des parties algorithmiques et reactives. Il s'agit d'une extension de ML avec des constructions pour la concurrence inspirees des langages synchrones. Celles-ci permettent d'obtenir une tres grande expressivite, mais leur implantation efficace represente un defi. Dans cet article, nous presentons l'implantation de ReactiveML, de la compilation a l'implantation du moteur d'execution en OCaml. Nous decrivons egalement une implantation parallele en memoire partagee du moteur d'execution utilisant le vol de tâches. L'approche choisie permet d'obtenir une execution efficace meme en presence de structures de controle complexes. Elle s'etend simplement au cas parallele avec des resultats experimentaux prometteurs.
Nous nous interessons dans ce manuscrit au langage ReactiveML, qui est une extension de ML avec des constructions inspirees des langages synchrones. L'idee de ces langages est de diviser l'execution d'un programme en une suite d'instants logiques discrets. Cela permet de proposer un modele de concurrence deterministe que l'on peut compiler vers du code sequentiel imperatif. La principale application de ReactiveML est la simulation discrete, par exemple de reseaux de capteurs. Nous cherchons ici a programmer des simulations a grande echelle, ce qui pose deux questions : sait-on les programmer de facon simple et modulaire ? sait-on ensuite executer ces programmes efficacement ? Nous repondons a la premiere question en proposant une extension du modele synchrone appelee domaines reactifs. Elle permet de creer des instants locaux invisibles de l'exterieur. Cela rend possible le raffinement temporel, c'est-a-dire le remplacement d'une approximation d'un systeme par une version plus detaillee sans changer son comportement externe. Nous developpons dans ce manuscrit la semantique formelle de cette construction ainsi que plusieurs analyses statiques, sous forme de systemes de types-et-effets, garantissant la surete des programmes dans le langage etendu. Enfin, nous montrons egalement plusieurs implementations paralleles du langage pour tenter de repondre a la question du passage a l'echelle des simulations. Nous decrivons tout d'abord une implementation avec threads communiquant par memoire partagee et basee sur le vol de tâches, puis une seconde implementation utilisant des processus lourds communiquant par envoi de messages.
The generation of efficient sequential code for synchronous data-flow languages raises two intertwined issues: control and memory optimization. While the former has been extensively studied, for instance in the compilation of Lustre and Signal, the latter has only been addressed in a restricted manner. Yet, memory optimization becomes a pressing issue when arrays are added to such languages. This article presents a two-level solution to the memory optimization problem. It combines a compile-time optimization algorithm, reminiscent of register allocation, paired with language annotations on the source given by the designer. Annotations express in-place modifications and control where allocation is performed. Moreover, they allow external functions performing in-place modifications to be safely imported. Soundness of annotations is guaranteed by a semilinear type system and additional scheduling constraints. A key feature is that annotations for well-typed programs do not change the semantics of the language: removing them may lead to less efficient code but will not alter the semantics. The method has been implemented in a new compiler for a LUSTRE-like synchronous language extended with hierarchical automata and arrays. Experiments show that the proposed approach removes most of the unnecessary array copies, resulting in faster code that uses less memory.