En C, une stratégie classique pour implémenter les codes de gestion d'erreur est de faire suivre chaque opération qui peut générer une erreur d'une structure conditionnelle qui teste si l'opération a renvoyé une erreur. Ce stratégie basique, cependant, est sujette à erreurs, et il est courant d'oublier des opérations de nettoyage requises, ainsi que d'oublier de mettre à jour des codes de gestion d'erreur existants lorsque la fonction est étendue avec de nouvelles opérations. De plus, une partie importante du code doit souvent être dupliquée. Un style de programmation, <EM> stratégie goto </EM>, qui peut réduire en partie certaines de ces difficultés. Pour améliorer la structure des codes de gestion d'erreur dans les logiciels système, nous définissions un algorithme qui permet de transformer les codes de gestion d'erreur implémentés suivant la stratégie basique en codes de gestion d'erreur qui utilisent la <EM> stratégie goto</EM>. Même lorsque les codes de gestion d'erreurs sont structurés, la gestion et la libération des ressources allouées restent un problème lorsqu'il s'agit d'assurer la robustesse du code système. Dans cette thèse, nous proposons un algorithme <EM> microscopique </EM> de détection d'omission de libération de ressource, basé sur une analyse principalement intra-procédurale, qui prend en compte les flux et les chemins du code et qui cible et exploite les propriétés des codes de gestion d'erreur. Notre algorithme est résistant aux faux positifs dans l'ensemble des acquisitions de ressources et des opérations de libération, ce qui produit un faible taux de faux positifs dans les rapports renvoyés par l'outil tout en passant à l'échelle.

Les systèmes temps-réel critiques sont de plus en plus complexes, et les exigences fonctionnelles et non-fonctionnelles ne cessent plus de croître. Le flot de conception de tels systèmes doit assurer, parmi d’autres propriétés, le déterminisme fonctionnel et la prévisibilité temporelle. Le déterminisme fonctionnel est inhérent aux modèles de calcul flot de données (ex. KPN, SDF, etc.) ; c’est pour cela qu’ils sont largement utilisés pour modéliser les systèmes embarqués de traitement de flux. Un effort considérable a été accompli pour résoudre le problème d’ordonnancement statique périodique et à mémoire de communication bornée des graphes flot de données. Cependant, les systèmes embarqués temps-réel optent de plus en plus pour l’utilisation de systèmes d’exploitation temps-réel et de stratégies d’ordonnancement dynamique pour gérer les tâches et les ressources critiques. Cette thèse aborde le problème d’ordonnancement temps-réel dynamique des graphes flot de données ; ce problème consiste à assigner chaque acteur dans un graphe à une tâche temps-réel périodique (i.e. calcul des périodes, des phases, etc.) de façon à : (1) assurer l’ordonnançabilité des tâches sur une architecture et pour une stratégie d’ordonnancement (ex. RM, EDF) données ; (2) exclure statiquement les exceptions d’overflow et d’underflow sur les buffers de communication ; et (3) optimiser les performances du système (ex. maximisation du débit, minimisation des tailles des buffers). / The ever-increasing functional and nonfunctional requirements in real-time safety-critical embedded systems call for new design flows that solve the specification, validation, and synthesis problems. Ensuring key properties, such as functional determinism and temporal predictability, has been the main objective of many embedded system design models. Dataflow models of computation (such as KPN, SDF, CSDF, etc.) are widely used to model stream-based embedded systems due to their inherent functional determinism. Since the introduction of the (C)SDF model, a considerable effort has been made to solve the static-periodic scheduling problem. Ensuring boundedness and liveness is the essence of the proposed algorithms in addition to optimizing some nonfunctional performance metrics (e.g. buffer minimization, throughput maximization, etc.). However, nowadays real-time embedded systems are so complex that real-time operating systems are used to manage hardware resources and host real-time tasks. Most of real-time operating systems rely on priority-driven scheduling algorithms (e.g. RM, EDF, etc.) instead of static schedules which are inflexible and difficult to maintain. This thesis addresses the real-time scheduling problem of dataflow graph specifications; i.e. transformation of the dataflow specification to a set of independent real-time tasks w.r.t. a given priority-driven scheduling policy such that the following properties are satisfied: (1) channels are bounded and overflow/underflow-free; (2) the task set is schedulable on a given uniprocessor (or multiprocessor) architecture. This problem requires the synthesis of scheduling parameters (e.g. periods, priorities, processor allocation, etc.) and channel capacities. Furthermore, the thesis considers two performance optimization problems: buffer minimization and throughput maximization.

