Clock analysis of synchronous dataflow programs
Thomas Wiben Jensen · 1995
Synchronous dataflow languages such as Lustre and Signal have been proposed as a tool for programming reactive systems. These languages rely on a clock analysis to ensure that synchronous operations receive their arguments at the same time. We present a denotational model of a Lustre-like dataflow language and show how a range of clock analyses for this language can be designed and proved correct. To the best of our knowledge this is the first formal correctness proof for such an analysis. We then give a type system formulation of this analysis using clocks as types and show how adding polymorphic clocks enables us to treat programs where clocks vary according to their context. The relationship to the clock analysis by constraint solving used in the language Signal is discussed. 1 Introduction One of the earliest models of concurrent computation is Kahn's networks of processes [Kah74, KM77]. Such a network consists of a set of deterministic processes, or agents, communicating in an ...