Synchronous Thread Management in a Distributed Operating System's Micro Kernel

This paper describes an experiment in programming part of an operating system kernel using the Esterel synchronous programming language. Using a synchronous programming language allows the construction of provable, deterministic reactive systems. The paper describes and analyzes the small executive realized and the formal verification of some of its properties. It also presents how multiple interconnected instances of this executive can be synchronized, yielding a distributed real-time platform operating under a sparse-time model. Key Words : Synchronous programming, distributed systems, thread management, real-time systems, deterministic system