Cette thèse s'inscrit dans la démarche de preuve de programmes à l'aide de vérification déductive. La vérification déductive consiste à produire, à partir des sources d'un programme, c'est-à-dire ce qu'il fait, et de sa spécification, c'est-à-dire ce qu'il est sensé faire, une conjecture qui si elle est vraie alors le programme et sa spécification concordent. On utilise principalement des démonstrateurs automatiques pour montrer la validité de ces formules. Quand ons'intéresse à la preuve de programmes qui utilisent des structures de données allouées en mémoire, il est élégant et efficace de spécifier son programme en utilisant la logique de séparation qui est apparu il y a une dizaine d'année. Cela implique de prouver des conjectures comportant les connectives de la logique de séparation, or les démonstrateurs automatiques ont surtout fait des progrès dans la logique du premier ordre qui ne les contient pas.Ce travail de thèse propose des techniques pour que les idées de la logique de séparation puissent apparaître dans les spécifications tout en conservant la possibilité d'utiliser des démonstrateurs pour la logique du premier ordre. Cependant les conjectures que l'ont produit ne sont pas dans la même logique du premier ordre que celles des démonstrateurs. Pour permettre une plus grande automatisation, ce travail de thèse a également défini de nouvelles conversions entre la logique polymorphe du premier ordre et la logique multi-sortée dupremier ordre utilisé par la plupart des démonstrateurs.La première partie a donné lieu à une implémentation dans l'outil Jessie, la seconde a donné lieu à une participation conséquente à l'écriture de l'outil Why3 et particulièrement dans l'architecture et écriture des transformations qui implémentent ces simplifications et conversions. / This thesis comes within the domain of proofs of programs by deductive verification. The deductive verification generates from a program source and its specification a mathematical formula whose validity proves that the program follows its specification. The program source describes what the program does and its specification represents what the program should do. The validity of the formula is mainly verified by automatic provers. During the last ten years separation logic has shown to be an elegant way to deal with programs which use data-structures with pointers. However it requires a specific logical language, provers, and specific reasoning techniques.This thesis introduces a technique to express ideas from separation logic in the traditional framework of deductive verification. Unfortunately the mathematical formulas produced are not in the same first-order logic than the ones of provers. Thus this work defines new conversions between the polymorphic first-order logic and the many-sorted logic used by most proves.The first part of this thesis leads to an implementation in the Jessietool. The second part results in an important participation to the writing of the Why3 tool, in particular in the architecture and writing of the transformations which implement these conversions.

No description available.

No description available.

No description available.

