Abstraction of Clocks in Synchronous Data-flow Systems -
APLAS 2008
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
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.
Article: .pdf
Long version:
.pdf
Slides: .pdf
This document was translated from LATEX by
HEVEA.