Synchronization of Periodic Clocks

%HEVEA\publinkCDEPPP05.ps.gzInternational audienceWe propose a programming model dedicated to real-time videostreamingapplications for embedded media devices, including highdefinitionTVs. This model is built on the synchronous programmingmodel extended with domain-specific knowledge — periodic evolutionof streams — to allow correct-by-construction properties of theapplication to be proven by the compiler. These properties includebuffer requirements and delays between input and output streams.Such properties are tedious to analyze by hand, due to the combinatoricsof video filters, multiple data rates and formats. We show howto extend a core synchronous data-flow language with a notion of periodicclocks, and to design a relaxed clock calculus (a type systemfor clocks) to allow non strictly synchronous processes to be composed.This relaxation is associated with a subtyping rule in the clockcalculus. Delay, buffer insertion and control code for these buffersare automatically inferred from the clock types through a systematicprogram transformation