The Lucid-Synchrone Bibliography

[DGP08] Gwenael Delaval, Alain Girault, and Marc Pouzet. A Type System for the Automatic Distribution of Higher-order Synchronous Dataflow Programs. In ACM International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES), Tucson, Arizona, June 2008. [ bib ]
We address the design of distributed systems with synchronous dataflow programming languages. As modular design entails handling both architecture and functional modularity, our first contribution is to extend an existing synchronous dataflow programming language with primitives allowing the description of a distributed architecture and the localization of some expressions onto some processors. We also present a distributed semantics to formalize the distributed execution of synchronous programs. Our second contribution is to provide a type system, in order to infer the localization of non-annotated values by means of type inference and to ensure, at compilation time, the consistency of the distribution. Our third contribution is to provide a type-directed projection operation to obtain automatically, from a centralized typed program, the local program to be executed by each computing resource. The type system as well as the automatic distribution mechanism has been fully implemented in the compiler of an existing synchronous data-flow programming language.

[BCHP08] Darek Biernacki, Jean-Louis Colaco, Grégoire Hamon, and Marc Pouzet. Clock-directed Modular Code Generation of Synchronous Data-flow Languages. In ACM International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES), Tucson, Arizona, June 2008. [ bib ]
The compilation of synchronous block diagrams into sequential imperative code has been addressed in the early eighties and can now be considered as folklore. However, modular code generation, though largely used in existing compilers and particularly in industrial ones, has never been precisely described or entirely formalized. Such a formalization is now fundamental in the long-term goal to develop a mathematically certified compiler for a synchronous language as well as in simplifying existing implementations.

This article presents in full detail the modular compilation of synchronous block diagrams into sequential code. We consider a first-order functional language reminiscent of Lustre, which it extends with a general n-ary merge operator, a reset construct, and a richer notion of clocks. The clocks are used to express activation of computations in the program and are specifically taken into account during the compilation process to produce efficient imperative code. We introduce a generic machine-based intermediate language to represent transition functions, and we present a concise clock-directed translation from the source to this intermediate language. We address the target code generation phase by describing a translation from the intermediate language to Java and C.