Les rejets urbains par temps de pluie entraînent des dégradations importantes dans les milieux récepteurs où ils sont rejetés sans traitement préalable. Parmi les campagnes de mesure françaises, effectuées depuis les années 70 à l'exutoire de bassins séparatifs ou unitaires, 17 d'entre elles ont été sélectionnées pour être intégrées dans la base de données constituée au CERGRENE avec l'aide financière de l'Agence de l'Eau Seine-Normandie. Son exploitation a pour objectifs de caractériser la pollution rejetée par temps de pluie (évaluation de masses annuellement rejetées, identification des caractéristiques des événements pluvieux les mieux reliées aux concentrations et aux masses par événement, description des événements les plus pollués, répartition de la masse en cours d'écoulement) et de fournir des éléments sur les dimensions des ouvrages de traitement. Il a fallu tout d'abord reconstituer les caractéristiques des événements pluvieux qui manquaient (volume écoulé, concentration moyenne ou masse produite). Pour cela, des équations de régression ont été établies site par site. Les ajustements obtenus ne sont pas tous de bonne qualité, à cause du nombre réduit de mesures disponibles ou du type des événements utilisés. Quand ils ne sont pas représentatifs de l'ensemble des événements de la campagne, la fiabilité des équations n'est pas assurée et leur domaine d'application ne contient pas tous les événements. Les masses annuelles ont pu être évaluées pour chaque site grâce aux reconstitutions précédentes. L'emploi des équations de régression a permis d'établir des intervalles de confiance autour des valeurs. Ces intervalles sont souvent très larges, et le nombre de sites est assez restreint. Par conséquent, la seule relation qui apparaît est celle qui est la plus évidente et qui existe entre les masses annuelles et les surfaces des sites. Concernant la répartition des masses de pollution en cours d'écoulement, leur forme est très variable d'un événement à un autre, sur un site donné. En moyenne, la pollution contenue dans la première partie de l'écoulement est légèrement supérieure à celle de la deuxième partie. Il y a néanmoins un nombre non négligeable d'événements pour lesquels la majeure partie de la masse de pollution est rejetée en fin d'écoulement. Lorsqu'on compare les sites, la pollution contenue dans les premiers flots (dans 20% de l'écoulement) varie sur les sites unitaires dans des intervalles qui sont les mêmes que sur les sites séparatifs. Pour traiter les rejets urbains de temps de pluie, des ouvrages de décantation (par stockage ou par traitement au fil de l'eau) sont reconnus être des outils efficaces. Nous avons calculé la masse interceptée par des ouvrages fictifs en faisant varier leurs dimensions (respectivement volume de stockage ou débit de traitement suivant le type d'ouvrage). Les reconstitutions utilisées conduisent à des intervalles de confiance très larges. Les résultats dépendent de la période de retour des événements pluvieux qui ont été utilisés. En première approximation, pour intercepter 80% de la masse produite sur une durée d'environ un an, il faut des volumes de l'ordre de 100 m3/ha act ou des débits de l'ordre de 10 1/s/ha act. Pour préciser ces chiffres, il faudrait disposer de longues séries d'événement de plusieurs années. Il serait alors possible en fonction de l'objectif (par exemple intercepter l'événement dont la période de retour est fixée ou intercepter la pollution rejetée pendant une année de pluviométrie moyenne) d'indiquer quelle dimension est la plus efficace.

L'objectif de ce travail est de modéliser le comportement hydro-mécanique de massifs rocheux fissurés. Ceci concerne précisément l'amélioration et l'extension d'un modèle par éléments discrets appelé BRIG3D. Ce modèle assimile un massif rocheux fissuré à un assemblage de blocs rigides qui interagissent au niveau de leurs interfaces. La déformation de ces interfaces est reliée aux déplacements relatifs des blocs. Sous l'effet des sollicitations du massif, chaque bloc, en interaction avec d'autres, se déplace vers une position d'équilibre. Les améliorations concernent la reformulation mécanique de BRIG3D. De nouvelles descriptions concernant le mouvement d'un corps rigide, la position des interfaces et le champ des contraintes sont introduites. Ce travail de recherche concerne également l'introduction d'un modèle par éléments frontières décrivant un écoulement laminaire, permanent et plan aux interfaces des blocs. Le couplage de ces deux modèles à permis d'analyser le comportement hydro-mécanique de massifs rocheux fissurés soumis à diverses sollicitations. Une étude particulière a été consacrée à l'analyse du comportement d'une fondation de barrage.

Dans le domaine du génie chimique, les ingénieurs tracent des courbes pour analyser les données recueillies. Une fois validée, cette connaissance est exploitée, en combinaison avec d'autres savoirs, sous forme de tâches. Cette thèse présente une architecture capable d'enchaîner n'importe quel type de tâches et de visualiser des courbes, appliquée à un problème d'aide à la conception de procédé de raffinage. L'architecture proposée repose sur une analyse objets des raisonnements, où figurent les notions de relations (inversibles ou non) et de flux du point de vue statique, de problèmes et de tâches du point de vue dynamique. Le module de visualisation exploite toutes les sortes de relations entre les variables et s'appuie sur des méthodes élaborées de tracé, dont deux sont nouvelles : la première s'inspire d'exemples a priori comme dans le raisonnement à base de cas, la seconde utilise les notions de monotonie et de concavité pour déduire des lignes dans un ensemble de points. L'application est exposée dans le détail et conduit à une analyse des problèmes de conception, et nous avons développé notamment une nouvelle classification de ces systèmes.

Dans les systèmes informatiques, la consommation énergétique est devenue le facteur le plus limitant de la croissance de performance observée pendant les décennies précédentes. Conséquemment, les paradigmes d'architectures d'ordinateur et de développement logiciel doivent changer si nous voulons éviter une stagnation de la performance durant les décennies à venir.Dans ce nouveau scénario, des nouveaux designs architecturaux et micro-architecturaux peuvent offrir des possibilités d'améliorer l'efficacité énergétique des ordinateurs, grâce à la spécialisation matérielle, comme par exemple les configurations de cœurs hétérogènes, des nouvelles unités de calcul et des accélérateurs. D'autre part, avec cette nouvelle tendance, le développement logiciel devra faire face au manque de portabilité de la performance entre les matériels toujours en évolution et à l'écart croissant entre la performance exploitée par les programmeurs et la performance maximale exploitable du matériel. Pour traiter ce problème, la contribution de cette thèse est une méthodologie et la preuve de concept d'un cadriciel d'auto-tuning à la volée pour les systèmes embarqués. Le cadriciel proposé peut à la fois adapter du code à une micro-architecture inconnue avant la compilation et explorer des possibilités d'auto-tuning qui dépendent des données d'entrée d'un programme.Dans le but d'étudier la capacité de l'approche proposée à adapter du code à des différentes configurations micro-architecturales, j'ai développé un cadriciel de simulation de processeurs hétérogènes ARM avec exécution dans l'ordre ou dans le désordre, basé sur les simulateurs gem5 et McPAT. Les expérimentations de validation ont démontré en moyenne des erreurs absolues temporels autour de 7 % comparé aux ARM Cortex-A8 et A9, et une estimation relative d'énergie et de performance à 6 % près pour le benchmark Dhrystone 2.1 comparée à des CPUs Cortex-A7 et A15 (big.LITTLE). Les résultats de validation temporelle montrent que gem5 est beaucoup plus précis que les simulateurs similaires existants, dont les erreurs moyennes sont supérieures à 15 %.Un composant important du cadriciel d'auto-tuning à la volée proposé est un outil de génération dynamique de code, appelé deGoal. Il définit un langage dédié dynamique et bas-niveau pour les noyaux de calcul. Pendant cette thèse, j'ai porté deGoal au jeu d'instructions ARM Thumb-2 et créé des nouvelles fonctionnalités pour l'auto-tuning à la volée. Une validation préliminaire dans des processeurs ARM ont montré que deGoal peut en moyenne générer du code machine avec une qualité équivalente ou supérieure comparé aux programmes de référence écrits en C, et même par rapport à du code vectorisé à la main.La méthodologie et la preuve de concept de l'auto-tuning à la volée dans des processeurs embarqués ont été développées autour de deux applications basées sur noyau de calcul, extraits de la suite de benchmark PARSEC 3.0 et de sa version vectorisée à la main PARVEC.Dans l'application favorable, des accélérations de 1.26 et de 1.38 ont été observées sur des cœurs réels et simulés, respectivement, jusqu'à 1.79 et 2.53 (toutes les surcharges dynamiques incluses).J'ai aussi montré par la simulation que l'auto-tuning à la volée d'instructions SIMD aux cœurs d'exécution dans l'ordre peut surpasser le code de référence vectorisé exécuté par des cœurs d'exécution dans le désordre similaires, avec une accélération moyenne de 1.03 et une amélioration de l'efficacité énergétique de 39 %.L'application défavorable a été choisie pour montrer que l'approche proposée a une surcharge négligeable lorsque des versions de noyau plus performantes ne peuvent pas être trouvées.En faisant tourner les deux applications sur les processeurs réels, la performance de l'auto-tuning à la volée est en moyenne seulement 6 % en dessous de la performance obtenue par la meilleure implémentation de noyau trouvée statiquement. / In computing systems, energy consumption is limiting the performance growth experienced in the last decades. Consequently, computer architecture and software development paradigms will have to change if we want to avoid a performance stagnation in the next decades.In this new scenario, new architectural and micro-architectural designs can offer the possibility to increase the energy efficiency of hardware, thanks to hardware specialization, such as heterogeneous configurations of cores, new computing units and accelerators. On the other hand, with this new trend, software development should cope with the lack of performance portability to ever changing hardware and with the increasing gap between the performance that programmers can extract and the maximum achievable performance of the hardware. To address this issue, this thesis contributes by proposing a methodology and proof of concept of a run-time auto-tuning framework for embedded systems. The proposed framework can both adapt code to a micro-architecture unknown prior compilation and explore auto-tuning possibilities that are input-dependent.In order to study the capability of the proposed approach to adapt code to different micro-architectural configurations, I developed a simulation framework of heterogeneous in-order and out-of-order ARM cores. Validation experiments demonstrated average absolute timing errors around 7 % when compared to real ARM Cortex-A8 and A9, and relative energy/performance estimations within 6 % for the Dhrystone 2.1 benchmark when compared to Cortex-A7 and A15 (big.LITTLE) CPUs.An important component of the run-time auto-tuning framework is a run-time code generation tool, called deGoal. It defines a low-level dynamic DSL for computing kernels. During this thesis, I ported deGoal to the ARM Thumb-2 ISA and added new features for run-time auto-tuning. A preliminary validation in ARM processors showed that deGoal can in average generate equivalent or higher quality machine code compared to programs written in C, including manually vectorized codes.The methodology and proof of concept of run-time auto-tuning in embedded processors were developed around two kernel-based applications, extracted from the PARSEC 3.0 suite and its hand vectorized version PARVEC. In the favorable application, average speedups of 1.26 and 1.38 were obtained in real and simulated cores, respectively, going up to 1.79 and 2.53 (all run-time overheads included). I also demonstrated through simulations that run-time auto-tuning of SIMD instructions to in-order cores can outperform the reference vectorized code run in similar out-of-order cores, with an average speedup of 1.03 and energy efficiency improvement of 39 %. The unfavorable application was chosen to show that the proposed approach has negligible overheads when better kernel versions can not be found. When both applications run in real hardware, the run-time auto-tuning performance is in average only 6 % way from the performance obtained by the best statically found kernel implementations.

L’évolution des notions juridiques de vie privée et de données personnelles. A l’inverse de la littérature foisonnante sur le thème de la surveillance, il ne s’agit pas ici de mettre en avant la nécessité de trouver un équilibre entre la surveillance entendue dans sa dimension sécuritaire et la protection de la vie privée et des données personnelles, en ce qu’elle constitue une liberté fondamentale reconnue par les institutions françaises et européennes. Cette recherche d’une balance équilibrée entre sécurité et liberté doit nécessairement être dépassée pour comprendre le phénomène de surveillance diffuse. La surveillance n’est plus la simple activité de recherche de renseignements concernant un individu potentiellement dangereux. Elle s’inscrit plutôt dans la poursuite de ceque Hannah Arendt qualifie de « crise de la culture ». La surveillance diffuse est même l’une des caractéristiques de la culture contemporaine dominée par la peur, la consommation et l’aliénation par les technologies. Devenue la nouvelle norme sociale admise, la surveillance diffuse désinstitue le droit des données personnelles et la protection de la vie privée. Progressivement, elle désinstitue également le Droit au profit du libéralisme économique qu’elle porte en son sein. / The purpose of this research is to understand how diffuse surveillance fits into the evolution of legal concepts of privacy and personal data. Contrary to the abundant literature on the subject of surveillance, it is not a questionhere of highlighting the need to find a balance between surveillance in its security dimension and the protection of privacy and data, as a fundamental freedom recognized by French and European institutions. This search for a balance between security and freedom must necessarily be overcome to understand the phenomenon of diffuse surveillance. Surveillance is no longer just a search for information about a potentially dangerous individual. Rather, it is a continuation of what Hannah Arendt calls the « crisis of culture ». Diffuse surveillance is even oneof the features of contemporary culture dominated by fear, consumption and alienation by technology. Having become the new accepted social norm, the diffuse surveillance deinstitutes the right of the personal data and the protection of the private life. Gradually, it also deinstitutes the Law to profit from the economic liberalism that it carries within it.

Comme la puissance de calcul des systèmes de calcul haute performance continue de croître, en utilisant un grand nombre de cœurs CPU ou d’unités de calcul spécialisées, les applications hautes performances destinées à la résolution des problèmes de très grande échelle sont de plus en plus sujettes à des pannes. En conséquence, la communauté de calcul haute performance a proposé de nombreuses contributions pour concevoir des applications tolérantes aux pannes. Cette étude porte sur une nouvelle classe d’algorithmes numériques de tolérance aux pannes au niveau de l’application qui ne nécessite pas de ressources supplémentaires, à savoir, des unités de calcul ou du temps de calcul additionnel, en l’absence de pannes. En supposant qu’un mécanisme distinct assure la détection des pannes, nous proposons des algorithmes numériques pour extraire des informations pertinentes à partir des données disponibles après une pannes. Après l’extraction de données, les données critiques manquantes sont régénérées grâce à des stratégies d’interpolation pour constituer des informations pertinentes pour redémarrer numériquement l’algorithme. Nous avons conçu ces méthodes appelées techniques d’Interpolation-restart pour des problèmes d’algèbre linéaire numérique tels que la résolution de systèmes linéaires ou des problèmes aux valeurs propres qui sont indispensables dans de nombreux noyaux scientifiques et applications d’ingénierie. La résolution de ces problèmes est souvent la partie dominante; en termes de temps de calcul, des applications scientifiques. Dans le cadre solveurs linéaires du sous-espace de Krylov, les entrées perdues de l’itération sont interpolées en utilisant les entrées disponibles sur les nœuds encore disponibles pour définir une nouvelle estimation de la solution initiale avant de redémarrer la méthode de Krylov. En particulier, nous considérons deux politiques d’interpolation qui préservent les propriétés numériques clés de solveurs linéaires bien connus, à savoir la décroissance monotone de la norme-A de l’erreur du gradient conjugué ou la décroissance monotone de la norme résiduelle de GMRES. Nous avons évalué l’impact du taux de pannes et l’impact de la quantité de données perdues sur la robustesse des stratégies de résilience conçues. Les expériences ont montré que nos stratégies numériques sont robustes même en présence de grandes fréquences de pannes, et de perte de grand volume de données. Dans le but de concevoir des solveurs résilients de résolution de problèmes aux valeurs propres, nous avons modifié les stratégies d’interpolation conçues pour les systèmes linéaires. Nous avons revisité les méthodes itératives de l’état de l’art pour la résolution des problèmes de valeurs propres creux à la lumière des stratégies d’Interpolation-restart. Pour chaque méthode considérée, nous avons adapté les stratégies d’Interpolation-restart pour régénérer autant d’informations spectrale que possible. Afin d’évaluer la performance de nos stratégies numériques, nous avons considéré un solveur parallèle hybride (direct/itérative) pleinement fonctionnel nommé MaPHyS pour la résolution des systèmes linéaires creux, et nous proposons des solutions numériques pour concevoir une version tolérante aux pannes du solveur. Le solveur étant hybride, nous nous concentrons dans cette étude sur l’étape de résolution itérative, qui est souvent l’étape dominante dans la pratique. Les solutions numériques proposées comportent deux volets. A chaque fois que cela est possible, nous exploitons la redondance de données entre les processus du solveur pour effectuer une régénération exacte des données en faisant des copies astucieuses dans les processus. D’autre part, les données perdues qui ne sont plus disponibles sur aucun processus sont régénérées grâce à un mécanisme d’interpolation. / As the computational power of high performance computing (HPC) systems continues to increase by using huge number of cores or specialized processing units, HPC applications are increasingly prone to faults. This study covers a new class of numerical fault tolerance algorithms at application level that does not require extra resources, i.e., computational unit or computing time, when no fault occurs. Assuming that a separate mechanism ensures fault detection, we propose numerical algorithms to extract relevant information from available data after a fault. After data extraction, well chosen part of missing data is regenerated through interpolation strategies to constitute meaningful inputs to numerically restart the algorithm. We have designed these methods called Interpolation-restart techniques for numerical linear algebra problems such as the solution of linear systems or eigen-problems that are the inner most numerical kernels in many scientific and engineering applications and also often ones of the most time consuming parts. In the framework of Krylov subspace linear solvers the lost entries of the iterate are interpolated using the available entries on the still alive nodes to define a new initial guess before restarting the Krylov method. In particular, we consider two interpolation policies that preserve key numerical properties of well-known linear solvers, namely the monotony decrease of the A-norm of the error of the conjugate gradient or the residual norm decrease of GMRES. We assess the impact of the fault rate and the amount of lost data on the robustness of the resulting linear solvers.For eigensolvers, we revisited state-of-the-art methods for solving large sparse eigenvalue problems namely the Arnoldi methods, subspace iteration methods and the Jacobi-Davidson method, in the light of Interpolation-restart strategies. For each considered eigensolver, we adapted the Interpolation-restart strategies to regenerate as much spectral information as possible. Through intensive experiments, we illustrate the qualitative numerical behavior of the resulting schemes when the number of faults and the amount of lost data are varied; and we demonstrate that they exhibit a numerical robustness close to that of fault-free calculations. In order to assess the efficiency of our numerical strategies, we have consideredan actual fully-featured parallel sparse hybrid (direct/iterative) linear solver, MaPHyS, and we proposed numerical remedies to design a resilient version of the solver. The solver being hybrid, we focus in this study on the iterative solution step, which is often the dominant step in practice. The numerical remedies we propose are twofold. Whenever possible, we exploit the natural data redundancy between processes from the solver toperform an exact recovery through clever copies over processes. Otherwise, data that has been lost and is not available anymore on any process is recovered through Interpolationrestart strategies. These numerical remedies have been implemented in the MaPHyS parallel solver so that we can assess their efficiency on a large number of processing units (up to 12; 288 CPU cores) for solving large-scale real-life problems.