Le langage de programmation Python est aujourd'hui parmi les plus populaires au monde grâce à son accessibilité ainsi que l'existence d'un grand nombre de librairies standards. Paradoxalement, Python est également reconnu pour ses performances médiocres lors de l'exécution de nombreuses tâches. Ainsi, l'écriture d’implémentations efficaces du langage est nécessaire. Elle est toutefois freinée par la sémantique complexe de Python, ainsi que par l’absence de sémantique formelle officielle. Pour régler ce problème, nous présentons une sémantique formelle pour Python axée sur l’implémentation de compilateurs optimisants. Cette sémantique est écrite de manière à pouvoir être intégrée et analysée aisément par des compilateurs déjà existants. Nous introduisons également semPy, un évaluateur partiel de notre sémantique formelle. Celui-ci permet d'identifier et de retirer automatiquement certaines opérations redondantes dans la sémantique de Python. Ce faisant, semPy génère une sémantique naturellement plus performante lorsqu'exécutée. Nous terminons en présentant Zipi, un compilateur optimisant pour le langage Python développé avec l'assistance de semPy. Sur certaines tâches, Zipi offre des performances compétitionnant avec celle de PyPy, un compilateur Python reconnu pour ses bonnes performances. Ces résultats ouvrent la porte à des optimisations basées sur une évaluation partielle générant une implémentation spécialisée pour les cas d'usage fréquent du langage. / Python is among the most popular programming language in the world due to its accessibility and extensive standard library. Paradoxically, Python is also known for its poor performance on many tasks. Hence, more efficient implementations of the language are required. The development of such optimized implementations is nevertheless hampered by the complex semantics of Python and the lack of an official formal semantics. We address this issue by presenting a formal semantics for Python focussed on the development of optimizing compilers. This semantics is written as to be easily reusable by existing compilers. We also introduce semPy, a partial evaluator of our formal semantics. This tool allows to automatically target and remove redundant operations from the semantics of Python. As such, semPy generates a semantics which naturally executes more efficiently. Finally, we present Zipi, a Python optimizing compiler developped with the aid of semPy. On some tasks, Zipi displays performance competing with those of PyPy, a Python compiler known for its good performance. These results open the door to optimizations based on a partial evaluation technique which generates specialized implementations for frequent use cases.

