Limusyn source code (Prelude with clock views)
A real-time system is a system whose correctness depends not only on the correctness of the values it produces, but also on the time when it produces those values. The rate at which it must produce values is defined by the environment it operates in.
When programming such a system, it is important that the programming language allows to reason about the constraints introduced by this context. Synchronous languages are well-adapted to the programming of critical real-time systems thanks to their clean formal semantics and to their formally defined compilation process. In this work, we will present extensions to the synchronous language Prelude to tackle two issues: Programming multicore systems predictably and handling system reconfiguration during execution.
Multicore hardware platforms have the potential to increase the performance of real-time systems. However, their architecture, especially the shared central memory, is prone to hard-to-predict delays, outweighing the potential benefits. To address this issue, models such as PREM and AER have been proposed. Our first contribution aims at producing AER-compliant multicore C code from a high-level Prelude program. This shifts the responsibility of low-level implementation concerns related to task communications onto the compiler, saving tedious and error-prone development efforts.
A multi-mode real-time system must respect different functional requirements during its execution. A mode of execution represents a possible system configurations, for an aircraft control system these may include take-off, cruise and landing. Mode change protocols define transitions to change safely from one mode to another. Our second contribution proposes clock views to decouple the rate of tasks and transitions. The resulting multi-mode support is both formally defined and generic enough to allows programmers to choose the kind of protocol they need for their application. A clock calculus based on refinement typing~ infers and checks the consistency of rates and views.