Ce manuscrit s'inscrit dans le domaine du calcul intensif (HPC) où le besoin croissant de performance pousse les fabricants de processeurs à y intégrer des mécanismes de plus en plus sophistiqués. Cette complexité grandissante rend l'utilisation des architectures compliquée. La modélisation des performances des architectures multi-cœurs permet de remonter des informations aux utilisateurs, c'est à dire les programmeurs, afin de mieux exploiter le matériel. Cependant, du fait du manque de documentation et de la complexité des processeurs modernes, cette modélisation est souvent difficile. L'objectif de ce manuscrit est d'utiliser des mesures de performances de petits fragments de codes afin de palier le manque d'information sur le matériel. Ces expériences, appelées micro-benchmarks, permettent de comprendre les performances des architectures modernes sans dépendre de la disponibilité des documentations techniques. Le premier chapitre présente l'architecture matérielle des processeurs modernes et, en particulier, les caractéristiques rendant la modélisation des performances complexe. Le deuxième chapitre présente une méthodologie automatique pour mesurer les performances des instructions arithmétiques. Les informations trouvées par cette méthode sont la base pour des modèles de calculs permettant de prédire le temps de calcul de fragments de codes arithmétique. Ce chapitre présent également comment de tels modèles peuvent être utilisés pour optimiser l'efficacité énergétique, en prenant pour exemple le processeur SCC. La dernière partie de ce chapitre motive le fait de réaliser un modèle mémoire prenant en compte la cohérence de cache pour prédire le temps d'accès au données. Le troisième chapitre présente l'environnement de développement de micro-benchmark utilisé pour caractériser les hiérarchies mémoires dotées de cohérence de cache. Ce chapitre fait également une étude comparative des performances mémoire de différentes architectures et l'impact sur les performances du choix du protocole de cohérence. Enfin, le quatrième chapitre présente un modèle mémoire permettant la prédiction du temps d'accès aux données pour des applications régulières de type \openmp. Le modèle s'appuie sur l'état des données dans le protocole de cohérence. Cet état évolue au fil de l'exécution du programme en fonction des accès à la mémoire. Pour chaque transition, une fonction de coût est associée. Cette fonction est directement dérivée des résultats des expériences faites dans le troisième chapitre, et permet de prédire le temps d'accès à la mémoire. Une preuve de concept de la fiabilité de ce modèle est faite, d'une part sur les applications d'algèbre et d'analyse numérique, d'autre part en utilisant ce modèle pour modéliser les performance des communications \mpi en mémoire partagée.

Ce mémoire, a pour objet de présenter une synthèse de mes travaux de recherche et de les mettre en perspective avec l'objectif général de la conception et du développement d'un environnement logiciel pour la modélisation et la simulation. Ils sont présentés selon trois axes thématiques : - bien modéliser pour mieux simuler, - calculer efficacement, précisément et juste, - générer un code de calcul dédié. Un dernier chapitre, plus technique, présente les contours et les fonctionnalités de cet environnement logiciel intégré pour la modélisation et la simulation, dont la conception a été le cadre général et le fil conducteur de l'essentiel de mes travaux.

Cette thèse développe une nouvelle méthodologie permettant d'établir des approximations analytiques pour les prix des options européennes. Notre approche combine astucieusement des développements stochastiques et le calcul de Malliavin afin d'obtenir des formules explicites et des évaluations d'erreur précises. L'intérêt de ces formules réside dans leur temps de calcul qui est aussi rapide que celui de la formule de Black et Scholes. Notre motivation vient du besoin croissant de calculs et de procédures de calibration en temps réel, tout en contrôlant les erreurs numériques reliées aux paramètres du modèle. On traite ainsi quatre catégories de modèles, en réalisant des paramétrisations spécifiques pour chaque modèle afin de mieux cibler le bon modèle proxy et obtenir ainsi des termes correctifs faciles à évaluer. Les quatre parties traitées sont : les diffusions avec sauts, les volatilités locales ou modèles à la Dupire, les volatilités stochastiques et finalement les modèles hybrides (taux-action). Il faut signaler aussi que notre erreur d'approximation est exprimée en fonction de tous les paramètres du modèle en question et est analysée aussi en fonction de la régularité du payoff.