Titre de l'écran-titre (visionné le 9 janvier 2024) / Les modèles hydrogéologiques permettent de décrire la réponse des systèmes aquifères soumis à différents forçages naturels et anthropiques, et peuvent donc être utilisés pour évaluer les éventuels effets néfastes associés à différentes stratégies de gestion de l'eau souterraine. Les variables simulées par les modèles sont intrinsèquement incertaines, et des analyses telles que l'estimation des paramètres, l'analyse quantitative des incertitudes et l'optimisation de gestion sous incertitude sont essentielles pour fournir des informations quantitatives robustes pour appuyer la prise de décision des gestionnaires de l'eau souterraine. Cependant, ces analyses sont rarement effectuées dans les modèles d'écoulement d'eau souterraine simulant l'intrusion saline, à cause des temps de calculs très longs des modèles simulant le transport advectif-dispersif. L'objectif de cette recherche était de fournir des cadres méthodologiques pour la mise en place de ces analyses dans les modèles opérationnels régionaux simulant l'intrusion saline. Des méthodologies reproductibles ont ainsi été développées pour l'estimation des paramètres, l'analyse quantitative des incertitudes et l'optimisation des pompages sous incertitude à l'aide de modèles d'intrusion saline dits à « interface abrupte », qui ne simulent pas explicitement les phénomènes de dispersion hydrodynamique. Des approches déterministes puis stochastiques ont été développées, prenant en compte l'incertitude dans les paramètres du modèle, l'incertitude dans les observations utilisées pour contraindre l'estimation des paramètres, et finalement l'incertitude climatique. Des méthodes ont été développées pour extraire des observations de charge d'eau douce équivalente et d'interface eau douce-eau salée de différents types de puits et de la géophysique, et pour estimer leurs incertitudes. Une analyse a posteriori a déterminé quels types d'observations étaient essentiels pour réduire les incertitudes prédictives du modèle, pour guider de futures collectes de données dans les aquifères insulaires ou côtiers. Une méthodologie a également été développée pour optimiser les pompages dans une lentille d'eau douce insulaire avec un modèle à interface abrupte, en corrigeant l'interface par une solution analytique pour estimer de manière simplifiée la dispersion d'eau salée liée au pompage. Toutes les méthodologies développées ont utilisé des logiciels d'écoulement de l'eau souterraine (MODLOW-SWI2) et des outils d'aide à la décision (PEST_HP, PEST++, PyEMU) libres et facilement accessibles. Ces méthodes ont été intégralement développées sous la forme de scripts Python pour faciliter leur reprise dans d'autres projets de modélisation hydrogéologique. Les résultats démontrent les avantages liés à la mise en place d'outils d'aide à la décision dans les modèles numériques d'écoulement de l'eau souterraine. L'optimisation des pompages sous incertitude permet d'obtenir le débit de pompage maximal en fonction du risque de salinisation (à comparer à la demande en eau); cette approche permet aux gestionnaires de l'eau souterraine de choisir le scénario souhaité en fonction de leur degré de tolérance au risque. L'estimation des paramètres permet de réduire les incertitudes prédictives du modèle, ce qui influence directement les débits de pompage optimaux. La prise en compte de l'incertitude climatique augmente l'incertitude prédictive du modèle et réduit les débits de pompages optimaux pour les gestionnaires ayant une attitude conservatrice face au risque. Cette recherche était motivée par des problématiques concrètes de gestion de l'eau souterraine aux Iles de la Madeleine (Québec, Canada), et les méthodologies mises en place pourraient être utilisées pour appuyer la prise de décision des gestionnaires de l'eau souterraine dans d'autres milieux côtiers ou insulaires. / Numerical models enable the assessment of a groundwater system's response to various natural processes and human activities, and thus can be used to evaluate whether a management strategy could lead to adverse effects. Model predictions are not exact predictions of the behavior of natural systems, and the implementation of analyses such as parameter estimation, uncertainty quantification and management optimization under uncertainty are therefore critical to support groundwater management. However, they are rarely implemented in seawater intrusion numerical models, due to the prohibitive model simulation times of advective-dispersive solute transport models. The objective of this research was to provide a framework for the implementation of these decision-support analyses in real-world seawater intrusion models at regional scales. Highly-reproducible, scripted methodologies were developed for parameter estimation, uncertainty quantification and pumping optimization under uncertainty using computationally-efficient sharp-interface models, which do not explicitly simulate hydrodynamic dispersion. Both deterministic and stochastic, ensemble-based approaches were implemented, accounting for parameter and observation uncertainty as well as climate uncertainty. Methodologies were developed for the processing and uncertainty quantification of freshwater heads and freshwater-seawater interface elevations from different types of wells and geophysical data. A data worth analysis provided insights on future data collection strategies in coastal or island aquifers, and found that interface observations, particularly geophysical observations, were most useful to reduce model predictive uncertainties. A methodology was also developed to optimize pumping rates in a sharp-interface model of an island freshwater lens, using an analytical correction for dispersion to overcome the limitations of the sharp-interface model. All the methodologies developed used widely available groundwater flow software (MODFLOW-SWI2) and decision-support tools (PEST, PEST_HP, PEST++, PyEMU), and were entirely scripted using Python to facilitate their adoption by the wider groundwater modeling community. The results collectively demonstrate the benefits of implementing decision-support analyses in groundwater numerical models. Pumping optimization under uncertainty enabled the quantification of the optimal tradeoff between increasing pumping rates (to meet the water demand) and the risk of well salinization, which allows groundwater managers to select their preferred management scenario depending on the level of risk that they consider to be acceptable. Conducting history matching enabled a reduction of model predictive uncertainty, which directly impacted the maximum allowable pumping rates. Accounting for climate uncertainty led to increased model predictive uncertainty and a reduction of the maximum allowable pumping rates for managers with a risk-averse stance. This research was motivated by real-world groundwater management challenges in the Magdalen Islands (Québec, Canada), and the methodologies that were developed could be used to support decision-making in other coastal or island aquifers.

