This thesis addresses the design and implementationof a programming language for real-time streaming applications,such as video decoding. The model of Kahnprocess networks is a natural fit for this area and hasbeen used extensively. In this model, a program consistsin a set of parallel processes communicating via singlereader, single writer queues. The strength of the modellies in its determinism.Synchronous functional languages such as Lustre arededicated to critical embedded systems. A Lustre programdefines a synchronous Kahn process network, thatis, which can be executed using finite queues and withoutdeadlocks. This is enforced by a dedicated type system,the clock calculus, which establishes a global timescale throughout a program. The global time scale isused to define clocks: per-queue boolean sequences indicating,for each time step, whether a process producesor consumes a token in the queue. This information isused both for enforcing synchrony and for generatingfinite-state software or hardware.We propose and study integer clocks, a generalizationof boolean clocks featuring arbitrarily big natural numbers.Integer clocks model the production or consumptionof several values from the same queue in the courseof a time step. We then rely on integer clocks to definethe local time scale construction, which may hide timesteps performed by a sub-program from the surroundingcontext.These principles are integrated into a clock calculus fora higher-order functional language. We study its properties,proving among other results that well-typed programsdo not deadlock. We adjust the clock-directedcode generation scheme of Lustre to generate finite-statedigital synchronous circuits from typed programs. Thetyping information controls certain trade-offs betweentime and space in the generated circuits.
分享
引用
