Study of the COQ Proof Assistant, application to Real-time scheduling

Advisor Joël Goossens
Keywords RTOS, scheduling, Automatic proof

Description

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.

References

  • Coq@Inria
  • Cerqueira, Felipe, Felix Stutz, and Björn B. Brandenburg. “PROSA: A Case for Readable Mechanized Schedulability Analysis” 28th Euromicro Conference on Real-Time Systems (ECRTS), 2016. PDF

Heterogeneous Embedded Real-Time Systems

Advisor Joël Goossens
Mentor Ph.D. student Antonio Paolillo
Keywords RTOS, heterogeneous platforms, FPGA, scheduling

Description

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.

References

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

Description

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 [1], RUN [2] and U-EDF [3]. However, such algorithms are more complex than traditional ones.

References

  • 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