The internship will start by studying Ipanema, a domain-specific language to define schedulers of processes, and the caracteristics for process scheduling on a multicore system. Ipanema is based on Bossa, a language allowing to write safe user-defined scheduling policies on single core systems.
The goal of the project is to propose some modifications of the Ipanema language associated with the static or dynamic semantics to allow verification of some critical properties, like starvation, process handling, and core state handling.
The first step is to study the current language constructs that allow both to handle multicore systems and to verify some critical properties. The intern will study the verification of these properties, and idealy propose an algorithm to statically determine if the user-specified scheduling policy is safe, or not, for these properties. If the current language lacks some features, the intern will have to propose new language construct.
The current version of Ipanema is based on an Linux 4.9 kernel. The second step of this project is to work on the C generator to allow proof-of-concept of the proposed constructs, and running live experiments.