Lucy-n: a n-Synchronous Extension of Lustre
MPC 2010
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