Lucy-n: a n-Synchronous Extension of Lustre

in*Tenth International Conference on Mathematics
of Program Construction*
(MPC 2010)

Louis Mandel, Florence Plateau and Marc Pouzet

LRI, Univ. Paris-Sud 11.

in

Louis Mandel, Florence Plateau and Marc Pouzet

LRI, Univ. Paris-Sud 11.

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. This synchronous restriction is obtained by associating a clock to every expression and relying on a dedicated type system — the clock calculus — to check that the actual clock of a streamequalsits expected clock and thus does not need to be buffered. 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 asub-typingrule which defines points where a buffer should be inserted.

This paper presents an implementation of the n-synchronous model inside a Lustre-like language called Lucy-n. The use of the language is illustrated on various examples including a video application. The clock calculus of Lucy-n is defined as an inference type system and is parametrized by the algorithm used to solve sub-typing constraints. We detail here one of those algorithms based on clock abstraction. A first way to abstract clocks has been presented in [APLAS08]. We consider in this paper an improved version of the abstract domain, whose correctness properties have been proved in Coq.

Article: .pdf

Lucy-n: lucync (clock typing prototype - bytecode OCaml version 3.10.2 - needs Glpk)

Coq proofs: .html