Lucy-n: a n-Synchronous Extension of Lustre MPC 2010

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.

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 stream equals its 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 a sub-typing rule 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