L'objectif de cette thèse est de développer une théorie de types pour le λ-calcul linéaire-algébrique, une extension du λ-calcul motivé par l'informatique quantique. Cette extension algébrique comprend tous les termes du λ-calcul plus leurs combinaisons linéaires, donc si t et r sont des termes, α.t+β.r est aussi un terme, avec α et β des scalaires pris dans un anneau. L'idée principale et le défi de cette thèse était d'introduire un système de types où les types, de la même façon que les termes, constituent un espace vectoriel, permettant la mise en évidence de la structure de la forme normale d'un terme. Cette thèse présente le système Lineal , ainsi que trois systèmes intermédiaires, également intéressants en eux-même : Scalar, Additive et λCA, chacun avec leurs preuves de préservation de type et de normalisation forte.

Non renseigné

L'utilisation massive des plateformes multi-cœurs et multi-processeurs a pour effet de favoriser la programmation parallèle à mémoire partagée. Néanmoins, exploiter efficacement et de manière correcte le parallélisme sur ces plateformes reste un problème de recherche ouvert. De plus, leur modèle d'exécution sous-jacent, et notamment les modèles de mémoire "relâchés", posent de nouveaux défis pour les outils d'analyse statiques et dynamiques. Dans cette thèse nous abordons deux aspects importants dans le cadre de la programmation sur plateformes multi-cœurs et multi-processeurs: l'optimisation de sections critiques implémentées selon l'approche pessimiste, et l'analyse dynamique de flots d'informations. Les sections critiques définissent un ensemble d'accès mémoire qui doivent être exécutées de façon atomique. Leur implémentation pessimiste repose sur l'acquisition et le relâchement de mécanismes de synchronisation, tels que les verrous, en début et en fin de sections critiques. Nous présentons un algorithme générique pour l'acquisition/relâchement des mécanismes de synchronisation, et nous définissons sur cet algorithme un ensemble de politiques particulier ayant pour objectif d'augmenter le parallélisme en réduisant le temps de possession des verrous par les différentes threads. Nous montrons alors la correction de ces politiques (respect de l'atomicité et absence de blocages), et nous validons expérimentalement leur intérêt. Le deuxième point abordé est l'analyse dynamique de flot d'information pour des exécutions parallèles. Dans ce type d'analyse, l'enjeu est de définir précisément l'ordre dans lequel les accès à des mémoires partagées peuvent avoir lieu à l'exécution. La plupart des travaux existant sur ce thème se basent sur une exécution sérialisée du programme cible. Ceci permet d'obtenir une sérialisation explicite des accès mémoire mais entraîne un surcoût en temps d'exécution et ignore l'effet des modèles mémoire relâchées. A contrario, la technique que nous proposons permet de prédire l'ensemble des sérialisations possibles vis-a-vis de ce modèle mémoire à partir d'une seule exécution parallèle ("runtime prediction"). Nous avons développé cette approche dans le cadre de l'analyse de teinte, qui est largement utilisée en détection de vulnérabilités. Pour améliorer la précision de cette analyse nous prenons également en compte la sémantique des primitives de synchronisation qui réduisent le nombre de sérialisations valides. Les travaux proposé ont été implémentés dans des outils prototype qui ont permit leur évaluation sur des exemples représentatifs.

Le concept de réversibilité est ancien, mais il soulève de nos jours beaucoup d'intérêt. Il est en effet exploité dans de nombreux domaines tels que la conception de circuits, le débogage et le test de programmes, la simulation et l'informatique quantique. L'idée d'un modèle de programmation réversible peut se montrer particulièrement intéressante pour la construction de systèmes sûrs de fonctionnement, ne serait-ce que parce que plusieurs techniques connues pour la construction de tels systèmes exploitent une forme ou une autre de retour en arrière ou de reprise. Nous poursuivons dans cette thèse l'étude entreprise avec CCS réversible par Vincent Danos et Jean Krivine, en définissant un pi-calcul d'ordre supérieur réversible (rhopi). Nous prouvons que le modèle obtenu est causalement cohérent, et que l'on peut encoder fidèlement rhopi dans une variante du pi-calcul d'ordre supérieur. Nous définissons également une primitive de reprise à grain fin qui permet de contrôler le retour en arrière dans une exécution concurrente. Nous spécifions formellement la sémantique de cette primitive, et nous montrons qu'elle possède de bonnes propriétés, y compris en présence d'opérations de reprise concurrentes. Enfin nous définissons un algorithme concurrent implantant cette primitive de reprise et ous montrons que cet algorithme respecte la sémantique définie.