Nous nous intéressons dans ce manuscrit au langage ReactiveML, qui est une extension de ML avec des constructions inspirées des langages synchrones. L'idée de ces langages est de diviser l'exécution d'un programme en une suite d'instants logiques discrets. Cela permet de proposer un modèle de concurrence déterministe que l'on peut compiler vers du code séquentiel impératif. La principale application de ReactiveML est la simulation discrète, par exemple de réseaux de capteurs. Nous cherchons ici à programmer des simulations à grande échelle, ce qui pose deux questions : sait-on les programmer de façon simple et modulaire ? sait-on ensuite exécuter ces programmes efficacement ? Nous répondons à la première question en proposant une extension du modèle synchrone appelée domaines réactifs. Elle permet de créer des instants locaux invisibles de l'extérieur. Cela rend possible le raffinement temporel, c'est-à-dire le remplacement d'une approximation d'un système par une version plus détaillée sans changer son comportement externe. Nous développons dans ce manuscrit la sémantique formelle de cette construction ainsi que plusieurs analyses statiques, sous forme de systèmes de types-et-effets, garantissant la sûreté des programmes dans le langage étendu. Enfin, nous montrons également plusieurs implémentations parallèles du langage pour tenter de répondre à la question du passage à l'échelle des simulations. Nous décrivons tout d'abord une implémentation avec threads communiquant par mémoire partagée et basée sur le vol de tâches, puis une seconde implémentation utilisant des processus lourds communiquant par envoi de messages.

Cette thèse présente un algorithme qui élimine les racines carrées et les divi- sions dans des programmes sans boucles, utilisés dans des systèmes embarqués, tout en préservant la sémantique. L'élimination de ces opérations permet d'éviter les erreurs d'arrondis à l'exécution, ces erreurs d'arrondis pouvant entraîner un comportement complètement inattendu de la part du programme. Cette trans- formation respecte les contraintes du code embarqué, en particulier la nécessité pour le programme produit de s'exécuter en mémoire fixe. Cette transformation utilise deux algorithmes fondamentaux développés dans cette thèse. Le premier permet d'éliminer les racines carrées et les divisions des expressions booléennes contenant des comparaisons d'expressions arithmétiques. Le second est un algo- rithme qui résout un problème d'anti-unification particulier, que nous appelons anti-unification contrainte. Cette transformation de programme est définie et prou- vée dans l'assistant de preuves PVS. Elle est aussi implantée comme une stratégie de ce système. L'anti-unification contrainte est aussi utilisée pour étendre la transformation à des programmes contenant des fonctions. Elle permet ainsi d'éliminer les racines carrées et les divisions de spécifications écrites en PVS. La robustesse de cette méthode est mise en valeur par un exemple conséquent: l'élimination des racines carrées et des divisions dans un programme de détection des conflits aériens.

