Study of the COQ Proof Assistant, application to Real-time scheduling
Advisor Joël Goossens
Keywords RTOS, scheduling, Automatic proof
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, or the Bedrock verified low-level programming library), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching. Citation https://coq.inria.fr/
The student will study the COQ tool and language. Then the student will illustrate how to use that tool in the framework real-time scheduling properties using example based upon real-time literature.
Heterogeneous Embedded Real-Time Systems
Advisor Joël Goossens
Mentor Ph.D. student Antonio Paolillo
Keywords RTOS, heterogeneous platforms, FPGA, scheduling
Today, MPSoC platforms integrate many components heterogeneous in nature. For example, the Zynq platform contains a symmetric multi-core CPU that can run software tasks supported by a RTOS micro-kernel but can also delegate work to a customisable circuitry area (FPGA). This is a common technique to implement image processing applications on embedded systems: it is energy efficient and it has low execution time overheads. However, the underlying software system supporting real-time applications and driving these powerful heterogeneous embedded platforms must provide a secure and efficient layer of resource management: CPU time control, multi-core process scheduling, task parallelism, memory management and low-power execution are key techniques to efficiently handle the limited set of resources available for the execution of these embedded systems.
The goal of the master's thesis is to study:
- How to integrate FPGA-based algorithms into real-time operating system tasks or services (for a micro-kernel architecture).
- The impact of these heterogeneous components on scheduling analysis.
- How to model FPGA resources and the tasks driving these resources (e.g. model the driver task with self-suspension blocking time).
The master's thesis will contain a deep practical part as the student will develop several use cases (with image processing applications as basis) on an actual RTOS to validate theoretical studies (from the state of the art or the student's original idea) with practical system implementations. The use cases will be deployed and tested on an embedded development board with a MPSoC platform such as the Zynq. To do so, he will receive guidance from the HIPPEROS kernel development team (http://hipperos.com/).
The analysis will take into account performance criteria such as timing overheads, energy efficiency and/or thermal aspects.
The Zynq System-on-Chip: https://en.wikipedia.org/wiki/Xilinx#Zynq
Towards Real-Time Operating Systems for Heterogeneous Reconfigurable Platforms - Marco Pagani, Mauro Marinoni, Alessandro Biondi, Alessio Balsini, Giorgio Buttazzo. http://www.cs.hs-rm.de/~kaiser/events/ospert16/pdf/ospert16-p5.pdf
A Framework for Supporting Real-Time Applications on Dynamic Reconfigurable FPGAs - Alessandro Biondi, Alessio Balsini, Marco Pagani, Enrico Rossi, Mauro Marinoni and Giorgio Buttazzo
Rate-monotonic scheduling on uniform multiprocessors - Baruah and Goossens Partitioned EDF scheduling on a few types of unrelated multiprocessors - Wiese, Bonifaci and Baruah
A New Configurable and Parallel Embedded Real-time Micro-Kernel for Multi-core platforms - Antonio Paolillo, Olivier Desenfans, Vladimir Svoboda, Joël Goossens and Ben Rodriguez: https://www.mpi-sws.org/~bbb/events/ospert15/pdf/ospert15-p25.pdf
Quantifying Energy Consumption for Practical Fork-Join Parallelism on an Embedded Real-Time Operating System - Antonio Paolillo, Paul Rodriguez, Nikita Veshchikov, Joël Goossens and Ben Rodriguez: http://antonio.paolillo.be/publications/conferences/rtns16_paolillo_paper.pdf
Implementing a Dynamic and Global Scheduling Algorithm in a Real-Time OS
Advisor Joël Goossens
Mentor Ph.D. student Paul Rodriguez
Keywords RTOS, scheduling
The problem of scheduling multiple tasks on multiple processors and multi-core platforms has been widely studied by the real-time scheduling community in recent years. The traditional (and industry standard) approach to this problem is to split the set of tasks into partitions and schedule each partition on each processor independently. However, this approach leads to wasted processor time due to the impossibility of balancing load perfectly between all partitions. Wasted cpu cycles leads to platform over-provisioning and therefore additional costs for all kinds of devices in which multi-processor scheduling is necessary.
By contrast, global scheduling techniques allow processes to be preempted on one processor and re-scheduled on another processor. This range of techniques offers potentially greater efficiency than the widely used partitioned techniques. A number of interesting algorithms for the global scheduling problem have been proposed, such as DP-Wrap , RUN  and U-EDF . However, such algorithms are more complex than traditional ones.
Greg Levin, Shelby Funk, Caitlin Sadowski, Ian Pye, and Scott Brandt. DP-FAIR: A simple model for understanding optimal multiprocessor scheduling. 22nd Euromicro Conference on Real-Time Systems (ECRTS), pp. 3-13, IEEE, 2010.
Paul Regnier, George Lima, Ernesto Massa, Greg Levin, and Scott Brandt. RUN: Optimal multiprocessor real-time scheduling via reduction to uniprocessor. 32nd Real-Time Systems Symposium (RTSS), pp. 104-115, IEEE, 2011.
Geoffrey Nelissen, Vandy Berten, Vincent Nélis, Joël Goossens, and Dragomir Milojevic. U-EDF: An unfair but optimal multiprocessor scheduling algorithm for sporadic tasks. 24th Euromicro Conference on Real-Time Systems (ECRTS), pp. 13-23, IEEE, 2012.
Antonio Paolillo, Olivier Desenfans, Vladimir Svoboda, Joël Goossens, and Ben Rodriguez. A new configurable and parallel embedded real-time micro-kernel for multi-core platforms. OSPERT, 2015.
The HIPPEROS Real-Time Operating System: https://www.mpi-sws.org/~bbb/events/ospert15/pdf/ospert15-p25.pdf