[CCP08] Paul Caspi, Jean-Louis Colaço, and Marc Pouzet. Objects in Block-Diagram Languages, January 2008. Unpublished. [ bib ]
[LGP07] Sébastien Labbé, Jean-Pierre Gallois, and Marc Pouzet. Slicing communicating automata specifications for efficient model reduction. In 18th Australian Conference on Software Engineering (ASWEC), 2007. [ bib ]
[CHP07] Paul Caspi, Grégoire Hamon, and Marc Pouzet. Real-Time Systems: Models and verification - Theory and tools, chapter Synchronous Functional Programming with Lucid Synchrone. ISTE, 2007. English version of [CHP06a]. Published during year 2007. [ bib ]
[BCP07] Darek Biernacki, Jean-Louis Colaco, and Marc Pouzet. Modular Compilation from Synchronous Block-diagrams. In Workshop on Automatic Program Generation for Embedded Systems (APGES), Salzburg, Austria, october 2007. Embedded System Week. [ bib ]
[CHP06b] Jean-Louis Colaço, Grégoire Hamon, and Marc Pouzet. Mixing Signals and Modes in Synchronous Data-flow Systems. In ACM International Conference on Embedded Software (EMSOFT'06), Seoul, South Korea, October 2006. [ bib | .pdf ]
Synchronous data-flow languages such as SCADE/Lustre manage infinite sequences or streams as primitive values making them naturally adapted to the description of data-dominated systems. Their conservative extension with means to define control-structures or modes have been a long-term research topic and several solutions have emerged.

In this paper, we pursue this effort and generalize existing solutions by providing two constructs: a general form of state machines called parameterized state machines, and valued signals, as can be found in Esterel. Parameterized state machines greatly reduce the reliance on error-prone mechanisms such as shared memory in automaton-based programming. Signals provide a new way of programming with multi-rate data in synchronous data-flow languages. Together, they allow for a much more direct and natural programming of systems that combine data-flow and state-machines.

The proposed extension is fully implemented in the new Lucid Synchrone compiler.

[Pou06] Marc Pouzet. Lucid Synchrone, version 3. Tutorial and reference manual. Université Paris-Sud, LRI, April 2006. Distribution available at: www.lri.fr/~pouzet/lucid-synchrone. [ bib ]
[GNP06] Alain Girault, Xavier Nicollin, and Marc Pouzet. Automatic Rate Desynchronization of Embedded Reactive Programs. ACM Transactions on Embedded Computing Systems (TECS), 5(3), 2006. [ bib ]
[CDE+06] Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, and Marc Pouzet. N-Synchronous Kahn Networks: a Relaxed Model of Synchrony for Real-Time Systems. In ACM International Conference on Principles of Programming Languages (POPL'06), Charleston, South Carolina, USA, January 2006. [ bib | .pdf ]
The design of high-performance stream-processing systems is a fast growing domain, driven by markets such like high-end TV, gaming, 3D animation and medical imaging. It is also a surprisingly demanding task, with respect to the algorithmic and conceptual simplicity of streaming applications. It needs the close cooperation between numerical analysts, parallel programming experts, real-time control experts and computer architects, and incurs a very high level of quality insurance and optimization.

In search for improved productivity, we propose a programming model and language dedicated to high-performance stream processing. This language builds on the synchronous programming model and on domain knowledge - the periodic evolution of streams - to allow correct-by-construction properties to be proven by the compiler. These properties include resource requirements and delays between input and output streams. Automating this task avoids tedious and error-prone engineering, due to the combinatorics of the composition of filters with multiple data rates and formats. Correctness of the implementation is also difficult to assess with traditional (asynchronous, simulation-based) approaches. This language is thus provided with a relaxed notion of synchronous composition, called n-synchrony: two processes are n-synchronous if they can communicate in the ordinary (0-)synchronous model with a FIFO buffer of size n.

Technically, we extend a core synchronous data-flow language with a notion of periodic clocks, and design a relaxed clock calculus (a type system for clocks) to allow non strictly synchronous processes to be composed or correlated. This relaxation is associated with two sub-typing rules in the clock calculus. Delay, buffer insertion and control code for these buffers are automatically inferred from the clock types through a systematic transformation into a standard synchronous program. We formally define the semantics of the language and prove the soundness and completeness of its clock calculus and synchronization transformation. Finally, the language is compared with existing formalisms.

[CHP06a] Paul Caspi, Grégoire Hamon, and Marc Pouzet. Systèmes Temps-réel : Techniques de Description et de Vérification - Théorie et Outils, volume 1, chapter Lucid Synchrone, un langage de programmation des systèmes réactifs, pages 217-260. Hermes, 2006. [ bib ]
Ce chapitre présente Lucid Synchrone, un langage dédié à la programmation de systèmes réactifs. Il est fondé sur le modèle synchrone de Lustre qu'il étend avec des caractéristiques présentes dans les langages fonctionnels tels que l'ordre supérieur ou l'inférence des types. Il offre un mécanisme de synthèse automatique des horloges et permet de décrire, dans un cadre unifié, une programmation flot de données et une programmation par automates.

Ce chapitre est une présentation du langage, destinée à la fois au programmeur cherchant à se familiariser avec celui-ci, mais aussi au chercheur s'intéressant aux systèmes réactifs et aux techniques qui peuvent être appliquées au niveau d'un langage, pour faciliter les activités de spécification, de programmation et de vérification.

[CDE+05] Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, and Marc Pouzet. Synchroning Periodic Clocks. In ACM International Conference on Embedded Software (EMSOFT'05), Jersey city, New Jersey, USA, September 2005. [ bib | .pdf.gz ]
[CPP05] Jean-Louis Colaço, Bruno Pagano, and Marc Pouzet. A Conservative Extension of Synchronous Data-flow with State Machines. In ACM International Conference on Embedded Software (EMSOFT'05), Jersey city, New Jersey, USA, September 2005. [ bib | .pdf.gz ]
This paper presents an extension of a synchronous data-flow language such as Lustre with imperative features expressed in terms of powerful state machine à la SyncChart. This extension is fully conservative in the sense that all the programs from the basic language still make sense in the extended language and their semantics is preserved.

From a syntactical point of view this extension consists in hierarchical state machines that may carry at each hierarchy level a bunch of equations. This proposition is an alternative to the joint use of Simulink and Stateflow but improves it by allowing a fine grain mix of both styles.

The central idea of the paper is to base this extension on the use of clocks, translating imperative constructs into well clocked data-flow programs from the basic language. This clock directed approach is an easy way to define a semantics for the extension, it is light to implement in an existing compiler and experiments show that the generated code compete favorably with ad-hoc techniques. The proposed extension has been implemented in the ReLuC compiler of Scade/Lustre and in the Lucid Synchrone compiler.

[CP05] Jean-Louis Colaço and Marc Pouzet. Clocks as First Class Abstract Types. Submitted to the Journal of Functional Programming (JFP), 2005. [ bib ]
[CP04] Jean-Louis Colaço and Marc Pouzet. Type-based Initialization Analysis of a Synchronous Data-flow Language. International Journal on Software Tools for Technology Transfer (STTT), 6(3):245-255, August 2004. [ bib ]
[Ham04] Grégoire Hamon. Synchronous Data-flow Pattern Matching. In Synchronous Languages, Applications, and Programming. Electronic Notes in Theoretical Computer Science, 2004. [ bib | .ps.gz ]
[CGHP04] Jean-Louis Colaço, Alain Girault, Grégoire Hamon, and Marc Pouzet. Towards a Higher-order Synchronous Data-flow Language. In ACM Fourth International Conference on Embedded Software (EMSOFT'04), Pisa, Italy, september 2004. [ bib | .pdf ]
The paper introduces a higher-order synchronous data-flow language in which communication channels may themselves transport programs. This provides a mean to dynamically reconfigure data-flow processes. The language comes as a natural and strict extension of both Lustre and Lucid Synchrone. This extension is conservative, in the sense that a first-order restriction of the language can receive the same semantics. We illustrate the expressivity of the language with some examples, before giving the formal semantics of the underlying calculus. The language is equipped with a polymorphic type system allowing types to be automatically inferred and a clock calculus rejecting programs for which synchronous execution cannot be statically guaranteed. To our knowledge, this is the first higher-order synchronous data-flow language where stream functions are first class citizens.

[CP03] Jean-Louis Colaço and Marc Pouzet. Clocks as First Class Abstract Types. In Third International Conference on Embedded Software (EMSOFT'03), Philadelphia, Pennsylvania, USA, october 2003. [ bib | .ps.gz ]
Clocks in synchronous data-flow languages are the natural way to define several time scales in reactive systems. They play a fundamental role during the specification of the system and are largely used in the compilation process to generate efficient sequential code. Based on the formulation of clocks as dependent types, the paper presents a simpler clock calculus reminiscent to ML type systems with first order abstract types à la Laufer & Odersky. Not only this system provides clock inference, it shares efficient implementations of ML type systems and appears to be expressive enough for many real applications.

[CP02a] Paul Caspi and Marc Pouzet. Lucid Synchrone, a functional extension of Lustre. Submitted to publication, 2002. [ bib ]
[CP02b] Jean-Louis Colaço and Marc Pouzet. Type-based Initialization Analysis of a Synchronous Data-flow Language. In Synchronous Languages, Applications, and Programming, volume 65. Electronic Notes in Theoretical Computer Science, 2002. [ bib | .ps.gz ]
One of the appreciated features of the synchronous data-flow approach is that a program defines a perfectly deterministic behavior. But the use of the delay primitive leads to undefined values at the first cycle; thus a data-flow program is really deterministic only if it can be shown that such undefined values do not affect the behavior of the system.

This paper presents an initialization analysis that guarantees the deterministic behavior of programs. This property being undecidable in general, the paper proposes a safe approximation of the property, precise enough for most data-flow programs. This analysis is a one-bit analysis - expressions are either initialized or uninitialized - and is defined as an inference type system with sub-typing constraints. This analysis has been implemented in the Lucid Synchrone compiler and in a new Scade-Lustre prototype compiler. It gives very good results in practice.

[Ham02] Grégoire Hamon. Calcul d'horloge et Structures de Contrôle dans Lucid Synchrone, un langage de flots synchrones à la ML. PhD thesis, Université Pierre et Marie Curie, Paris, France, 14 novembre 2002. [ bib ]
[Cuo02] Pascal Cuoq. Ajout de synchronisme dans les langages fonctionnels typés. PhD thesis, Université Pierre et Marie Curie, Paris, France, october 2002. [ bib ]
[Pou02] Marc Pouzet. Lucid Synchrone: un langage synchrone d'ordre supérieur. Paris, France, 14 novembre 2002. Habilitation à diriger les recherches. [ bib | .ps.gz ]
[BH01] Sylvain Boulmé and Grégoire Hamon. Certifying Synchrony for Free. In International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), volume 2250, La Havana, Cuba, December 2001. Lecture Notes in Artificial Intelligence, Springer-Verlag. Short version of A clocked denotational semantics for Lucid-Synchrone in Coq, available as a Technical Report (LIP6), at www.lri.fr/~pouzet. [ bib | .ps.gz ]
We express reactive programs in Coq using data-flow synchronous operators. Following Lucid Synchrone approach, synchronous static constraints are here expressed using dependent types. Hence, our analysis of synchrony is here directly performed by Coq typechecker.

[Pou01] Marc Pouzet. Lucid Synchrone, version 2. Tutorial and reference manual. Université Pierre et Marie Curie, LIP6, Mai 2001. Distribution available at: www.lri.fr/~pouzet/lucid-synchrone. [ bib ]
[CP01] Pascal Cuoq and Marc Pouzet. Modular Causality in a Synchronous Stream Language. In European Symposium on Programming (ESOP'01), Genova, Italy, April 2001. [ bib | .ps.gz ]
This article presents a causality analysis for a synchronous stream language with higher-order functions. This analysis takes the shape of a type system with rows. Rows were originally designed to add extensible records to the ML type system (Didier Rémy, Mitchell Wand). We also restate briefly the coiterative semantics for synchronous streams (Paul Caspi, Marc Pouzet), and prove the correctness of our analysis with respect to this semantics.

[HP00] Grégoire Hamon and Marc Pouzet. Modular Resetting of Synchronous Data-flow Programs. In ACM International conference on Principles of Declarative Programming (PPDP'00), Montreal, Canada, September 2000. [ bib | .ps.gz ]
This paper presents an extension of a synchronous data-flow language providing full functionality with a modular reset operator. This operator can be considered as a basic primitive for describing dynamic reconfigurations in a purely data-flow framework. The extension proposed here is conservative with respect to the fundamental properties of the initial language: reactivity (i.e, execution in bounded memory and time) and referential transparency are kept. The reset operator is thus compatible with higher-order. This is obtained by extending the clock calculus of the initial language and providing a compilation method. We illustrate the use of this operator by describing an automatic encoding of Mode-automata. All the experiments presented in the paper has been done with Lucid Synchrone, an ML extension of Lustre.

[eMP00] Jean-Louis Colaço et Marc Pouzet. Prototypages. Rapport final du projet GENIE II, Verilog SA, Janvier 2000. [ bib ]
[CP00] Paul Caspi and Marc Pouzet. Lucid Synchrone, a functional extension of Lustre. Technical report, Université Pierre et Marie Curie, Laboratoire LIP6, 2000. [ bib ]
[CP99a] Paul Caspi and Marc Pouzet. Lucid Synchrone: une extension fonctionnelle de Lustre. In Journées Francophones des Langages Applicatifs (JFLA), Morzine-Avoriaz, Février 1999. INRIA. [ bib | .ps.gz ]
[HP99] Grégoire Hamon and Marc Pouzet. Un Simulateur Synchrone pour Lucid Synchrone. In Journées Francophones des Langages Applicatifs (JFLA), Morzine-Avoriaz, Février 1999. INRIA. [ bib | .ps.gz ]
[CP99b] Paul Caspi and Marc Pouzet. Lucid Synchrone, version 1.01. Tutorial and reference manual. Laboratoire d'Informatique de Paris 6, January 1999. [ bib ]
[CP98] Paul Caspi and Marc Pouzet. A Co-iterative Characterization of Synchronous Stream Functions. In Coalgebraic Methods in Computer Science (CMCS'98), Electronic Notes in Theoretical Computer Science, March 1998. Extended version available as a VERIMAG tech. report no. 97-07 at www.lri.fr/~pouzet. [ bib | .ps.gz ]
[CP97] Paul Caspi and Marc Pouzet. A Co-iterative Characterization of Synchronous Stream Functions. Technical Report 07, VERIMAG, October 1997. [ bib | .ps.gz ]
[CP96] Paul Caspi and Marc Pouzet. Synchronous Kahn Networks. In ACM SIGPLAN International Conference on Functional Programming, Philadelphia, Pensylvania, May 1996. [ bib | .ps.gz ]
[eMP96] Paul Caspi et Marc Pouzet. Réseaux de Kahn Synchrones. In Journées Francophones des Langages Applicatifs (JFLA), Val Morin (Québec), Canada, 28-30 janvier 1996. [ bib | .ps.gz ]
[CP95] Paul Caspi and Marc Pouzet. A Functional Extension to Lustre. In M. A. Orgun and E. A. Ashcroft, editors, International Symposium on Languages for Intentional Programming, Sydney, Australia, May 1995. World Scientific. [ bib | .ps.gz ]

This file was generated by bibtex2html 1.91.