HDRs 2021

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.

Les assistants de preuve sont des logiciels conçus pour la réalisation de bibliothèques de mathématiques numérisées. Celles-ci contiennent des définitions, énoncés et preuves tous formalisés dans une variante de logique fixée, de sorte que la vérification de la bonne formation des énoncés, et la correction des preuves, puissent être réduites à un processus mécanique, celui associé au formalisme logique sous-jacent. Le noyau de l’assistant de preuve est le composant du logiciel qui réalise cette vérification, tandis que l’assistant de preuve à proprement parler implémente un ensemble de techniques d’automatisation qui permettent à ses utilisateurs de mener à bien la formalisation en pratique de définitions et de théories mathématiques arbitrairement sophistiquées. A ce jour, les assistants de preuves ont principalement été utilisés dans un contexte de vérification de programmes: compilation, programmation système, sécurité, etc. Le théorème à formaliser est alors celui qui spécifie le comportement attendu du programme. Cette spécification peut porter sur des aspects variés du comportement des programmes : correction fonctionnelle, gestion de la mémoire, arithmétique des ordinateurs, etc. Néanmoins, les assistants de preuve ont récemment attiré l’attention d’un nombre croissant de chercheurs en mathématiques, motivés par la vérification de preuves complexes, et non nécessairement calculatoires. La formalisation de ces dernières exige de l’assistant de preuve des formes d’automatisation essentiellement différentes de celles qui servent les besoins de la preuve de programme au sens large. Répondre à ces besoins, pour faciliter la vérification formelle de mathématiques à grande échelle, est un sujet de recherche actuel, qui est le cadre dans lequel se placent les travaux présentés ici. Ce mémoire présente une synthèse de trois contributions principales à la vérification formelle de théories mathématiques en théorie des types dépendants. La première de ces contributions porte sur la réalisation d’une bibliothèque de mathématiques formalisées couvrant les résultats classiques d’algèbre de niveau licence, ainsi que des pans plus avancés de théorie des groupes finis. Ces derniers culminent avec une formalisation du théorème de l’ordre impair (Feit-Thompson,1963). Il s’agit ici de mettre en perspective les différents ingrédients, de natures variées, qui permettent d’obtenir un corpus ample, cohérent, lisible, réutilisable, et facile à maintenir dans la durée. Ces ingrédients couvrent la conception d’un langage de tactiques, l’utilisation de techniques avancées d’inférence et d’unification, aussi bien que des techniques de formalisation, par exemple celles qui exploitent des schémas de réflexion. La deuxième contribution porte sur la vérification formelle du théorème d’Apéry, qui établit l’irrationalité de la constante ζ(3). Au delà de l’intérêt intrinsèque de la vérification formelle ce résultat, il s’agit ici de discuter la coopération de systèmes de preuves formelles avec des systèmes de calcul formel. La preuve vérifiée est en effet une preuve par calcul symbolique, dans laquelle des opérateurs de récurrence jouant un rôle crucial sont calculés par une bibliothèque de calcul formel. Les algorithmes qui produisent ces opérateurs fournissent également des données auxiliaires, des certificats, qui permettent une vérification efficace a posteriori de la correction des résultats produits. On discute ici la mise en œuvre de cette coopération, ainsi que ses limites. La troisième et dernière contribution porte sur la vérification formelle d’algorithmes de calcul numérique rigoureux, en particulier de quadratures réelles. Les algorithmes numériques dits rigoureux analysent précisément leur sources d’erreur (d’arrondi et de méthode), et calculent des bornes d’erreur explicites sur leurs résultats. Néanmoins, les conditions sous lesquelles ces calculs d’erreur sont corrects, typiquement une classe de régularité, sont difficiles `a tester statiquement sur les entrées fournies par l’utilisateur, ce qui est une source d’erreurs difficiles à détecter. Une implémentation formellement vérifiée permet de s’affranchir de ces erreurs. On discute ici deux approches d’implémentation de quadrature rigoureuse et formellement vérifiée, pour des fonctions réelles et des intégrales propres et impropres