La spécificité des logiciels scientifiques développés par IFP Energies nouvelles tient avant tout à l'originalité des modèles représentant les situations physiques exprimés sous forme de systèmes d'EDPs assortis de lois de fermeture complexes. Le développement de ces logiciels, conçus pour être exécutés sur les super calculateurs parallèles modernes, nécessite de combiner des méthodes volumes finis robustes et efficaces avec des technologies informatiques qui permettent de tirer au mieux parti de ces calculateurs (parallélisme, gestion de la mémoire, réseaux d'interconnexion, etc). Ces technologies de plus en plus sophistiquées ne peuvent plus être maîtrisées dans leur ensemble par les chercheurs métiers chargés d'implémenter des nouveaux modèles. Dans ce rapport nous proposons un langage spécifique aux méthodes de discrétisation Volumes Finis permettant le prototypage rapide de codes industriels ou de recherche. Nous décrivons le cadre mathématique sur lequel nous nous basons ainsi que la mise au point du nouveau langage. Les travaux out été validés sur des problèmes académiques puis par le prototypage d'une application industrielle dans le cadre de l'axe ''CO2 maîtrisé''.

In this thesis, we present a Thread-Level Speculation (TLS) framework whose main feature is to speculatively parallelize a sequential loop nest in various ways, to maximize performance. We perform code transformations by applying the polyhedral model that we adapted for speculative and runtime code parallelization. For this purpose, we designed a parallel code pattern which is patched by our runtime system according to the profiling information collected on some execution samples. We show on several benchmarks that our framework yields good performance on codes which could not be handled efficiently by previously proposed TLS systems.

Concevoir et implanter des programmes parallèles est une tâche complexe, sujette aux erreurs. La vérification des programmes parallèles est également plus difficile que celle des programmes séquentiels. Pour permettre le développement et la preuve de correction de programmes parallèles, nous proposons de combiner le langage parallèle fonctionnel quasi-synchrone BSML, les squelettes algorithmiques - qui sont des fonctions d'ordre supérieur sur des structures de données réparties offrant une abstraction du parallélisme - et l'assistant de preuve Coq, dont le langage de spécification est suffisamment riche pour écrire des programmes fonctionnels purs et leurs propriétés. Nous proposons un plongement des primitives BSML dans la logique de Coq sous une forme modulaire adaptée à l'extraction de programmes. Ainsi, nous pouvons écrire dans Coq des programmes BSML, raisonner dessus, puis les extraire et les exécuter en parallèle. Pour faciliter le raisonnement sur ceux-ci, nous formalisons le lien entre programmes parallèles, manipulant des structures de données distribuées, et les spécifications, manipulant des structures séquentielles. Nous prouvons ainsi la correction d'une implantation du squelette algorithmique BH, un squelette adapté au traitement de listes réparties dans le modèle de parallélisme quasi synchrone. Pour un ensemble d'applications partant d'une spécification d'un problème sous forme d'un programme séquentiel simple, nous dérivons une instance de nos squelettes, puis nous extrayons un programme BSML avant de l'exécuter sur des machines parallèles.

Ce travail porte sur la compilation des langages de programmation logique par contraintes sur les domaines finis (DF). Plutôt que d'adopter l'approche usuelle considérant le résolveur comme une boîte noire nous avons choisi l'approche boîte de verre de P. Van Hentenryck. Dans celle-ci, le résolveur gère une seule contrainte primitive. Toutes les contraintes complexes (équations, contraintes symboliques...) sont traduites en des appels de contraintes primitives. Le résolveur est ainsi simple et homogène. De plus, l'utilisateur peut définir ses propres contraintes en termes de cette primitive. Cette primitive nous permet de définir une machine abstraite pour la compilation des contraintes DF. En outre, le traitement d'une seule primitive permet de définir des optimisations globales dont bénéficient toutes les contraintes de haut niveau. Toutes ces idées sont détaillées et aboutissent à la définition du langage clp (FD). L'étude des performances de clp (FD) montre que cette approche est très efficace, meilleure en tous cas que les résolveurs boîtes noires. Nous étudions également les aptitudes de clp (FD) à résoudre des contraintes booléennes car elles sont un cas particulier des DF. Là encore clp (FD) se compare très bien avec des résolveurs spécialisés. Nous nous intéressons enfin à la détection de la satisfaction des contraintes pour permettre à l'utilisateur de spécifier des calculs dirigés par les données (plutôt que par les instructions). Ce travail débouche donc tout naturellement sur l'implantation des langages concurrents.