Depuis les années 50 sont apparues, comme domaine d'étude, ce que l'on appelle les sciences cognitives, qui ont fédéré des disciplines telles que, entre autres, la neurobiologie, la psychologie, la philosophie, la linguistique... et bien entendu l'informatique. Sans revenir sur l'historique de la constitution des sciences cognitives, nous en retiendrons qu'elles sont apparues à partir du moment o'u les sciences sont devenues capables d'aborder la question de la conscience, en décortiquant et objectivant les phénomènes de mémoire, de perception, de langage et d'émotions. Objectiver le sujet, qui est au cœur des sciences cognitives, est l'expression d'un paradoxe dont nous parlerons dans ce chapitre, et la science informatique y a pris toute sa part. L'Intelligence Artificielle (IA) a été le versant en informatique des sciences cognitives. Parler d'intelligence artificielle fait d'ailleurs toujours l'objet de polémiques, la question de savoir jusqu'où l'on peut dire qu'une machine est capable d'intelligence n'étant pas tranchée aujourd'hui. Face à cette indétermination, nous soutiendrons l'hypothèse dite de l'IA forte, qui propose de considérer que l'ensemble de ce que l'on peut observer chez l'homme en termes de langage, pensée, conscience, est strictement le fruit de son métabolisme, neuronal en particulier. Nous ne demanderons pas au lecteur d'adhérer à cette hypothèse, mais soulignons ici qu'elle motive les travaux et les orientations de recherches que nous présentons dans ce mémoire. L'hypothèse d'IA forte trouve un écho particulier en informatique pour les raisons suivantes. L'informatique est une discipline qui dès l'origine [Turing, 1936; Church, 1936] a su abstraire la mécanique du traitement de l'information de son support. En effet, les machines de Turing ont existé bien avant d'être instanciées sur support physique. Selon cette perspective, qu'un traitement soit effectué sur silicium, au sein d'une clepsydre améliorée, ou sur un support neuronal ne change rien à l'affaire. La métaphore de la chambre chinoise de John Searle [Searle, 1980] illustre cette indépendance au support. Elle compare l'ordinateur à une personne enfermée dans une salle qui manipule des symboles chinois auxquels elle ne comprend rien, suivant pour ce faire un système de règles. Si l'on adhère à l'hypothèse d'IA forte, ce que ne fait pas Searle, le système de règles pourrait décrire une intelligence, équivalente à celle de l'Homme, dont l'opérateur est le moteur. Ce qui motive notre recherche informatique est l'hypothèse de l'existence de ces règles, autrement dit, d'un programme qui conduise 'a ce qu'une intelligence de même nature que celle de l'Homme puisse être instanciée par une machine de Turing. Faire cette hypothèse, toutefois, ne permet pas de guider la conception du programme, ou plutôt d'un programme, qui puisse doter une machine d'intelligence. Il est alors nécessaire de trouver ailleurs les arguments permettant de concevoir ces programmes. Là encore, l'hypothèse d'IA forte joue un rôle central. Si on admet que l'intelligence dont l'Homme fait preuve n'est que le résultat de la mécanique de ses neurones, il devient pertinent de s'inspirer des neurones 1Chapitre 1. Préambule pour concevoir un programme intelligent. L'argument ici n'est pas de dire que la voie neuromimétique est la seule qui puisse permettre de concevoir des machines intelligentes, mais plutôt de souligner que, sous l'hypothèse d'IA forte, cette voie permettra d'aboutir. En plus de cette garantie de succès, toute théorique car rien ne dit que la technologie permettra d'instancier ces machines, l'inspiration des neurones a un autre avantage pour l'informatique, qui se défend sans recourir à l'hypothèse d'IA forte. En effet, qu'ils suffisent ou non à rendre compte de l'intelligence, les mécanismes neuronaux qui s'expriment au sein du système nerveux sont un exemple de traitement de l'information de nature foncièrement différente de ceux conçus par les approches classiques de génie logiciel. L'étude de ces systèmes est alors susceptible d'apporter à l'informatique des paradigmes nouveaux, et c'est ce que nous défendons le plus ardemment dans nos travaux de recherche. L'ensemble de ce chapitre consiste 'a préciser ces quelques lignes d'introduction, en abordant le talon d'Achille des sciences cognitives, 'a savoir la question de la définition de l'intelligence. Nous abordons ensuite la question de la pluridisciplinarité, saisie du point de vue de l'informatique, pour défendre l'apport des sciences dites " molles " à notre discipline. Nous nous trouvons en effet dans la situation où un recours aux sciences humaines et sociales peut être défendu comme une aide pour débloquer les difficultés que rencontrent des sciences pourtant " dures " lorsqu'elles abordent la question de l'intelligence.

