@comment{{This file has been generated by bib2bib 1.96}}
@comment{{Command line: bib2bib --expand /Users/pouzet/bib/these.bib /Users/pouzet/bib/lucy.bib /Users/pouzet/bib/rml.bib}}
@techreport{pouzet:spectre95,
author = {Marc Pouzet},
title = {Fast Compaction of Tail-recursive Expressions using
an Abstract Distance},
institution = {Verimag},
year = 1995,
number = {Spectre-95-3},
month = {February},
address = {Grenoble, France},
note = {Available by anonymous ftp on
{\tt imag.fr} in {\tt pub/SPECTRE}}
}
@phdthesis{pouzet:these94,
author = {Marc Pouzet},
title = {Compaction des langages Fonctionnels},
school = {Universit\'e {Paris VII}},
year = 1994,
month = {October}
}
@inproceedings{pouzet:rempar93,
author = {Marc Pouzet},
title = {Parall\'elisation \`a Grain Fin des Programmes Fonctionnels},
booktitle = {5-i\`emes Rencontres du Parall\'elisme},
year = 1993,
month = {Mai},
address = {Brest, France}
}
@inproceedings{pouzet:CAPD94,
author = {Marc Pouzet},
title = {Fine Grain Parallelisation of Functional Programs for
{VLIW} or Superscalars Architectures},
booktitle = {IFIP WG 10.3 International Conference on Applications in
Parallel and Distributed Computing},
organisation = {IFIP WG 10.3},
year = 1994,
month = {April},
address = {Caracas,Venezuela}
}
@inproceedings{pouzet:europar95,
author = {Marc Pouzet},
title = {{The Program Compaction Revisited: the Functional Framework}},
booktitle = {International Conference on Parallel Processing
(EURO-PAR'95)},
series = {LNCS 966},
address = {Stockholm, Sweden},
year = 1995,
month = {August 29-31},
url = {euro-par95.ps.gz}
}
@inproceedings{pouzet:pact96,
author = {Marc Pouzet},
title = {Using the Parallel Complexity of Programs to Improve
Compaction},
booktitle = {IEEE International Conference on Parallel
Architectures and Compilation Techniques (PACT)},
year = 1996,
month = {October},
address = {Boston},
url = {pact96.ps.gz}
}
@article{pouzet:tsi96,
author = {Marc Pouzet},
title = {Une pr\'esentation fonctionnelle de la compaction de code},
journal = {Techniques et Sciences Informatiques (TSI)},
year = 1996,
volume = 15,
number = 7,
note = {Num\'ero sp\'ecial "langages applicatifs"},
url = {tsi96.ps.gz}
}
@inproceedings{lucy:islip95,
author = {Paul Caspi and Marc Pouzet},
title = {{A Functional Extension to Lustre}},
booktitle = {International Symposium on Languages for
Intentional Programming},
year = 1995,
month = {May},
address = {Sydney, Australia},
editor = {M.~A. Orgun and E.~A. Ashcroft},
publisher = {World Scientific},
url = {islip95.ps.gz}
}
@inproceedings{lucy:jfla96,
author = {Paul Caspi et Marc Pouzet},
title = {{R\'eseaux de Kahn Synchrones}},
booktitle = {Journ\'ees Francophones des Langages Applicatifs (JFLA)},
year = 1996,
month = {28-30 janvier},
address = {Val Morin (Qu\'ebec), Canada},
url = {jfla96.ps.gz}
}
@inproceedings{lucy:icfp96,
author = {Paul Caspi and Marc Pouzet},
title = {{Synchronous Kahn Networks}},
booktitle = {ACM SIGPLAN International Conference on
Functional Programming (ICFP)},
year = 1996,
month = {May},
address = {Philadelphia, Pensylvania},
url = {icfp96.ps.gz}
}
@inproceedings{lucy:cmcs98,
author = {Paul Caspi and Marc Pouzet},
title = {{A Co-iterative Characterization of
Synchronous Stream Functions}},
booktitle = {Coalgebraic Methods in Computer Science
(CMCS'98)},
series = {Electronic Notes in Theoretical Computer Science},
year = 1998,
month = {March},
note = {Extended version available as a VERIMAG tech. report
no. 97--07 at {\tt www.di.ens.fr/$\sim$pouzet/bib/bib.html}},
url = {cmcs98.ps.gz},
url = {coiteration-report98.ps.gz}
}
@techreport{lucy:verimag97,
author = {Paul Caspi and Marc Pouzet},
title = {{A Co-iterative Characterization of
Synchronous Stream Functions}},
institution = {VERIMAG},
year = 1997,
number = 07,
month = {October},
url = {coiteration-report98.ps.gz}
}
@inproceedings{lucy:jfla99,
author = {Paul Caspi and Marc Pouzet},
title = {{Lucid Synchrone: une extension fonctionnelle de Lustre}},
booktitle = {Journ\'ees Francophones des Langages Applicatifs (JFLA)},
year = 1999,
address = {Morzine-Avoriaz},
month = {F\'evrier},
publisher = {INRIA},
url = {jfla99.ps.gz}
}
@inproceedings{lucy:jfla99-2,
author = {Gr\'egoire Hamon and Marc Pouzet},
title = {{Un Simulateur Synchrone pour Lucid Synchrone}},
booktitle = {Journ\'ees Francophones des Langages Applicatifs (JFLA)},
year = 1999,
address = {Morzine-Avoriaz},
month = {F\'evrier},
publisher = {INRIA},
url = {jfla99-2.ps.gz}
}
@misc{lucy:genie00,
author = {Jean-Louis Cola\c{c}o et Marc Pouzet},
title = {{Prototypages}},
howpublished = {Rapport final du projet GENIE II, Verilog SA},
month = {Janvier},
year = 2000
}
@manual{lucy:manual99,
title = {{Lucid Synchrone, version 1.01. Tutorial and
reference manual}},
author = {Paul Caspi and Marc Pouzet},
organization = {Laboratoire d'Informatique de Paris 6},
month = {January},
year = 1999
}
@manual{lucy:manual01,
author = {Marc Pouzet},
title = {{Lucid Synchrone}, version 2.
{Tutorial and reference manual}},
organization = {Universit\'e Pierre et Marie Curie, LIP6},
month = {Mai},
year = 2001,
note = {Distribution available at:
{\tt www.lri.fr/$\sim$pouzet/lucid-synchrone}}
}
@manual{lucy:manual06,
author = {Marc Pouzet},
title = {{Lucid Synchrone}, version 3.
{Tutorial and reference manual}},
organization = {Universit\'e Paris-Sud, LRI},
month = {April},
year = 2006
}
@techreport{lucy:lip6-00,
author = {Paul Caspi and Marc Pouzet},
title = {{Lucid Synchrone}, a functional extension of {Lustre}},
institution = {Universit\'e Pierre et Marie Curie, Laboratoire LIP6},
year = 2000
}
@unpublished{lucy:toplas,
author = {Paul Caspi and Marc Pouzet},
title = {{Lucid Synchrone}, a functional extension of {Lustre}},
note = {Submitted to publication},
year = 2002
}
@inproceedings{lucy:ppdp00,
author = {Gr\'egoire Hamon and Marc Pouzet},
title = {{Modular Resetting of Synchronous Data-flow Programs}},
booktitle = {ACM International conference on
Principles of Declarative Programming (PPDP'00)},
year = 2000,
address = {Montreal, Canada},
month = {September},
url = {ppdp00.ps.gz},
abstract = { 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.}
}
@inproceedings{lucy:esop01,
author = {Pascal Cuoq and Marc Pouzet},
title = {{Modular Causality in a Synchronous Stream Language}},
booktitle = {European Symposium on Programming (ESOP'01)},
year = 2001,
address = {Genova, Italy},
month = {April},
url = {esop01.ps.gz},
abstract = {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 \hbox{originally} designed to add
extensible records to the ML type system (Didier R\'emy, Mitchell
Wand). We \hbox{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.}
}
@inproceedings{lucy:lpar01,
author = {Sylvain Boulm\'e and Gr\'egoire Hamon},
title = {{Certifying Synchrony for Free}},
booktitle = {International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR)},
year = 2001,
volume = 2250,
address = {La Havana, Cuba},
month = {December},
publisher = {Lecture Notes in Artificial Intelligence, Springer-Verlag},
note = {Short version of {\em A clocked denotational semantics for
{L}ucid-{S}ynchrone in {C}oq}, available as a Technical
Report (LIP6), at
{\tt www.di.ens.fr/$\sim$pouzet/bib/bib.html}},
url = {lpar01.ps.gz},
url = {lucid_in_coq_report.ps.gz},
abstract = {We express reactive programs in Coq using data-flow synchronous
operators. Following Lucid Synchrone approach, synchro\-nous static
constraints are here expressed using dependent types. Hence, our
analysis of synchrony is here directly performed by Coq typechecker.}
}
@inproceedings{lucy:slap02,
author = {Jean-Louis Cola\c{c}o and Marc Pouzet},
title = {{Type-based Initialization Analysis of a
Synchronous Data-flow Language}},
booktitle = {{Synchronous Languages, Applications,
and Programming}},
publisher = {Electronic Notes in Theoretical Computer Science},
volume = 65,
year = 2002,
url = {slap02.ps.gz},
abstract = {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 {\em 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
{\em 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.}
}
@inproceedings{lucy:hamon-slap04,
author = {Gr\'egoire Hamon},
title = {{Synchronous Data-flow Pattern Matching}},
booktitle = {{Synchronous Languages, Applications,
and Programming}},
publisher = {Electronic Notes in Theoretical Computer Science},
year = 2004,
url = {hamon-slap04.ps.gz}
}
@phdthesis{lucy:these-hamon02,
author = {Gr\'egoire Hamon},
title = {{Calcul d'horloge et Structures de Contr\^ole
dans Lucid Synchrone, un langage de flots synchrones
\`a la ML}},
school = {Universit\'e Pierre et Marie Curie},
year = 2002,
address = {Paris, France},
month = {14 novembre}
}
@phdthesis{lucy:these-cuoq02,
author = {Pascal Cuoq},
title = {{Ajout de synchronisme dans les langages
fonctionnels typ\'es}},
school = {Universit\'e Pierre et Marie Curie},
year = 2002,
address = {Paris, France},
month = {october}
}
@manual{lucy:habilitation-pouzet02,
author = {Marc Pouzet},
title = {{Lucid Synchrone}: un langage synchrone d'ordre
sup\'erieur},
organisation = {Universit\'e Pierre et Marie Curie},
year = 2002,
address = {Paris, France},
month = {14 novembre},
note = {Habilitation \`a diriger les recherches },
url = {habilitation-pouzet02.ps.gz}
}
@inproceedings{lucy:emsoft03,
author = {Jean-Louis Cola\c{c}o and Marc Pouzet},
title = {{Clocks as First Class Abstract Types}},
booktitle = {Third International Conference on
Embedded Software (EMSOFT'03)},
address = {Philadelphia, Pennsylvania, USA},
month = {october},
year = 2003,
url = {emsoft03.ps.gz},
abstract = {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 {\em dependent types},
the paper presents a simpler clock calculus reminiscent to ML type
systems with first order abstract types {\em \`a 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.}
}
@inproceedings{lucy:emsoft04,
author = {Jean-Louis Cola\c{c}o and
Alain Girault and Gr\'egoire Hamon and Marc Pouzet},
title = {{Towards a Higher-order Synchronous Data-flow Language}},
booktitle = {ACM Fourth International
Conference on Embedded Software (EMSOFT'04)},
address = {Pisa, Italy},
month = {september},
year = 2004,
url = {emsoft04.pdf},
abstract = {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.}
}
@article{lucy:sttt04,
author = {Jean-Louis Cola\c{c}o and Marc Pouzet},
title = {{Type-based Initialization Analysis of a
Synchronous Data-flow Language}},
journal = {International Journal on Software Tools
for Technology Transfer (STTT)},
year = {2004},
month = {August},
volume = {6},
number = {3},
pages = {245--255}
}
@unpublished{lucy:jfp05,
author = {Jean-Louis Cola\c{c}o and Marc Pouzet},
title = {{Clocks as First Class Abstract Types}},
note = {Submitted to the Journal of Functional Programming (JFP)},
year = 2005
}
@article{lucy:tecs06,
author = {Alain Girault and Xavier Nicollin and Marc Pouzet},
title = {{Automatic Rate Desynchronization of Embedded Reactive Programs}},
journal = {ACM Transactions on Embedded Computing Systems (TECS)},
volume = 5,
number = 3,
year = 2006
}
@inproceedings{lucy:emsoft05a,
author = {Albert Cohen and Marc Duranton and Christine Eisenbeis
and Claire Pagetti and Florence Plateau and Marc Pouzet},
title = {{Synchroning Periodic Clocks}},
booktitle = {ACM International Conference on
Embedded Software (EMSOFT'05)},
address = {Jersey city, New Jersey, USA},
month = {September},
year = 2005,
url = {emsoft05a.pdf}
}
@inproceedings{lucy:emsoft05b,
author = {Jean-Louis Cola\c{c}o and Bruno Pagano and Marc Pouzet},
title = {{A Conservative Extension of Synchronous Data-flow with
State Machines}},
booktitle = {ACM International Conference on
Embedded Software (EMSOFT'05)},
address = {Jersey city, New Jersey, USA},
month = {September},
year = 2005,
url = {emsoft05b.pdf},
abstract = {This paper presents an extension of a synchronous
data-flow language such as Lustre with imperative features expressed
in terms of powerful state machine \`a 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.
}
}
@inproceedings{lucy:popl06,
author = {Albert Cohen and Marc Duranton and Christine Eisenbeis
and Claire Pagetti and Florence Plateau and Marc Pouzet},
title = {{$N$-Synchronous Kahn Networks: a Relaxed Model of Synchrony for Real-Time Systems}},
booktitle = {ACM International Conference on
Principles of Programming Languages (POPL'06)},
address = {Charleston, South Carolina, USA},
month = {January},
year = 2006,
url = {popl06.pdf},
abstract = { 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$-\emph{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.}
}
@inbook{lucy:hermes06,
author = {Paul Caspi and Gr\'egoire Hamon and Marc Pouzet},
editor = {Nicolas Navet},
title = {{Syst\`emes Temps-r\'eel~: Techniques de Description et
de V\'erification -- Th\'eorie et Outils}},
chapter = {{Lucid Synchrone, un langage de programmation des
syst\`emes r\'eactifs}},
publisher = {Hermes},
volume = {1},
year = 2006,
pages = {217-260},
url = {chap_lucid_synchrone_hermes06.pdf},
abstract = {Ce chapitre pr\'esente {\bf Lucid Synchrone},
un langage d\'edi\'e \`a
la programmation de syst\`emes r\'eactifs. Il est fond\'e sur le
mod\`ele synchrone de {\bf Lustre} qu'il \'etend avec
des caract\'eristiques pr\'esentes dans les langages fonctionnels tels
que l'ordre sup\'erieur ou l'inf\'erence des types. Il offre un
m\'ecanisme de synth\`ese automatique des horloges et permet de
d\'ecrire, dans un cadre unifi\'e, une programmation flot de donn\'ees
et une programmation par automates.
Ce chapitre est une pr\'esentation du langage, destin\'ee \`a la fois au
programmeur cherchant \`a se familiariser avec celui-ci, mais aussi au
chercheur s'int\'eressant aux syst\`emes r\'eactifs et aux techniques qui
peuvent \^etre appliqu\'ees au niveau d'un langage, pour faciliter les
activit\'es de sp\'ecification, de programmation et de v\'erification.
}
}
@inproceedings{lucy:emsoft06,
author = {Jean-Louis Cola\c{c}o and Gr\'egoire Hamon and Marc Pouzet},
title = {{Mixing Signals and Modes in Synchronous
Data-flow Systems}},
booktitle = {ACM International Conference on
Embedded Software (EMSOFT'06)},
address = {Seoul, South Korea},
month = {October},
year = 2006,
url = {emsoft06.pdf},
abstract = {
Synchronous data-flow languages such as SCADE/Lustre manage
infinite sequences or {\em 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 {\em 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 {\em 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. }
}
@inproceedings{labbe07,
author = {S\'ebastien Labb\'e and Jean-Pierre Gallois and
Marc Pouzet},
title = {Slicing Communicating Automata Specifications
For Efficient Model Reduction},
booktitle = {18th Australian Conference on Software Engineering (ASWEC)},
year = 2007
}
@inbook{lucy:iste07,
author = {Paul Caspi and Gr\'egoire Hamon and Marc Pouzet},
title = {Real-Time Systems: Models and verification --- Theory
and tools},
chapter = {{Synchronous Functional Programming with Lucid Synchrone}},
publisher = {ISTE},
year = 2007,
editors = {Nicolas Navet and Stephan Mertz},
note = {English translation of~\cite{lucy:hermes06}},
url = {chap_lucid_synchrone_english_iste08.pdf},
abstract = {Lucid Synchrone is a programming language dedicated to
the design of reactive systems. It is based on the synchronous model
of Lustre which it extends with
features usually found in functional languages such as higher-order
or constructed data-types.
The language is equipped with several static analysis, all expressed
as special type-systems and used to ensure the absence of certain
run-time errors on the final application. It provides, in particular,
automatic type and clock inference and statically detects
initialization issues or dead-locks.
Finally, the language offers both data-flow and automata-based
programming inside a unique framework.}
}
@misc{lucy:caspicolacopouzet07,
author = {Paul Caspi and Jean-Louis Cola\c{c}o and Marc Pouzet},
title = {{Objects in Block-Diagram Languages}},
month = {January},
year = 2008,
note = {Unpublished}
}
@inproceedings{lucy:apges07,
author = {Darek Biernacki and Jean-Louis Colaco and Marc Pouzet},
title = {{Clock-directed Modular Compilation from
Synchronous Block-diagrams}},
booktitle = {Workshop on Automatic Program Generation for Embedded
Systems (APGES)},
year = 2007,
address = {Salzburg, Austria},
month = {october},
note = {Embedded System Week},
url = {apges07.pdf}
}
@inproceedings{lucy:lctes08b,
author = {Gwenael Delaval and Alain Girault and Marc Pouzet},
title = {{A Type System for the Automatic Distribution
of Higher-order Synchronous Dataflow Programs}},
booktitle = {ACM International Conference on
Languages, Compilers, and Tools for Embedded Systems
(LCTES)},
year = 2008,
address = {Tucson, Arizona},
month = {June},
url = {lctes08b.pdf},
abstract = {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.
}
}
@inproceedings{lucy:lctes08a,
author = {Darek Biernacki and Jean-Louis Colaco and Gr\'egoire Hamon
and Marc Pouzet},
title = {{Clock-directed Modular Code Generation of Synchronous Data-flow
Languages}},
booktitle = {ACM International Conference on
Languages, Compilers, and Tools for Embedded Systems
(LCTES)},
year = 2008,
address = {Tucson, Arizona},
month = {June},
url = {lctes08a.pdf},
abstract = {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.
}
}
@inproceedings{lucy:aplas08,
author = {Albert Cohen and Louis Mandel and Florence Plateau and
Marc Pouzet},
title = {{Abstraction of Clocks in Synchronous Data-flow Systems}},
booktitle = {The Sixth ASIAN Symposium on Programming Languages and Systems
(APLAS)},
year = 2008,
month = {December},
date = {9--11},
address = {Bangalore, India},
abstract = {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
sub-typing. The present paper introduces a simple way to achieve
this relaxed model through the use of clock
envelopes. These clock envelopes are set 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.},
url = {aplas08.pdf},
x-type = {article},
topics = {team}
}
@misc{lucy:hfl09,
author = {Albert Cohen and Louis Mandel and Florence Plateau
and Marc Pouzet},
title = {{Relaxing Synchronous Composition with Clock Abstraction}},
howpublished = {Workshop on Hardware Design using Functional languages
(HFL 09) - ETAPS},
year = 2009,
address = {York, UK},
url = {http://www.lri.fr/~plateau/hfl09/},
topics = {team}
}
@inproceedings{lucy:lctes09,
author = {Paul Caspi and Jean-Louis Cola\c{c}o and L\'eonard G\'erard
and Marc Pouzet and Pascal Raymond},
title = {{Synchronous Objects with Scheduling Policies}:
Introducing Safe Shared Memory in {Lustre}},
year = {2009},
month = {June},
address = {Dublin},
booktitle = {ACM International Conference on
Languages, Compilers, and Tools for Embedded Systems
(LCTES)},
abstract = {This paper addresses the problem of designing and implementing
complex control systems for real-time embedded software. Typical
applications involve different control laws corresponding to
different phases or modes, e.g., take-off, full flight and
landing in a fly-by-wire control system. On one hand, existing
methods such as the combination of Simulink/Stateflow provide
powerful but unsafe mechanisms by means of imperative updates of
shared variables. On the other hand, synchronous languages and
tools such as Esterel or Scade/Lustre are too restrictive and
forbid to fully separate the specification of modes from their
actual instantiation with a particular control automaton.
In this paper, we introduce a conservative extension of a
synchronous data-flow language close to Lustre, in order to be able
to define systems with modes in a more modular way, while insuring
the absence of data-races. We show that such a system can be viewed
as an object where modes are methods acting on a shared
memory. The object is associated to a scheduling policy which
specifies the ways methods can be called to build a valid
synchronous reaction. We show that the verification of the proper
use of an object reduces to a
type inference problem using row types introduced by Wand,
R\'emy and Vouillon. We define the semantics of the extended
synchronous language and the type system.
The proposed extension has been implemented and we illustrate its
use through several examples.},
url = {lctes09.pdf},
x-type = {article},
topics = {team}
}
@inproceedings{lucy:emsoft09,
author = {Marc Pouzet and Pascal Raymond},
title = {{Modular Static Scheduling of Synchronous Data-flow
Networks: An efficient symbolic representation}},
booktitle = {ACM International Conference on
Embedded Software (EMSOFT'09)},
address = {Grenoble, France},
month = {October},
year = 2009,
url = {emsoft09.pdf},
x-type = {article},
topics = {team},
abstract = {This paper addresses the question of producing modular sequential
imperative code from synchronous data-flow networks. Precisely,
given a system with several input and output flows, how to decompose
it into a minimal number of classes executed atomically and
statically scheduled without restricting possible feedback loops
between input and output?
Though this question has been identified by Raymond in the early
years of Lustre, it has almost been left aside until the recent
work of Lublinerman, Szegedy and Tripakis. The problem is proven to
be intractable, in the sense that it belongs to the family of
optimization problems where the corresponding decision problem ---
there exists a solution with size $c$ --- is NP-complete. Then, the
authors derive an iterative algorithm looking for
solutions for $c = 1,2,...$ where each step is encoded as a SAT
problem.
Despite the apparent intractability of the problem, our experience
is that real programs do not exhibit such a complexity.
Based on earlier work by Raymond, this paper presents a new symbolic encoding
of the problem in terms of input/output relations. This encoding
simplifies the problem, in the sense that it rejects
solutions, while keeping all the optimal ones. It allows, in
polynomial time, (1) to identify nodes for which several schedules
are feasible and thus are possible sources of combinatorial
explosion; (2) to obtain solutions which in some cases are already
optimal; (3) otherwise, to get a non trivial lower bound for $c$ to
start an iterative combinatorial search.
The solution applies to a large class of
block-diagram formalisms based on atomic computations and a
delay operator, ranging from synchronous languages such as
Lustre or SCADE to modeling tools such as Simulink.}
}
@article{lucy:jdaes10,
author = {Marc Pouzet and Pascal Raymond},
title = {{Modular Static Scheduling of Synchronous Data-flow
Networks: An efficient symbolic representation}},
journal = {Journal of Design Automation for Embedded Systems},
year = 2010,
note = {Special issue of selected papers from
\url{http://esweek09.inrialpes.fr/}{Embedded System Week}.
Extended version of~\cite{lucy:emsoft09}.},
volume = {3},
number = {14},
pages = {165-192},
pdf = {jdaes10.pdf},
url = {http://www.springerlink.com/content/0929-5585/14/3/},
abstract = {This paper addresses the question of producing modular
sequential imperative code from synchronous
data-flow networks. Precisely, given a system with
several input and output flows, how to decompose it
into a minimal number of classes executed atomically
and statically scheduled without restricting
possible feedback loops between input and output?
Though this question has been identified by Raymond
in the early years of LUSTRE, it has almost been
left aside until the recent work of Lublinerman,
Szegedy and Tripakis. The problem is proven to be
intractable, in the sense that it belongs to the
family of optimization problems where the
corresponding decision problem --- there exists a
solution with size $c$ --- is NP-complete. Then, the
authors derive an iterative algorithm looking for
solutions for $c = 1, 2,...$ where each step is
encoded as a satisfiability (SAT) problem.
Despite the apparent intractability of the problem, our
experience is that real programs do not exhibit such
a complexity. Based on earlier work by Raymond, the
current paper presents a new encoding of the problem
in terms of input/output relations. This encoding
simplifies the problem, in the sense that it rejects
some solutions, while keeping all the optimal
ones. It allows, in polynomial time, (1) to identify
nodes for which several schedules are feasible and
thus are possible sources of combinatorial
explosion; (2) to obtain solutions which in some
cases are already optimal; (3) otherwise, to get a
non trivial lower bound for c to start an iterative
combinatorial search. The method has been validated
on several industrial examples.}
}
@misc{lucy:dcc10,
author = {Louis Mandel and Florence Plateau
and Marc Pouzet},
title = {{Lucy-n: a n-Synchronous Extension of Lustre}},
howpublished = {Workshop on Designing Correct Circuits
(DCC 10) - ETAPS},
year = 2010,
month = {March},
address = {Paphos, Cyprus}
}
@article{lucy:tecs09,
author = {C\'edric Auger and Jean-Louis Cola\c{c}o and Xun Gong
and Gr\'egoire Hamon and Marc Pouzet},
title = {{From Lustre to Sequential Code: A Formalization}},
journal = {Submitted to ACM TECS},
year = 2009
}
@phdthesis{lucy:these-delaval08,
author = {Gw\"enael Delaval},
title = {{R\'epartition modulaire de programmes synchrones}},
school = {Institut Polytechnique de Grenoble},
year = 2008,
address = {Grenoble, France},
month = {1er juillet}
}
@phdthesis{lucy:these-plateau10,
author = {Florence Plateau},
title = {{Mod\`ele \emph{n}-synchrone pour la programmation de r\'eseaux de Kahn
\`a m\'emoire born\'ee}},
school = {Universit\'e Paris-Sud~11},
year = 2010,
address = {Orsay, France},
month = {6 janvier},
url = {www.lri.fr/~plateau}
}
@inproceedings{lucy:jfla10,
author = {Louis Mandel and Florence Plateau
and Marc Pouzet},
title = {{Lucy-n: une extension n-Synchrone de Lustre}},
booktitle = {Journ\'ees Francophones des Langages Applicatifs (JFLA)},
year = 2010,
address = {La Ciota, France},
month = {Janvier},
organization = {INRIA}
}
@inproceedings{lucy:cdc10,
author = {Albert Benveniste and Benoit Caillaud and Marc Pouzet},
title = {{The Fundamentals of Hybrid Systems Modelers}},
booktitle = {49th IEEE International Conference on Decision and Control (CDC)},
year = {2010},
address = {Atlanta, Georgia, USA},
month = {December 15-17},
url = {cdc10.pdf},
abstract = { Hybrid systems modelers have become the corner stone of
embedded system development, with Simulink a de facto standard and
Modelica a new player. Such tools still raise
a number of issues that, we believe, require more fundamental understanding.
In
this paper we propose using \emph{non standard analysis} as a
semantic domain for hybrid systems --- non standard analysis is an
extension of classical analysis in which infinitesimals (the
$\varepsilon$ and $\eta$ in the celebrated generic sentence
$\forall \varepsilon. \exists \eta \dots$ in college maths) can be
manipulated as first class citizens. This allows us to provide a
denotational semantics and a constructive semantics for hybrid
systems, thus establishing simulation engines on a firm mathematical
basis. In passing, we cleanly separate the job of the numerical
analyst (solving differential equations) from that of the computer
scientist (generating execution schemes).}
}
@inproceedings{lucy:mpc10,
author = {Louis Mandel and Florence Plateau and Marc Pouzet},
title = {{Lucy-n: a n-Synchronous Extension of Lustre}},
booktitle = {10th International Conference on Mathematics of
Program Construction (MPC'10)},
month = {June},
year = 2010,
address = {Manoir St-Castin, Qu\'ebec, Canada},
publisher = {Springer LNCS},
url = {mpc10.pdf},
abstract = {
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 LucyN. 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~\cite{lucy:aplas08}. 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.
}
}
@inproceedings{lucy:lctes11,
author = {Albert Benveniste and Timothy Bourke and
Benoit Caillaud and Marc Pouzet},
title = {{Divide and recycle: types and compilation for a
hybrid synchronous language}},
booktitle = {ACM SIGPLAN/SIGBED Conference on Languages,
Compilers, Tools and Theory for Embedded Systems (LCTES'11)},
month = {April},
address = {Chicago, USA},
year = 2011,
url = {lctes11.pdf},
abstract = {Hybrid modelers such as Simulink have become corner stones of embedded
systems development.
They allow both \emph{discrete} controllers and their \emph{continuous}
environments to be expressed \emph{in a single language}.
Despite the availability of such tools, there remain a number of issues
related to the lack of reproducibility of simulations and to the
separation of the continuous part, which has to be exercised by a
numerical solver, from the discrete part, which must be guaranteed not to
evolve during a step.
Starting from a minimal, yet full-featured, Lustre-like synchronous
language, this paper presents a conservative extension
where data-flow equations can be mixed with ordinary differential
equations (ODEs) with possible reset.
A type system is proposed to statically distinguish discrete computations
from continuous ones and to ensure that signals are used in their proper
domains.
We propose a semantics based on \emph{non-standard analysis} which gives a
synchronous interpretation to the whole language, clarifies the
discrete/continuous interaction and the treatment of zero-crossings, and
also allows the correctness of the type system to be established.
The extended data-flow language is realized through a source-to-source
transformation into a synchronous subset, which can then be compiled using
existing tools into routines that are both efficient and bounded in their
use of memory.
These routines are orchestrated with a single off-the-shelf numerical
solver using a simple but precise algorithm which treats causally-related
cascades of zero-crossings.
We have validated the viability of the approach through experiments with
the SUNDIALS library.},
x-type = {article},
topics = {team}
}
@article{lucy:jcss11,
author = {Albert Benveniste and Timothy Bourke and Benoit
Caillaud and Marc Pouzet},
title = {{Non-Standard Semantics of Hybrid Systems Modelers}},
journal = {Journal of Computer and System Sciences (JCSS)},
year = 2012,
note = {Special issue in honor of Amir Pnueli},
doi = {http://dx.doi.org/10.1016/j.jcss.2011.08.009},
volume = {78},
month = {May},
pages = {877-910},
url = {jcsspaper.pdf},
abstract = { Hybrid system modelers have become a corner stone of complex
embedded system development. Embedded systems include not only
control components and software, but also physical devices. In this
area, Simulink is a de facto standard design framework, and Modelica
a new player. However, such tools raise several issues related to
the lack of reproducibility of simulations (sensitivity to
simulation parameters and to the choice of a simulation engine).
In this paper we propose using techniques from \emph{non-standard
analysis} to define a semantic domain for hybrid systems.
Non-standard analysis is an extension of classical analysis in which
infinitesimal (the $\varepsilon$ and $\eta$ in the celebrated
generic sentence $\forall\varepsilon\exists\eta\dots$ of college
maths) can be manipulated as first class citizens. This approach
allows us to define both a denotational semantics, a constructive
semantics, and a Kahn Process Network semantics for hybrid systems,
thus establishing simulation engines on a sound but flexible
mathematical foundation. These semantics offer a clear distinction
between the concerns of the numerical analyst (solving differential
equations) and those of the computer scientist (generating execution
schemes).
We also discuss a number of practical and fundamental issues in
hybrid system modelers that give rise to non reproducibility of
results, nondeterminism, and undesirable side effects. Of particular
importance are cascaded mode changes (also called ``zero-crossings''
in the context of hybrid systems modelers).}
}
@inproceedings{lucy:emsoft11,
author = {Albert Benveniste and Timothy Bourke and
Benoit Caillaud and Marc Pouzet},
title = {{A Hybrid Synchronous Language with Hierarchical
Automata}: {Static Typing and Translation to Synchronous Code}},
booktitle = {ACM SIGPLAN/SIGBED Conference on Embedded Software (EMSOFT'11)},
month = {October},
address = {Taipei, Taiwan},
year = 2011,
url = {emsoft11.pdf},
abstract = {Hybrid modeling tools such as Simulink
have evolved from simulation
platforms into development platforms on which simulation, testing, formal
verification and code generation are performed.
It is thus critical to place them on a firm semantical basis where it can be
proven that the results of simulation, compilation and verification are
mutually consistent.
Synchronous languages have addressed these issues but only for
discrete systems.
They cannot be used to model hybrid systems with both efficiency and
precision.
Following the approach of Benveniste et al., we present the design of
a hybrid modeler built from a synchronous language and an
off-the-shelf numerical solver. The main novelty is a language which
includes
control structures, such as hierarchical
automata, for both continuous and discrete contexts. These constructs
can be arbitrarily mixed with data-flow and ordinary differential
equations (ODEs). A type system is required to statically ensure that
all discrete state changes are aligned with zero-crossing events and
that the function passed to the numerical solver is free of
side-effects during integration.
We show that well-typed programs can be compiled through a source-to-source
translation into synchronous code which is then translated into
sequential code using an existing synchronous language compiler.
Based on the presented material, a compiler for a new synchronous language
with hybrid features has been developed.
We demonstrate its effectiveness on some examples.
}
}
@inproceedings{lucy:fmcad11,
author = {Louis Mandel and Florence Plateau and Marc Pouzet},
title = {{Static Scheduling of Latency Insensitive Designs
with Lucy-n}},
year = 2011,
booktitle = {International Conference on
Formal Methods in Computer-Aided Design (FMCAD)},
address = {Austin, Texas, USA},
month = {October 30 -- November 2},
abstract = {Lucy-n is a data-flow programming language similar to Lustre
extended with a buffer operator.
It 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 latency
introduced by wires, we add 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 shell
wrappers.},
url = {MandelPlateauPouzet-FMCAD-2011.pdf}
}
@inproceedings{lucy:lctes12,
author = {L\'eonard G\'erard and Adrien Guatto and
C\'edric Pasteur and Marc Pouzet},
title = {{A Modular Memory Optimization for Synchronous Data-Flow
Languages. Application to Arrays in a Lustre Compiler}},
booktitle = {Languages, Compilers and Tools for Embedded Systems
(LCTES'12)},
year = 2012,
address = {Beijing},
month = {June 12-13},
organization = {ACM},
abstract = {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 been only
addressed in a restricted manner. Yet, memory optimization becomes a
pressing issue when arrays are added to such languages.
This article presents a two-levels 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 \emph{in-place} modifications to be imported safely. 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 a less efficient code
but with the very same 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.},
note = {Best paper award},
url = {lctes12.pdf}
}
@inproceedings{lucy:emsoft12,
author = {Albert Cohen and L\'eonard G\'erard and Marc Pouzet},
title = {{Programming parallelism with futures in Lustre}},
booktitle = {ACM International Conference on Embedded Software (EMSOFT'12)},
year = 2012,
address = {Tampere, Finland},
organization = {ACM},
month = {October 7-12},
abstract = {Efficiently distributing synchronous programs is a challenging and
long-standing subject. This paper introduces the use
of \emph{futures} in a Lustre-like language, giving the programmer
control over the expression of parallelism. In the
synchronous model where computations are considered instantaneous,
futures increase expressiveness by decoupling the beginning from the
end of a computation.
Through a number of examples, we show how to desynchronize long
computations and implement parallel patterns such as fork-join,
pipelining and data parallelism. The proposed extension preserves
the main static properties of the base language, including
static resource bounds and the absence of deadlock, livelock and
races. Moreover, we prove that adding or removing futures preserves
the underlying synchronous semantics.},
note = {Best paper award},
url = {emsoft12.pdf}
}
@inproceedings{lucy:hscc13,
author = {Timothy Bourke and Marc Pouzet},
title = {{Z\'elus, a Synchronous Language with ODEs}},
booktitle = {International Conference on
Hybrid Systems: Computation and Control (HSCC 2013)},
year = 2013,
month = {April 8--11},
address = {Philadelphia, USA},
organization = {ACM},
abstract = {
Z\'elus is a new programming language for modeling systems that mix
discrete logical time and continuous time
behaviors. From a user's perspective, its main originality is to
extend an existing \lustre-like synchronous language with Ordinary
Differential Equations (ODEs). The extension is conservative: any
synchronous program expressed as data-flow equations and hierarchical
automata can be composed arbitrarily with ODEs in \emph{the same source
code}.
A dedicated type system and causality analysis ensure that all discrete
changes are aligned with
zero-crossing events so that no side effects or discontinuities occur
during integration. Programs are statically
scheduled and translated into sequential code which, by construction, runs
in bounded time and space.
Compilation is effected by source-to-source translation into a small
synchronous subset which is
processed by a standard synchronous compiler architecture.
The resulting code is paired with an off-the-shelf numeric solver.
This experiment show that it is possible to build a modeler for
explicit hybrid systems \emph{\`a la Simulink/Stateflow} on top of an
existing synchronous language, using it both as a semantic basis and as a
target for code generation.},
url = {hscc13.pdf}
}
@unpublished{rml:simulation06,
author = {Farid Benbadis and Louis Mandel and Marc Pouzet
and Ludovic Samper},
title = {{Simulation of Ad hoc Networks in ReactiveML}},
note = {Submitted to journal publication},
year = 2007,
month = {Feb},
url = {simulator-ad-hoc-networks06.pdf},
abstract = {This paper presents a programming experiment of complex network
routing protocols for mobile ad hoc networks within the reactive
language ReactiveML.
Mobile ad hoc networks are highly dynamic networks characterized by
the absence of physical infrastructure. In such networks, nodes are
able to move, evolve concurrently and synchronize continuously with
their neighbors. Due to mobility, connections in the network can
change dynamically and nodes can be added or removed at any time. All
these characteristics~---~concurrency with many communications and the
need of complex data-structure~---~combined to our routing protocol
specifications make the use of standard simulation tools ({\it e.g.},
NS-2, OPNET) inadequate. Moreover network protocols appear to be very
hard to program efficiently in conventional programming languages.
In this paper, we show that the {\em synchronous reactive model} as
introduced in the pioneering work of Boussinot matters for programming
such systems. This model provides adequate programming constructs ---
namely synchronous parallel composition, broadcast communication and
dynamic creation --- which allow a natural implementation of the hard
part of the simulation. This thesis is supported by two concrete
examples: the first example is a routing protocol in mobile ad hoc
networks and the simulation focuses only on the network layer. The
second one is a routing protocol for sensors networks and the wholes
layers are faithfully simulated (hardware, MAC and network
layers). More importantly, the physical environment (e.g., clouds) has
also been integrated into the simulation using the tool Lucky.
The implementation has been done in ReactiveML, an embedding of the reactive
model inside a statically typed, strict functional language. ReactiveML
provides reactive programming constructs together with most of the
features of Ocaml. Moreover, it provides an efficient execution
scheme for reactive constructs which made the simulation of real-size
examples (with several thousand of nodes) feasible.}
}
@inproceedings{rml:glonemo06,
author = {Ludovic Samper and Florence Maraninchi and
Laurent Mounier and Louis Mandel},
title = {{GLONEMO}: Global and Accurate Formal Models for the
Analysis of Ad-Hoc Sensor Networks},
booktitle = {Proceedings of the First International
Conference on Integrated Internet Ad hoc and Sensor Networks (InterSense'06)},
year = {2006},
address = {Nice, France},
month = may
}
@inproceedings{rml:jfla05,
author = {Louis Mandel et Marc Pouzet},
title = {{{ReactiveML},
un langage pour la programmation r\'eactive en ML}},
booktitle = {Journ\'ees Francophones des Langages Applicatifs (JFLA)},
year = 2005,
address = {Obernai, France},
month = {Mars},
publisher = {INRIA},
url = {jfla05.ps.gz},
abstract = {Nous pr\'esentons ReactiveML, un langage d\'edi\'e \`a la
programmation de syst\`emes r\'eactifs complexes tels que les
interfaces graphiques, les jeux vid\'eo ou les probl\`emes de
simulation. Le langage est bas\'e sur le mod\`ele \emph{r\'eactif
synchrone} introduit dans les ann\'ees 90 par Fr\'ed\'eric Boussinot.
Ce mod\`ele combine les principes du mod\`ele synchrone avec la
possibilit\'e de cr\'eer dynamiquement des processus.
ReactiveML est une extension conservative d'un langage ML avec
appel par valeur. Il ajoute des constructions suppl\'ementaires
pour d\'ecrire les comportements temporels des syst\`emes.
Nous illustrons l'expressivit\'e du langage sur des exemples et
donnons une s\'emantique formelle du noyau du langage. La
s\'emantique exprime les interactions entre les expressions ML
et les constructions r\'eactives. Le langage est statiquement
typ\'e avec un syst\`eme d'inf\'erence de type \`a la Milner.
}
}
@inproceedings{rml:mandel-slap05,
author = {Louis Mandel and Farid Benbadis},
title = {{Simulation of Mobile Ad-Hoc Networks in {ReactiveML}}},
booktitle = {{Synchronous Languages, Applications, and
Programming (SLAP)}},
editor = {Electronic Notes in Theoretical Computer Science},
year = 2005,
note = {available at \verb#www-spi.lip6.fr/~mandel/rml#},
url = {mandel-slap05.ps.gz},
abstract = {This paper presents a programming experiment of a complex
network routing protocol for mobile ad hoc networks within the ReactiveML
language.
Mobile ad hoc networks are highly dynamic networks characterized by
the absence of physical infrastructure. In such networks, nodes are
able to move, evolve concurrently and synchronize continuously with
their neighbors. Due to mobility, connections in the network can
change dynamically and nodes can be added or removed at any time. All
these characteristics~---~concurrency with many communications and the
need of complex data-structure~---~combined to our routing protocol
specifications make the use of standard simulation tools ({\it e.g.},
NS, OPNET) inadequate. Moreover network protocols appear to be very
hard to program efficiently in conventional programming languages.
In this paper, we show that the {\em synchronous reactive model}, as
introduced in the pioneering work of Boussinot, matters for
programming such systems. This model provides adequate programming
constructs --- namely synchronous parallel composition, broadcast
communication and dynamic creation --- which allow a natural
implementation of the hard part of the simulation.
The implementation has been done in ReactiveML, an embedding of the reactive
model inside a statically typed, strict functional language. ReactiveML
provides reactive programming constructs together with most of the features
of Ocaml. Moreover, it provides an efficient execution scheme for
reactive constructs which made the simulation of real-size examples
feasible. Experimental results show that the ReactiveML implementation is
two orders of magnitude faster than the original C version; it was
able to simulate more than 1000 nodes where the original C version
failed (after 200 nodes) and compares favorably with the version programmed
in NAB.}
}
@inproceedings{rml:ppdp05,
author = {Louis Mandel and Marc Pouzet},
title = {{ReactiveML, a Reactive Extension to ML}},
booktitle = {ACM International Conference
on Principles and Practice of Declarative Programming
(PPDP)},
year = 2005,
address = {Lisboa},
month = {July},
url = {ppdp05.pdf},
abstract = {We present ReactiveML, a programming language dedicated to the
implementation of complex reactive systems as found in graphical user
interfaces, video games or simulation problems. The language is based
on the {\em reactive} model introduced by Boussinot. This model
combines the so-called {\em synchronous} model found in Esterel
which provides instantaneous communication and parallel composition
with classical features found in asynchronous models like dynamic
creation of processes.
The language comes as a conservative extension of an existing
call-by-value ML language and it provides additional constructs for
describing the temporal part of a system.
The language receives a behavioral
semantics {\em \`a la} Esterel and a transition semantics describing
precisely the interaction between ML values and reactive
constructs. It is statically typed through a Milner type inference
system and programs are compiled into regular ML programs.
The language has been used for programming several complex simulation
problems (e.g., routing protocols in mobile ad-hoc
networks).}
}
@phdthesis{rml:these-mandel06,
author = {Louis Mandel},
title = {Conception, S{\'e}mantique et Implantation de {ReactiveML} : un langage {\`a} la {ML} pour la programmation r{\'e}active},
school = {Universit{\'e} Paris 6},
year = {2006}
}
@article{rml:tsi08,
author = {Louis Mandel and Marc Pouzet},
title = {{ReactiveML} : un langage fonctionnel pour
la programmation r{\'e}active},
journal = {Techniques et Sciences Informatiques (TSI)},
year = 2008,
url = {tsi08.pdf}
}
@inproceedings{rml:mandel-plateau-slap08,
author = {Louis Mandel and Florence Plateau},
title = {Interactive Programming of Reactive Systems},
booktitle = {Proceedings of Model-driven High-level Programming of Embedded Systems ({SLA++P'08})},
year = 2008,
month = apr,
address = {Budapest, Hungary},
url = {MandelPlateau-SLAP-2008.pdf}
}
@manual{rml:distribution,
title = {The ReactiveML distribution},
author = {Louis Mandel},
organization = {Universit\'e Paris-Sud 11},
note = {Available at: \texttt{rml.lri.fr}}
}
This file was generated by bibtex2html 1.96.