Contact Version française

The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

Publications : Florence Plateau

Back
plateau
[17] Louis Mandel and Florence Plateau. Scheduling and buffer sizing of n-synchronous systems: Typing of ultimately periodic clocks in Lucy-n. In Eleventh International Conference on Mathematics of Program Construction (MPC'12), Madrid, Spain, June 2012. [ bib | .pdf ]
Lucy-n is a language for programming networks of processes communicating through bounded buffers. A dedicated type system, termed a clock calculus, automatically computes static schedules of the processes and the sizes of the buffers between them.

In this article, we present a new algorithm which solves the subtyping constraints generated by the clock calculus. The advantage of this algorithm is that it finds schedules for tightly coupled systems. Moreover, it does not overestimate the buffer sizes needed and it provides a way to favor either system throughput or buffer size minimization.

[16] Louis Mandel, Florence Plateau, and Marc Pouzet. Static scheduling of latency insensitive designs with Lucy-n. In Formal Methods in Computer Aided Design (FMCAD 2011), Austin, TX, USA, October 2011. [ bib | .pdf ]
Lucy-n is a dataflow programming language similar to Lustre extended with a buffer operator. This language is based on the n-synchronous model which was initially introduced for programming multimedia streaming applications. In this article, we show that Lucy-n is also applicable to model Latency Insensitive Designs (LID). In order to model relay stations, we have to introduce a delay operator. Thanks to this new operator, a LID can be described by a Lucy-n program. Then, the Lucy-n compiler automatically provides static schedules for computation nodes and buffer sizes needed in the shell wrappers.

[15] Louis Mandel and Florence Plateau. Typage des horloges périodiques en Lucy-n. In Sylvain Conchon, editor, Vingt-deuxièmes Journées Francophones des Langages Applicatifs, La Bresse, France, January 2011. INRIA. [ bib | .pdf ]
Lucy-n est un langage permettant de programmer des réseaux de processus communiquant à travers des buffers de taille bornée. La taille des buffers et les rythmes d'exécution relatifs des processus sont calculés par une phase de typage appelée calcul d'horloge. Ce typage nécessite la résolution d'un ensemble de contraintes de sous-typage. L'an dernier, nous avons proposé un algorithme de résolution de ces contraintes utilisant des méthodes issues de l'interprétation abstraite. Cette année nous présentons un algorithme tirant profit de toute l'information contenue dans les types.

[14] Louis Mandel, Florence Plateau, and Marc Pouzet. Lucy-n: a n-synchronous extension of Lustre. In Tenth International Conference on Mathematics of Program Construction (MPC 2010), Québec, Canada, June 2010. [ bib | .pdf ]
Synchronous functional languages such as Lustre or Lucid Synchrone define a restricted class of Kahn Process Networks which can be executed with no buffer. Every expression is associated to a clock indicating the instants when a value is present. A dedicated type system, the clock calculus, checks that the actual clock of a stream equals its expected clock and thus does not need to be buffered. The n-synchrony relaxes synchrony by allowing the communication through bounded buffers whose size is computed at compile-time. It is obtained by extending the clock calculus with a subtyping rule which defines buffering points.

This paper presents the first implementation of the n-synchronous model inside a Lustre-like language called Lucy-n. The language extends Lustre with an explicit buffer construct whose size is automatically computed during the clock calculus. This clock calculus is defined as an inference type system and is parametrized by the clock language and the algorithm used to solve subtyping constraints. We detail here one algorithm based on the abstraction of clocks, an idea originally introduced in [6]. The paper presents a simpler, yet more precise, clock abstraction for which the main algebraic properties have been proved in Coq. Finally, we illustrate the language on various examples including a video application.

[13] Louis Mandel, Florence Plateau, and Marc Pouzet. Clock typing of n-synchronous programs. In Designing Correct Circuits (DCC 2010), Paphos, Cyprus, March 2010. [ bib ]
[12] Louis Mandel, Florence Plateau, and Marc Pouzet. Lucy-n : une extension n-synchrone de Lustre. In Éric Cariou, Laurence Duchien, and Yves Ledru, editors, Journées nationales du GDR-GPL, Pau, France, March 2010. GDR GPL. [ bib ]
[11] Louis Mandel, Florence Plateau, and Marc Pouzet. Lucy-n : une extension n-synchrone de Lustre. In Vingt-et-unièmes Journées Francophones des Langages Applicatifs, Vieux-Port La Ciotat, France, January 2010. INRIA. [ bib | .pdf ]
Les langages synchrones flot de données permettent de programmer des réseaux de processus communicant sans buffers. Pour cela, chaque flot est associé à un type d'horloges, qui indique les instants de présence de valeurs sur le flot. La communication entre deux processus f et g peut être faite sans buffer si le type du flot de sortie de f est égal au type du flot d'entrée de g. Un système de type, le calcul d'horloge, infère des types tels que cette condition est vérifiée. Le modèle n-synchrone a pour but de relâcher ce modèle de programmation en autorisant les communications à travers des buffers de taille bornée. En pratique, cela consiste à introduire une règle de sous-typage dans le calcul d'horloge.

Nous avons présenté l'année dernière un article décrivant comment abstraire des horloges pour vérifier la relation de sous-typage. Cette année, nous présentons un langage de programmation n-synchrone : Lucy-n. Dans ce langage, l'inférence des types d'horloges est paramétrable par l'algorithme de résolution des contraintes de sous-typage. Nous montrons ici un algorithme basé sur les travaux de l'an dernier et comment programmer en Lucy-n à travers l'exemple d'une application de traitement multimédia.

[10] Florence Plateau. Modèle n-synchrone pour la programmation de réseaux de Kahn à mémoire bornée. Thèse de doctorat, Université Paris-Sud, 2010. [ bib ]
[9] Louis Mandel, Florence Plateau, and Marc Pouzet. The ReactiveML toplevel (tool demonstration). In ACM SIGPLAN Workshop on ML, Edinburgh, Scotland, UK, August 2009. [ bib ]
[8] Albert Cohen, Louis Mandel, Florence Plateau, and Marc Pouzet. Relaxing synchronous composition with clock abstraction. In Hardware Design using Functional languages (HFL 09), pages 35-52, York, UK, March 2009. [ bib ]
[7] Louis Mandel and Florence Plateau. Abstraction d'horloges dans les systèmes synchrones flot de données. In Vingtièmes Journées Francophones des Langages Applicatifs, Saint-Quentin sur Isère, January 2009. INRIA. [ bib | .pdf ]
Les langages synchrones flot de données tels que Lustre manipulent des séquences infinies de données comme valeurs de base. Chaque flot est associé à une horloge qui définit les instants où sa valeur est présente. Cette horloge est une information de type et un système de types dédié, le calcul d'horloges, rejette statiquement les programmes qui ne peuvent pas être exécutés de manière synchrone. Dans les langages synchrones existants, cela revient à se demander si deux flots ont la même horloge et repose donc uniquement sur l'égalité d'horloges. Des travaux récents ont montré l'intérêt d'introduire une notion relâchée du synchronisme, où deux flots peuvent être composés dès qu'ils peuvent être synchronisés par l'introduction d'un buffer de taille bornée (comme c'est fait dans le modèle SDF d'Edward Lee). Techniquement, cela consiste à remplacer le typage par du sous-typage. Ce papier est une traduction et amélioration technique de [6] qui présente un moyen simple de mettre en oeuvre ce modèle relâché par l'utilisation d'horloges abstraites. Les valeurs abstraites représentent des ensembles d'horloges concrètes qui ne sont pas nécessairement périodiques. Cela permet de modéliser divers aspects des logiciels temps-réel embarqués, tels que la gigue bornée présente dans les systèmes vidéo, le temps d'exécution des processus temps réel et, plus généralement, la communication à travers des buffers de taille bornée. Nous présentons ici l'algèbre des horloges abstraites et leurs principales propriétés théoriques.

[6] Albert Cohen, Louis Mandel, Florence Plateau, and Marc Pouzet. Abstraction of Clocks in Synchronous Data-flow Systems. In The Sixth ASIAN Symposium on Programming Languages and Systems (APLAS), Bangalore, India, December 2008. [ bib | PDF | .pdf ]
Synchronous data-flow languages such as Lustre manage infinite sequences or streams as basic values. Each stream is associated to a clock which defines the instants where the current value of the stream is present. This clock is a type information and a dedicated type system - the so-called clock-calculus - statically rejects programs which cannot be executed synchronously. In existing synchronous languages, it amounts at asking whether two streams have the same clocks and thus relies on clock equality only. Recent works have shown the interest of introducing some relaxed notion of synchrony, where two streams can be composed as soon as they can be synchronized through the introduction of a finite buffer (as done in the SDF model of Edward Lee). This technically consists in replacing typing by subtyping. The present paper introduces a simple way to achieve this relaxed model through the use of clock envelopes. These clock envelopes are sets of concrete clocks which are not necessarily periodic. This allows to model various features in real-time embedded software such as bounded jitter as found in video-systems, execution time of real-time processes and scheduling resources or the communication through buffers. We present the algebra of clock envelopes and its main theoretical properties.

[5] Louis Mandel and Florence Plateau. Interactive programming of reactive systems. In Proceedings of Model-driven High-level Programming of Embedded Systems (SLA++P'08), Electronic Notes in Computer Science, pages 44-59, Budapest, Hungary, April 2008. Elsevier Science Publishers. [ bib | PDF | .pdf ]
[4] 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) [3]. [ bib ]
[3] 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 ]
[2] Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, and Marc Pouzet. Synchronizing periodic clocks. In ACM International Conference on Embedded Software (EMSOFT'05) [1]. [ bib ]
[1] Albert Cohen, Marc Duranton, Christine Eisenbeis, Claire Pagetti, Florence Plateau, and Marc Pouzet. Synchronizing periodic clocks. In ACM International Conference on Embedded Software (EMSOFT'05), Jersey city, New Jersey, USA, September 2005. [ bib ]

Back
This page was generated by bibtex2html.