Le déploiement reste l'une des étapes du cycle de vie des logiciels la moins standardisée et outillée à ce jour. Dans ce travail, nous identifions quatre grands défis à relever pour dé- ployer des systèmes logiciels distribués et hétérogènes. Le premier défi est de réussir à initier le consensus manquant autour d'un langage générique de déploiement de logiciels. Le deuxième défi consiste en la vérification statique de déploiements logiciels décrits dans ce langage pour assurer un déroulement correct avant d'exécuter les opérations de déploiement. Le troisième défi est de réaliser une plate-forme intergicielle capable d'interpréter ce langage et d'effectuer le déploiement de n'importe quel système logiciel réparti. Enfin le quatrième défi est d'appli- quer ces déploiements de systèmes dans les environnements ouverts distribués, c'est-à-dire les réseaux fluctuants et à grande échelle comme les réseaux ubiquitaires ou les grilles de calcul. Notre contribution consiste à définir une démarche de déploiement de systèmes distribués cen- trée sur quatre rôles pour relever ces défis : l'expert réseau, l'expert logiciel, l'administrateur système et l'architecte métier. D'un côté, l'approche DeployWare, conforme à l'ingénierie des modèles, est définie par un méta-modèle multi-rôles pour décrire le déploiement de la couche intergicielle du système ainsi que par une machine virtuelle capable d'exécuter automatique- ment le déploiement de cette couche. L'utilisation d'un langage de méta-modélisation permet d'écrire des programmes de vérification statique des modèles de déploiement. De l'autre côté, l'approche DACAR propose un méta-modèle d'architecture générique pour exprimer et exé- cuter le déploiement d'une application métier à base de composants. Cette double approche DeployWare/DACAR permet de prendre en compte, lors de la description du déploiement, les propriétés des environnements ouverts distribués selon une approche conforme à l'informatique auto-gérée. Notre contribution est validée par plusieurs expériences pour valider la capacité de prise en charge des environnements ouverts ubiquitaires, et pour éprouver l'hétérogénéité des technologies déployables dans le monde des services d'entreprise.

Cette thèse traite de problématique de dimensionnement d'un système technique complexe. L'objectif est de proposer et d'outiller un processus de conception selon lequel le dimensionnement statique de l'architecture initiale d'un système satisfait dès le début les exigences statiques et dynamiques sans nécessité de redimensionnement. Ainsi, nous avons proposé une nouvelle démarche de conception dans laquelle la prise en compte des exigences statiques et dynamiques est effectuée de maniéré simultanée et globale dans la phase de conception préliminaire. Cette démarche se base sur les exigences pour déterminer les solutions admissibles et utilise des méthodes de résolution ensemblistes telles que la méthode de calcul par intervalle et la méthode de propagation par contraintes. En effet, les variables de conception sont exprimées par intervalles et les exigences statiques et dynamiques sont implémentées dans un même modèle NCSP. Les exigences dynamiques sont plus difficiles à intégrer. Il s'agit des exigences fonctionnelles du système, de la résonance et des critères de stabilité, de commandabilité et de transmittance. Dans un premier temps, nous avons réussi à intégrer le comportement dynamique d'un système technique sous forme d'équation différentielle ordinaire par intervalles et dans un deuxième temps, nous avons traduit les exigences dynamiques sous forme de contraintes algébriques définies par un ensemble d'équations et inéquations. La solution générée représente les valeurs admissibles des variables de conception satisfaisant simultanément les exigences statiques et dynamiques imposées. Ce couplage entre le dimensionnement statique et dynamique dans l'approche de conception proposée permet d'éviter le sur-dimensionnement puisque les exigences dynamiques interviennent dans le choix des coefficients de sécurité, et d'éviter les boucles de redimensionnement en cas d'échec ce qui permet de gagner en temps de calcul et de réduire le coût de conception. La démarche de conception proposée est validée par application sur le cas de dimensionnement d'un système de suspension active MacPherson.