Home » HDRs

HDRs 2021

  Audrey Queudet, Synchronisation et Autonomie énergétique des Systèmes temps réel embarqués
Synchronisation et Autonomie énergétique des Systèmes temps réel embarqués
Author : Audrey Queudet
Document :

Keywords : Real-time systemDynamic real-time schedulingEnergy autonomySoftware transactional memoryMulticore synchronizationReal-time systemsDynamic real-time schedulingEnergy autonomySoftware transactional memoryMulticore synchronization

The work presented in this document addresses two main research concerns: (i) the synchronization of multicore real-time applications, and (ii) the energy autonomy of embedded real-time systems. These problems are approached from a scheduling point of view by taking into account several types of constraints: temporal constraints, resource sharing constraints, quality of service (QoS) constraints, and energy constraints. Efficiently managing concurrent memory access in a multicore real-time context is complex. Systematic locking can reduce the parallelism of the execution platform and thus lead to a significant performance loss. Based on this observation, we have studied the adaptation of transactional memories (non-blocking synchronization mechanisms) to multicore real-time systems. Through an experimental study, we compared the performance of several transactional memories in order to determine the key factors (e.g. operating system, scheduling policy, memory allocator) impacting the execution jitter of transactions, jitter that can directly impact the respect of the temporal constraints of tasks in a real-time system. We then proposed a hard real-time software transactional memory, called STM-HRT, which guarantees the progress of all transactions in the system. A functional and temporal analysis of the STM-HRT allowed us to validate the proposed non-blocking synchronization mechanism. New generation embedded systems such as wireless sensor nodes have been proliferating in recent years. For many of these systems, energy autonomy is a key issue. The technology of energy harvesting, which consists of capturing energy from the environment to power a system, makes it possible in particular to provide these resource-constrained embedded systems with the capacity for energy self-sufficiency. The intelligence embedded in these systems has very often real-time requirements in terms of software processing. It is then necessary to guarantee the perpetual operation of the system by jointly managing two types of constraints: time and energy. This is precisely the purpose of our contributions on this topic, by considering the problem from the point of view of the scheduling of tasks on the processor. We first highlighted the inefficiency of “classical” real-time schedulers such as EDF, which are unable to cope with fluctuations in the supply energy. However, we have shown that it remains the best non-idling scheduler in the context of energy harvesting and that it is the best choice of integration for a system that cannot have a predictive estimate of the exploitable energy. Our work then consisted in identifying some key properties of a scheduler in the energy harvesting context. Then, we contributed to the problem of the feasibility of a set hard real-time tasks in this same context, by proposing a new test which is robust with respect to the power of the energy source. The contributions presented right after aim at providing solutions adapted to situations of transient processing and/or energy consumption overload that a system may suffer from. Based on a new task model integrating QoS constraints, we have proposed new schedulers controlling in particular the number and identity of task jobs skipped in case of overload. Finally, we proposed a necessary feasibility test integrating both QoS and energy constraints.

Defense date : 07-06-2021
Jury president : Maryline Chetto
Jury :
  • Daniel Chillet [Rapporteur]
  • Laurent George [Rapporteur]
  • Pascal Richard [Rapporteur]
  • Alfons Crespo
  • Liliana Cucu-Grosjean

  Assia Mahboubi, Machine-checked computer-aided mathematics
Machine-checked computer-aided mathematics
Author : Assia Mahboubi
Document :

Keywords : Computer algebraType theoryFormal proofs

Defense date : 05-01-2021
Jury president : Yves Bertot(Yves.Bertot@inria.fr)
Jury :

    Copyright : LS2N 2017 - Legal notices -