Abstraction et formalisation en théorie des jeux.

  • By: Stéphane Le Roux
  • Number: PhD2008-01
  • Date: January 2008
  • Abstract:  Strategic games are a fundamental class of games in game theory: the notion of Nash equilibrium was first defined for this class. One may wonder whether or not every strategic game has a Nash equilibrium, but this is not the case. Furthermore, there seems to be no simple characterisation of the strategic games that actually have a Nash equilibrium. At least two ways to cope with this issue can be found in the literature: First, one defines a subclass (up to embedding) of strategic games, namely sequential games; then one defines the stronger notion of subgame perfect equilibrium as a refinement of Nash equilibrium for this subclass; finally, one proves that every sequential game has a subgame perfect equilibrium. That is how Kuhn proved that every sequential game has a Nash equilibrium. Second, one weakens the notion of Nash equilibrium, for instance by using probabilities. That is how Nash proved that every finite strategic game has a probabilistic Nash equilibrium.
    All this work was done for games involving payoffs that are real numbers, a few years after this restriction was consciously made and justified by von Neumann and Morgenstern who also considered abstract payoffs without further studying them. Due to great success of the real-number restriction, it soon became a principle for most of the game theorists. Unfortunately, this shift from a conscious restriction to a dogma may prevent alternative approaches from emerging. Some of these alternative approaches may be not only interesting for themselves, but they also may help understand better the traditional approach.
    This thesis proposes to suppress the "real-number-only dogma", and to consider alternative approaches. It introduces very abstract formalisms that generalise the notion of strategic games and the notion of Nash equilibrium. Subsequently, not all these abstract games have (abstract) Nash equilibria. This thesis exploits both Kuhn's technique and Nash's technique to cope with this issue. Along Kuhn and his precursors (\textit{e.g.} Zermelo), this thesis introduces the notion of abstract sequential game and substantially generalises Kuhn's result, all of this being fully formalised using the proof assistant Coq. Then it generalises abstract sequential games in graphs and thus further generalises Kuhn's result. Along Nash and his precursors (\textit{e.g.} Borel), this thesis considers ways of weakening the notion of Nash equilibrium to guarantee existence for every game. The probabilistic approach is irrelevant in this new settings, but depending on the new setting, either a notion of discrete non-determinism or the notion of sink for strongly connected component in a digraph will help solve the problem.
  • Abstract (in french): Les jeux stratégiques sont une classe de jeux fondamentale en théorie des jeux~: la notion d'équilibre de Nash fut d'abord définie pour cette classe. On peut se demander si tout jeu stratégique a un équilibre de Nash, mais ce n'est pas le cas. En outre, il semble qu'il n'existe pas de caractérisation simple des jeux stratégiques qui ont un équilibre de Nash. Dans la littérature, on peut trouver au moins deux méthodes qui pallient ce problème~: selon la première méthode, on définit les jeux séquentiels qui, à plongement près, sont une sous-classe des jeux stratégiques~; ensuite on définit les équilibres parfaits en sous-jeux qui sont, pour les jeux séquentiels, un raffinement de la notion d'équilibre de Nash~; enfin on prouve que tout jeu séquentiel a un équilibre parfait en sous-jeux. C'est ainsi que Kuhn montra que tout jeu séquentiel a un équilibre de Nash. Selon la deuxième méthode, on affaiblit la notion d'équilibre de Nash, par exemple en utilisant les probabilités. C'est ainsi que Nash montra que tout jeu stratégique fini a un équilibre de Nash probabiliste.
    Les travaux susnommés furent effectués pour des jeux impliquant seulement des gains qui sont des nombres réels; ceci après justification de cette restriction par von Neumann et Morgenstern qui mentionnèrent également, sans en poursuivre l'étude, une notion de gain abstrait. En raison de son succès, la restriction aux nombres réels devint rapidement un principe pour la plupart des théoriciens de jeux. Malheureusement, ce glissement d'une restriction consciente vers un dogme peut interdire l'émergence d'approches alternatives. Cependant, certaines de ces approches pourraient être non seulement intéressantes pour elles-mêmes, mais aussi aider à mieux appréhender l'approche traditionnelle.
    Cette thèse propose la suppression du dogme "tout est nombre réel" et l'étude d'approches alternatives. Elle introduit des formalismes abstraits qui généralisent les notions de jeu stratégique et d'équilibre de Nash. Bien entendu, certains jeux abstraits n'ont pas d'équilibre de Nash abstrait. Pour pallier ce problème d'existence, cette thèse exploite successivement les techniques de Kuhn et de Nash. Selon Kuhn et ses précurseurs (\textit{e.g.} Zermelo), cette thèse introduit la notion de jeu séquentiel abstrait et généralise le résultat de Kuhn de manière substantielle, tout ceci étant intégralement formalisé dans l'assistant de preuve Coq. Ensuite on généralise les jeux séquentiels abstraits au moyen des graphes et on obtient des résultats encore plus généraux. Selon Nash et ses précurseurs (\textit{e.g.} Borel), cette thèse considère des manières d'affaiblir la notion d'équilibre de Nash afin de garantir l'existence d'équilibre pour tout jeu. Cependant, l'approche probabiliste n'est plus pertinente dans les jeux abstraits. Alors, en fonction de la classe de jeux abstraits considérée, on résout le problème soit grâce à une notion de non-déterminisme discret, soit grâce à une notion de puits pour composante fortement connexe dans un graphe orienté.
  • Keywords:  Game Theory, strategic game, sequential game, Nash equilibrium, subgame perfect equilibrium, game, abstraction, generalisation, graph, convertibility, preference, best response, weakening, discrete non-determinism, strongly connected component, formalisation, automated proof verification.
  • Keywords (in french):  Théorie des jeux, jeu stratégique, jeu séquentiel, équilibre parfait en sous-jeux, jeu, abstraction, généralisation, graphe, convertibilité, préférence, meilleure réponse, affaiblissement, non-déterminisme discret, composante fortement connexe, formalisation, vérification automatique de preuve.
  • Availability: Electronic copy only.
  • Size: 226p
  • Format: Portable Document Format
  • Get it

Techniques modulo pour les bisimulations faibles.

  • By: Damien POUS
  • Number: PhD2008-02
  • Date: February 2008
  • Abstract:  While programming languages tend to give higher abstraction levels to the programmer, the programs that are written nowadays tend to be more complex: these programs are distributed, concurrent, interactive, and often, mobile. Moreover the critical role they may play sometimes requires a really precise analysis of their properties. This dissertation is devoted to the study of proof techniques for the analysis of such programs. We develop a theory of "up-to" techniques for coinduction, in the abstract setting of complete lattices. This theory contains new and general modularity results; it establishes the grounds for the reminder of the dissertation, where we focus on up-to techniques for bisimilarity. Up-to techniques for weak bisimilarity are known to be problematic. We show that these problems are related to similar phenomenons in term rewriting theory, and, using tools from this domain (strong normalisation and well-founded inductions), we develop up-to techniques going beyond existing ones. The benefits of these new techniques are illustrated by applying one of them in order to prove the correctness of a non-trivial distributed algorithm, for which standard techniques are not sufficient to give a satisfactory proof. Independently, by applying our general theory of up-to techniques in the function space, we show how to obtain second-order techniques, that allow us to revisit the "up to context" techniques: we define a generic method that greatly simplifies the study of such techniques. We illustrate this method by using it to recover up to contexts techniques in the case of CCS.
  • Abstract (in french): Bien que les langages de programmation actuels fournissent des niveaux d'abstraction de plus en plus élevés, les programmes définis de nos jours sont de plus en plus délicats à étudier: ils sont distribués, concurrents, interactifs, et bien souvent mobiles. De plus, le rôle parfois critique qu'ils endossent nécessite une analyse de plus en plus fine de leurs propriétés. Nous étudions dans cette thèse des techniques de preuve permettant de faciliter l'étude de tels programmes. Nous développons tout d'abord une théorie des techniques "modulo" pour la co-induction, dans le cadre abstrait des treillis complets. Cette théorie, qui établit des résultats de modularité génériques, fournit un socle solide pour la suite de la thèse, dédiée aux techniques modulo pour la bisimilarité. Dans le cas dit "faible" ces techniques modulo souffrent de limitations, dues à des phénomènes bien connus en théorie de la réécriture. En utilisant les outils de ce domaine (normalisation forte et inductions bien fondées), nous définissons de nouvelles techniques afin de contourner ces limitations. L'utilité de ces techniques est illustrée par l'étude détaillée d'un algorithme distribué non trivial (il s'agit de l'optimisation d'un environement d'exécution pour des processus distribués), et pour lequel les techniques standard s'avèrent insuffisantes D'autre part, en appliquant notre théorie des techniques modulo dans un espace de fonctions, nous montrons comment obtenir des techniques de second ordre, qui nous permettent de revisiter les techniques dites "modulo contexte": nous définissons une méthode qui permet de simplifer grandement l'étude de telles techniques, en la ramenant de façon systématique à une étude de cas élementaire. Nous illustrons cette méthode en l'appliquant dans le cas de CCS.
  • Keywords:  Semantics ; Process algebras ; Behavioural equivalences ; Bisimulation ; Up-to techniques ; Coinduction ; Complete lattices ; Relation algebras ; Distributed abstract machines.
  • Keywords (in french):  Sémantique ; Algèbres de processus ; Equivalences comportementales ; Bisimulation ; Techniques modulo ; Co-induction ; Treillis complets ; Algèbres relationnelles ; Machines abstraites distribuées.
  • Availability: Electronic copy only.
  • Size: 256p
  • Format: Portable Document Format
  • Get it

Propositions pour une versions inter-opérable du protocole /eXplicit Control Protocol/ dans des réseaux hétérogènes à haut débit.

  • By: Dino-Martin LOPEZ-PACHECO
  • Number: PhD2008-03
  • Date: June 2008
  • Abstract:  The congestion control protocols aim to fairly share the network resources between users and avoid congestion. In this thesis, we have first compared the performance of different protocols in networks where the bandwidth varies over time (Variable Bandwidth Environments -- VBE --) due to the aggregation/disaggregation of flows and/or the presence of Quality of Service (QoS) mechanisms. Thus, we have shown that the routers-assisted protocols providing Explicit Rate Notification (ERN protocols) provide higher fairness level and avoid congestion better than End-to-End (E2E) protocols (e.g., TCP-based protocols). However, the absence of inter-operability of ERN protocols with the non-ERN routers (like the DropTail routers) and the E2E congestion control protocols (like TCP) prevent the deployed of ERN protocols in current networks. In order to solve the problems of inter-operability of ERN protocols with non-ERN routers, we have proposed a solution which detects the set of non-ERN router between two ERN routers, estimates the available bandwidth in that set of non-ERN routers, and creates a virtual router that computes a feedback reflecting the estimated available bandwidth. Regarding the inter-operability problems of ERN protocols with E2E protocols, we have proposed a solution which provides friendliness between both kind of protocols. The mechanisms implemented by our friendliness solution can be divided in two steps. First, our solution estimates the resources needed by the ERN and E2E protocols in terms of bandwidth. Later, our friendliness solution randomly drops packets belonging to the E2E flows, with a probability updated on base of the results found in the first step. Since the success of ERN protocols depends on the information about the state of the network provided by the routers (the feedback), in this thesis we have studied the behavior of ERN protocols in scenarios where a percentage of the feedback has been lost. Such studies show that feedback losses in networks with VBE may lead to a chaotic behavior of ERN flows. Therefore, we have proposed a new architecture for ERN protocols which improves the responsiveness and the robustness of ERN flows in networks with VBE and feedback losses. The set of mechanisms and solutions presented in this thesis, easy to apply to several ERN protocols, have been implemented and validated on the eXplicit Control Protocol (XCP). Thus, we have shown that our solutions surmount the inter-operability problems of ERN protocols in a wide range of network topologies and scenarios. This thesis has provided the basis for creating an ERN protocol able to be gradually deployed in current heterogeneous large \emph{bandwidth-delay product} networks, where users frequently need to move very large amount of data (e.g., Data Grid).
  • Abstract (in french): Les protocoles de contrôle de congestion ont pour but d'autoriser un partage équitable des ressources entre les utilisateurs et d'éviter la congestion dans les réseaux de communications. Dans cette thèse, nous avons commencé par comparer la performance des différents protocoles dans des modèles de réseaux qui intègrent la notion de variation de bande passante produit par l'agrégation/désagrégation des flux ainsi que la présence des mécanismes fournissant de la Qualité du Service. Ainsi, nous avons montré que ce sont les protocoles basés sur l'assistance de routeurs fournissant aux émetteurs un taux d'émission explicite (``Explicit Rate Notification'' -- ERN --) partagent mieux les ressources du réseaux entre les utilisateurs et évitent mieux la congestion que les protocoles de bout-en-bout (comme les protocoles basés sur TCP). Cependant, l'absence d'inter-opérabilité des protocoles ERN avec les routeurs non-ERN (par exemple, les routeurs DropTail) et les protocoles de congestion de bout-en-bout (comme TCP), empêche leur mise en place dans les réseaux actuels. Pour résoudre les problèmes d'inter-opérabilité des protocoles ERN avec des routeurs non-ERN, nous avons proposé des stratégies et des mécanismes capables de détecter les groupes des routeurs non-ERN entre deux routeurs ERN, d'estimer la bande passante minimale disponible à l'intérieur de ces groupes, et de créer des routeurs virtuels qui remplacent chaque groupe de routeurs non-ERN par un routeur ERN. Nous avons également proposé un système d'équité inter-protocolaire entre les protocoles ERN et les protocoles de bout-en-bout. Avec notre solution, les routeurs ERN dans une première étape estiment les besoins en terme de bande passante des flux ERN et non-ERN puis, dans une deuxième étape, limitent le débit des flux non-ERN en rejetant leurs paquets avec une probabilité qui dépend des résultats de la première étape. Le succès des protocoles ERN est basé sur l'information de rétroalimentation, calculée par les routeurs, et renvoyée par les récepteurs aux émetteurs. Nous avons montré que les protocoles ERN deviennent instables face aux pertes de l'information de rétroalimentation dans des environnements hétérogènes et à bande passante variable. Dans ce cadre là, nous avons proposé une nouvelle architecture qui améliore la robustesse des protocoles ERN, ainsi que la réactivité des émetteurs. Toutes nos propositions, applicables sur d'autres protocoles ERN, ont été expérimentées et validées sur le protocole eXplicit Control Protocol (XCP). Ainsi, nous avons montré que nos solutions surmontent les défis concernant les problèmes d'inter-opérabilité des protocoles ERN dans un grand nombre des scénarios et de topologies. De cette façon, nous avons développé les bases pour bénéficier d'un protocole ERN capable d'être déployé dans des réseaux hétérogènes à grand produit bande passante-délai où le transfert de grande quantité des données est nécessaire, tels que les réseaux de grilles.
  • Keywords:  Congestion control protocols, Routers-assisted protocols, Explicit Rate Notification protocols, inter-operable ERN protocols, End-to-End protocols, XCP, TCP, HSTCP, Variable Bandwidth Environments, heterogeneous high speed networks.
  • Keywords (in french):  Protocoles de contrôle de congestion, Protocoles basés sur l'assistance des routeurs, Protocoles de notification de vitesse explicite, Protocoles ERN inter-opérables, Protocoles de bout-en-bout, XCP, TCP, HSTCP, Environnements à Bande passante Variable, Réseaux hétérogènes à haut débit.
  • Availability: Electronic copy only.
  • Size: 150p
  • Format: Portable Document Format
  • Get it

Opérateurs arithmétiques matériels optimisés.

  • By: Romain MICHARD
  • Number: PhD2008-04
  • Date: June 2008
  • Abstract:  Computer arithmetic is a branch of computer science dedicated to number systems, arithmetic algorithms and their hardware and software implementations. This thesis deals with the study and hardware implementation of operators for the evaluation of functions in digital signal and image processing. Different types of operators are presented: a division optimized operators generator, some studies about a function evaluation algorithm using fractional approximations, and functions evaluation operators based on polynomial approximations and requiring few hardware resources. The various operators proposed in this thesis have been validated on FPGA circuits.
  • Abstract (in french): L'arithmétique des ordinateurs est une branche de l'informatique qui traite des systèmes de représentation des nombres, des algorithmes arithmétiques et de leurs implantations matérielles ou logicielles. Cette thèse porte sur l'étude et l'implantation matérielle d'opérateurs pour l'évaluation de fonctions en traitement du signal et des images. Sont présentés successivement un générateur d'opérateurs optimisés pour la division, des études portant sur un algorithme d'évaluation de fonctions au moyen d'approximations par fractions rationnelles, et des opérateurs d'évaluation de fonctions basés sur des approximations polynomiales qui demandent peu de matériel. Les différents opérateurs proposés dans cette thèse ont tous été validés sur des circuits FPGA.
  • Keywords:  computer arithmetic, FPGA, hardware operator, fixed point, polynomial approximation, shift-and-add algorithm, division, SRT algorithm, VHDL generator.
  • Keywords (in french):  arithmétique des ordinateurs, FPGA, opérateur matériel, virgule fixe, approximation polynomiale, algorithme addition/décalage, division, opérateur SRT, générateur VHDL.
  • Availability: Electronic copy only.
  • Size: 120p
  • Format: Portable Document Format
  • Get it

Communication-aware scheduling on heterogeneous master-worker platforms.

  • By: Jean-François PINEAU
  • Number: PhD2008-05
  • Date: September 2008
  • Abstract:  The results summarized in this document deal with the scheduling of independent tasks on large scale master-worker platforms, when realistic communication models are utilized. The contributions of this work are divided into three main parts: 1) Parallel algorithms: we underline the difficulty of scheduling identical independent tasks on heterogeneous master-worker platforms using the one-port communication model. We look at several sources of heterogeneity as well as several objective functions; 2) Matrix product: we compute the total communication volume that is needed for matrix multiplication in the presence of memory constraints and when data is centralized, and we develop a memory layout whose performance is close to the theoretical lower bound on the communication volume. We extend this algorithm for heterogeneous platforms; 3) Scheduling: lots of applications are constituted of a very large number of independent identical tasks. We focus on steady-state, and prove how to minimize the slowdown of one application when several are deployed, and how to minimize power consumption when only one application is present.
  • Abstract (in french): Les travaux présentés dans cette thèse portent sur diverses techniques d'ordonnancement de tâches indépendantes pour des plates-formes de type maître-esclaves distribuées à grande échelle, lorsque les temps de communications des tâches sont pris en compte par des modèles réalistes. Les contributions de cette thèse se situent à trois niveaux : 1) Algorithmique Parallèle : nous avons montré la complexité d'ordonnancer des tâches indépendantes sur une plate-forme hétérogène en modélisant les communications avec un modèle un-port, en regardant plusieurs sources d'hétérogénéité et plusieurs fonctions objectives; 2) Produit de matrices : nous avons calculé la borne théorique du volume de communication minimal nécessaire pour effectuer un produit de matrices dont les données sont centralisées, et où la mémoire des esclaves est limitée, et nous avons défini un algorithme efficace de partage de la mémoire, impliquant un volume de communication proche de la borne théorique. Nous avons ensuite étendu cet algorithme à des plate-formes hétérogènes; 3) Ordonnancement : dans le cadre d'ordonnancement d'applications constituées d'un très grand nombre de tâches indépendantes et de caractéristiques identiques, nous avons étudié en régime permanent comment minimiser le retard de chaque application lorsqu'elles sont plusieurs à entrer en compétition pour les ressources de calcul, et comment minimiser la consommation de la plate-forme lorsqu'une seule application est déployée.
  • Keywords:  Scheduling, independent tasks, communication models, master-worker platform.
  • Keywords (in french):  Ordonnancement, tâches indépendantes, modèles de communication, plate-forme maître-esclaves.
  • Availability: Electronic copy only.
  • Size: 200p
  • Format: Portable Document Format
  • Get it

Peer-to-Peer Prefix Tree for Large Scale Service Discovery.

  • By: Cédric TEDESCHI
  • Number: PhD2008-06
  • Date: October 2008
  • Abstract:  The problem studied in this thesis is the service discovery on platforms distributed at large scale, a service being a computing service (software components, scientific computing libraries, or binaries) offered with some characteristics and a performance level related to the hardware supporting it. Traditional approaches, designed for reliable and small scale environments, rely upon centralized solutions, unable to scale well in geographically distributed unreliable platforms. Our contribution centers around three main parts. 1) We propose a novel approach called DLPT (Distributed Lexicographic Placement Table), whose design is inspired by peer-to-peer systems. It calls upon an indexing system structured as a prefix tree. This structure supports multi-attribute range queries. 2) We study the mapping of nodes of this tree onto heterogeneous processors of the dynamic underlying network. We propose and adapt some load balancing heuristics for this kind of architectures. 3) Our architecture, targeted for platforms within which processors are unreliable and constantly joining and leaving the network, requires fault-tolerance mechanisms. Replication, usually used, is costly and unable to manage transient faults. We propose alternative best-effort mechanisms based on the self-stabilization theory for the construction and maintenance of prefix trees in a peer-to-peer environment. Among the mechanisms provided, one is proven to be snap-stabilizing. This means that the tree is rebuilt in an optimal time after an arbitrary number of faults. This approach is written in a coarse grain communication model and assumes several restrictions on initial topology handled, making it hard to implement on real platforms. To address these drawbacks, another self-stabilizing protocol is given for actual message-passing environments. Finally, we present a software prototype of this architecture and its first promising experiments on the Grid'5000 platform.
  • Abstract (in french): Cette thèse étudie la découverte de services (composants logiciels, exécutables, librairies scientifiques) sur des plates-formes distribuées à grande échelle. Les approches traditionnelles, proposées pour des environnements stables et relativement petits, s'appuient sur des techniques centralisées impropres au passage à l'échelle dans des environnements géographiquement distribués et instables. Notre contribution s'articule autour de trois axes. 1) Nous proposons une nouvelle approche appelée DLPT (Distributed Lexicographic Placement Table), qui s'inspire des systèmes pair-à-pair et s'appuie sur un réseau de recouvrement structuré en arbre de préfixes. Cette structure permet des recherches multi-attributs sur des plages de valeurs. 2) Nous étudions la distribution des noeuds de l'arbre sur les processeurs de la plate-forme sous-jacente, distribuée, dynamique et hétérogène. Nous proposons et adaptons des heuristiques de répartition de la charge pour ce type d'architectures. 3) Notre plate-forme cible, par nature instable, nécessite des mécanismes robustes pour la tolérance aux pannes. La réplication traditionnellement utilisée s'y avère coûteuse et incapable de gérer des fautes transitoires. Nous proposons des techniques de tolérance aux pannes best-effort fondées sur la théorie de l'auto-stabilisation pour la construction d'arbres de préfixes dans des environnements pair-à-pair. Nous présentons deux approches. La première, écrite dans un modèle théorique à gros grain, permet de maintenir des arbres de préfixes instantanément stabilisants, c'est-à-dire reconstruits en un temps optimal après un nombre arbitraire de fautes. La deuxième, écrite dans le modèle à passage de messages, permet l'implantation d'une telle architecture dans des réseaux très dynamiques. Enfin, nous présentons un prototype logiciel mettant en oeuvre cette architecture et présentons ses premières expérimentations sur la plate-forme Grid'5000.
  • Keywords:  Service Discovery, Peer-to-Peer Systems, Grid Computing, Prefix Trees, Fault-tolerance, Self-Stabilization.
  • Keywords (in french):  Découverte de services, Systèmes pair-à-pair, Grilles de calcul, Arbres de préfixes, Tolérance aux pannes, Auto-stabilisation.
  • Availability: Electronic copy only.
  • Size: 152p
  • Format: Portable Document Format
  • Get it

Arrondi correct de fonctions mathématiques Fonctions univariées et bivariées, certification et automatisation.

  • By: Christoph Quirin LAUTER
  • Number: PhD2008-07
  • Date: October 2008
  • Abstract:  This work extends the practically accessible research space for correctly rounded floating-point implementations of mathematical functions. Interest goes first from univariate functions like log to classes of univariate functions like x^n, then to the bivariate function x^y. An innovative approach for detecting the rounding boundary cases of x^y using partial worst-case information is proposed. The novel techniques yields to a consequent speed-up.

     

    Then automatic approaches are contributed that allow for certifying a correctly rounded implementation of a function. For the certification of bounds on approximation errors, a novel algorithm for computing certified infinity norms is presented and implemented. Concerning round-off error in an implementation of a mathematical function, techniques are developed for analysing them using the Gappa tool.

    Finally, algorithms are developed that permit to automate the implementation process for mathematical functions. A first realisation in the Sollya tool allows for generating and certifying, without any human intervention, the code for evaluating a function. With such an automatic tool, large solution spaces can be searched in order to find an optimised implementation. In the future, an integration of the techniques in a compiler could be investigated.

  • Abstract (in french): Cette thèse élargit l'espace de recherche accessible en pratique pour des implantations de fonctions mathématiques correctement arrondies en virgule flottante. Elle passe d'abord de l'arrondi correct de fonctions univariées comme log à des familles de fonctions univariées x^n, puis à la fonction bivariée x^y. Une approche innovatrice pour la détection de cas de frontière d'arrondi de x^y à l'aide d'une information partielle sur les pires cas de cette fonction est proposée. Cette innovation provoque un gain en vitesse conséquent.

     

    Ensuite, cette thèse propose des approches automatiques pour certifier une implantation de fonction correctement arrondie. Pour la certifications des bornes d'erreur d'approximation, un nouvel algorithme pour le calcul de normes infini certifiées est présenté et mis en pratique. Puis les erreurs d'arrondi dans une implantation de fonction mathématique sont analysées par des techniques développées pour l'outil de preuve formelle Gappa.

    Finalement, des algorithmes sont développés qui permettent l'automatisation de l'implantation de fonctions. Une première mise en œuvre dans l'outil Sollya permet de générer et certifier, sans aucune intervention humaine, le code pour évaluer une fonction mathématique. À l'aide d'un tel outil automatique, de larges espaces de recherches peuvent être parcouru afin d'optimiser une implantation. Au futur, une intégration de ces techniques dans un compilateur est envisageable.

  • Keywords:  Mathematical and elementary functions, Power function, Correct rounding, libm, Floating-point code, Certification, Infinity norm, Supremum norm, Sollya, Numerical code synthesis.
  • Keywords (in french): Fonctions mathématiques et élémentaires, fonction power, arrondi correct, libm, virgule flottante, certification, norme infini, norme sup, Sollya, synthèse de code numérique.
  • Availability: Electronic copy only.
  • Size: 212p
  • Format: Portable Document Format
  • Get it

Contributions to Session Aware Frameworks for Next Generation Internet Services.

  • By: Narjess AYARI
  • Number: PhD2008-08
  • Date: October 2008
  • Abstract:  This thesis focuses on studying the contribution of edge processing equipments in improving the perceived end-to-end QoS. Our goal is to recommend an efficient scheme for improving the perceived end-to-end QoS, either under server overload, or across failures. Firstly, we have advocated a methodology, for efficiently improving the scalability of high performance cluster-based Internet servers, subjected to multiple flow-based sessions. We have proposed a fully client/server transparent framework that uses original concepts to guarantee fine grained session integrity. It provides the means necessary to improve the operator's profitability, by maximizing the useful throughput of its edge processing equipments. Indeed, we believe that the useful throughput reveals the scalability pattern more accurately, from an economic-justified point of view. Secondly, we have turned our attention to investigating the problem of session aware admission control. We have discussed the trade-off faced by an operator when dealing with offered user-sessions. Based on an economic-justified model, where session interruption is perceived in a worse way than session rejection, we have advocated an optimal management, which consists in accepting all the offered packets, when the server load is below a given threshold, and in giving, above that threshold, a higher priority to the packets pertaining to the already active sessions. Through simulations, we have shown that, responsive session aware admission control contributes in providing improved QoS to subscribers, under overload. As well, it achieves an increased success rate, thereby improved operator's revenue. Additionally, we have shown that session awareness guarantees QoS in terms of the completion of the accepted sessions independently of their duration. At a second step, we have described a fully client/server transparent methodology for engineering fault tolerant network services. The design that we have advocated is based on the concept of active replication. It adds no additional complexity to a legitimate processing server during failsafe periods, and enhances the robustness of Internet servers across failures. In particular, it avoids the interruption of the active sessions, should the legitimate processing server fail. Advanced experiments have been conducted using representative interactive services. Results have shown that the framework provides truthful state replication during failsafe periods, as well as a sustained performance, during failures.
  • Abstract (in french): Cette thèse s'inscrit dans le cadre d'études visant à améliorer la qualité de service d'un serveur Internet, mono-serveur ou en grappe, en cas de surcharge ou en cas de panne. En premier lieu, nous recommandons une architecture orientée session pour le traitement efficace de trafic réseau, offert à une grappe de serveurs Internet. En effet, le traitement à l'échelle session est plus approprié pour l'évaluation de critères de performance d'un serveur Internet. Nous nous focalisons ensuite sur l'évaluation de mécanismes de contrôle d'admission implicites, opérant à l'échelle session. Nous sommes motivés par un constat économique, soulignant que le phénomène d'interruption de sessions contribue significativement à la réduction des bénéfices de l'opérateur. Nous proposons des mécanismes visant à garantir une meilleure utilisation des ressources d'un serveur de traitement. Une évaluation des mécanismes proposés est conduite via simulation. Nous démontrons que le paradigme orienté session garantie une qualité de service pour les sessions offertes, indépendamment de leur durée. En deuxième lieu, nous nous intéressons à améliorer la disponibilité des services Internet. En effet, nous avons constaté que la panne d'un serveur de traitement résulte aussi bien en l'indisponibilité du service offert, qu'en l'interruption des sessions déjà établies avec celui-ci. Ceci se traduit naturellement par une réduction du gain de l'opérateur ainsi que par la dégradation de la qualité de service offerte aux abonnés. Nous proposons une architecture flexible basée sur le concept de la réplication active des conversations légitimes. Cette architecture garantie aux services dits "à états" une performance adéquate, en cas de panne du serveur de traitement légitime. Elle est totalement transparente aux clients et ne rajoute pas une complexité additionnelle aux serveurs primaires. L'architecture proposée a été entièrement développée et mise en ?uvre par nos soins. Nous avons évalué sa performance à améliorer la fiabilité de services à caractère interactif. Les résultats démontrent que l'architecture proposée permet une réplication consistante des états du service hautement disponible, et qu'elle réagit efficacement aux pannes.
  • Keywords:  Session aware networking, admission control, active replication, high availability, reliability.
  • Keywords (in french):  Session aware networking, contrôle d'admission, réplication active, haute disponibilité, fiabilité.
  • Availability: Electronic copy only.
  • Size: 153p
  • Format: Portable Document Format
  • Get it

Analyse et déploiement de solutions algorithmiques et logicielles pour des applications bioinformatiques à grande échelle sur la grille.

  • By: Raphaël BOLZE
  • Number: PhD2008-09
  • Date: October 2008
  • Abstract:  This thesis was conducted by the needs of the Decrypthon project (collaborative project between AFM, CNRS and IBM). First we show the role of architect played in order to select and define the Decrypthon grid infrastructure. The resources of this grid are hosted by five Universities (Bordeaux I, Lille I, ENS-Lyon, Pierre et Marie Curie Paris VI et Orsay). The network connexion is provided by RENATER (Réseau National de Télécommunications pour l'Enseignement et la Recherche). The CRIHAN ( Centre de ressources Informatiques de Hautes Normandie) is also involved into this parternship and provides data warehouse for scientists. In a second hand we present several experiments carried on Grid'5000 in order to validate the grid middleware DIET and its tools on a large scale platform such as Grid'5000. On this research platform, we also studied the application of the project "Help Cure Muscular Dystrophy", one of the project selected by the Decrypthon. This study have prepared the launch of a 6 months computing phase on the volunteers grid : World Community Grid support by IBM US. The document presents all steps before and after the computing phase which require more than 80 centuries of CPU time on the volunteers device. Finally, we have designed several heuristics to tackle the problem of online multi-workflow scheduling in a shared grid environement. We have implemented those heuristics into DIET middleware and we have validated their behaviors with case study applications from Decrypthon. This work asks for many software developments in the aim to grid enabled bioinformatic applications and transparenlty give access to the Decrypthon grid, but also into DIET middleware and tools around : DIET_Webboard, VizDIET, GoDIET, LogService, MA_DAG, etc. The results expose in this thesis were obtained with tree different grids : the Decrypthon grid, the volunteer grid (World Community Grid) and the research grid (Grid'5000).
  • Abstract (in french): Cette thèse présente un ensemble d'objectifs dont le fil conducteur est le programme Décrypthon (projet tripartite entre l'AFM, le CNRS et IBM) où les applications et les besoins ont évolué au fur et à mesure de l'avancée de nos travaux. Dans un premier temps nous montrerons le rôle d'architecte que nous avons endossé pour la conception de la grille Décrypthon. Les ressources de cette grille sont supportées par les cinq universités partenaires (Bordeaux I, Lille I, ENS-Lyon, Pierre et Marie Curie Paris VI et Orsay), ainsi que le réseau RENATER (Réseau National de Télécommunications pour l'Enseignement et la Recherche), sur lequel est connecté l'ensemble des machines. Le Centre de ressources informatiques de Haute Normandie (CRIHAN) participe également au programme, il héberge les données volumineuses des projets scientifiques. Nous présenterons ensuite les expériences que nous avons effectuées sur l'intergiciel DIET afin de tester ses propriétés de façon à explorer sa stabilité dans un environnement à grande échelle comme Grid'5000. Nous nous sommes intéressés, en outre, au projet "Help Cure Muscular Dystrophy", un des projets sélectionnés par le programme Décrypthon. Nous avons conduit des expériences dans le but de préparer la première phase de calcul sur la grille de volontaires "World Community Grid". Nous dévoilerons l'ensemble des étapes qui ont précédées et suivies la première phase calculatoire qui a demandé quelques 80 siècles de temps processeur. Pour terminer, nous avons développé une fonctionnalité à l'intergiciel DIET, le rendant capable de gérer l'exécution de tâches ayant des dépendances. Nous nous sommes intéressés à développer des algorithmes prenant en compte plusieurs applications qui demandent l'accès aux mêmes ressources de manière concurrente. Nous avons validé cette fonctionnalité avec des applications issues des projets du programme Décrython. Ces travaux ont nécessité un développement logiciel important, d'une part sur les applications du Décrypthon elles-mêmes et sur leur portage afin de rendre transparente leur utilisation sur la grille Décrypthon, mais aussi au niveau de l'intergiciel DIET et son écosystème : DIET_Webboard, VizDIET, GoDIET, LogService, MA_DAG, etc. Les résultats présentés ont été obtenus sur trois grilles mises à notre disposition: la grille universitaire du Décrypthon, la grille d'internautes (World Community Grid) et la grille expérimentale Grid'5000.
  • Keywords:  grid middleware, bioinformatics, multi-workflow scheduling, volunteer computing, comparative grids study, Décrypthon.
  • Keywords (in french): intergiciel de grille, bioinformatique, ordonnancement multi-workflow, calcul sur grille de volontaire, étude compartive de grilles, Décrypthon.
  • Availability: Electronic copy only.
  • Size: 192p
  • Format: Portable Document Format
  • Get it

Sur les automates cellulaires probabilistes: comportements asynchrones.

  • By: Damien REGNAULT
  • Number: PhD2008-10
  • Date: November 2008
  • Abstract:  In this thesis, we study the behavior of cellular automata under asynchronous dynamics, where at each time step a random subset of cells is updated. The behavior of cellular automata under these dynamics is radically different from their classical behavior. Under synchronous dynamics, signals appear, move, collide and disappear. Under asynchronous dynamics, patterns appear quickly and the regions corresponding to the different patterns compete with each other to recover the whole configuration. Depending on the rule of the automaton, either a pattern manage to cover the whole configuration and the dynamics reaches a stable configuration; or the different regions evolve constantly. We considered many cellular automata in order to encounter different behaviors: random walks, movements of particles, percolation, interactions between 2D regions, etc. We developed general tools which can be used to analyze many cases.
  • Abstract (in french): Dans cette thèse, nous étudions le comportement des automates cellulaires en dynamiques asynchrones, où à chaque pas de temps seulement un sous-ensemble aléatoire de cellules se met à jour. Le comportement des automates cellulaires évoluant sous ces régimes est radicalement différent de leur comportement classique. En dynamique synchrone, on constate principalement des signaux qui naissent, se déplacent, s'intersectent et meurent. En dynamique asynchrone, des motifs propres à la règle apparaissent rapidement et les zones coloriées par ces différents motifs entrent en compétition pour recouvrir la configuration. Selon la règle de l'automate, soit un motif l'emporte et la dynamique atteint une configuration stable; soit ces zones évoluent en permanence. Nous avons utilisé une approche exploratoire pour rencontrer un grand nombre de comportements différents: marches aléatoires, mouvements de particules, percolation, interactions entre zones 2D, etc. Nous avons également cherché à développer des outils généraux permettant ainsi d'analyser un grand nombre de cas.
  • Keywords:  Cellular automata, stochastic dynamics, relaxation time, stochastic processes, random walks, percolation.
  • Keywords (in french):  Théorie des jeux, jeu stratégique, jeu séquentiel, équilibre parfait en sous-jeux, jeu, abstraction, généralisation, graphe, convertibilité, préférence, meilleure réponse, affaiblissement, non-déterminisme discret, composante fortement connexe, formalisation, vérification automatique de preuve.
  • Availability: Electronic copy only.
  • Size: 166p
  • Format: Portable Document Format
  • Get it

Géométrie pour l'auto-assemblage.

  • By: Florent BECKER
  • Number: PhD2008-11
  • Date: November 2008
  • Abstract:  .
  • Abstract (in french): .
  • Keywords (in french):.
  • Availability: Electronic copy only.
  • Size: p
  • Format: Portable Document Format
  • Get it

On the Out-Of-Core Factorization of Large Sparse Matrices.

  • By: Emmanuel AGULLO
  • Number: PhD2008-12
  • Date: November 2008
  • Abstract:  .
  • Abstract (in french): .
  • Keywords (in french):.
  • Availability: Electronic copy only.
  • Size: p
  • Format: Portable Document Format
  • Get it

Robustesse et émergence dans les systèmes complexes.

  • By: Jean-Baptiste ROUQUIER
  • Number: PhD2008-13
  • Date: December 2008
  • Abstract:  .
  • Abstract (in french): The aim of this work is to better understand what happens when one perturbs a complex system, using the model of cellular automata. We focus mainly on two perturbations. The first one deals with how time is passing: as opposed to the usual model, we use asynchronous updates, i.e. at each time step, only some cells are updated. The second perturbations deals with the topology, i.e. the graph of interactions between cells. The first part studies experimentally the apparition of directed percolation in cellular automata, in particular in the framework of damage spreading. The last chapter of this part proves an equivalence between a class of probabilistic cellular automata and asynchronous cellular automata. The second part studies in a first chapter the interplay of both mentioned perturbations: asynchronism and topology. While the usual model is defined on a Zd grid, we study a grid where some links are temporarily broken. The a second chapter proves a few theoretical properties of the minority rule when the topology is a tree. In this thesis, we conducted both experimental and theoretical studies. A transverse question is formal simulations between models. The aim of those works is, in the long term, to know how to get systems with a predefined global behavior, or how to make robust against some perturbations a given complex system.
  • Abstract (in french) L'objet de ce travail est de mieux comprendre ce qui se produit lorsque l'on perturbe un système complexe, en utilisant les automates cellulaires comme modèle. Nous nous intéressons principalement à deux perturbations. La première concerne l'écoulement du temps : contrairement au modèle habituel, nous utilisons des mises à jour asynchrones, c'est-à-dire que, à chaque étape, seulement une partie des cellules sont mises à jour. L'autre perturbation concerne la topologie, c'est-à-dire le graphe d'interaction entre les cellules. Une première partie étudie expérimentalement l'apparition de la percolation dirigée dans les automates cellulaires, notamment dans le cadre du  damage spreading ». Le dernier chapitre de cette partie prouve une équivalence entre une classe d'automates cellulaires probabilistes et les automates cellulaires asynchrones. La seconde partie étudie dans un premier chapitre l'interaction des deux perturbations évoquées: asynchronisme et topologie. Alors que le modèle habituel utilise une grille Zd, nous étudions une grille où certains liens sont temporairement coupés. Puis un second chapitre démontre des propriétés théoriques sur la règles minorité lorsque la topologie est un arbre. Nous avons dans cette thèse mené à la fois des études expérimentales et des études théoriques. Une préoccupation transversale est la simulation formelle entre modèles. L'enjeu de ces travaux est, à terme, de savoir comment obtenir des systèmes ayant un comportement global prédéfini, ou bien comment rendre robuste à certaines perturbations un système complexe donné.
  • Keywords:  cellular automata, complex systems, perturbation, robustness, synchronisation, coalescence, coupling, simulation, equivalence, reduction, CA, probabilistic cellular automata, PCA, elementary cellular automata, ECA, asynchronous cellular automata, directed percolation, universality class, phase transition, minority, trees, hitting time, relaxing time, asynchronism, topology perturbation, discrete dynamical system, stochastic process, Markov chain.
  • Keywords (in french):  automates cellulaires, systèmes complexes, perturbation, robustesse, synchronisation, coalescence, couplage, simulation, équivalence, réduction, CA, automate cellulaire probabiliste, PCA, automate cellulaire élémentaire, ECA, automate cellulaire asynchrone, percolation dirigée, classe d'universalité, transition de phase, minorité, arbres, temps d'atteinte, temps transitoire, temps de relaxation, asynchronisme, perturbation de la topologie, systéme dynamique discret, processus stochastique, chaîne de Markov.
  • Availability: Electronic copy only.
  • Size: 128p
  • Format: Portable Document Format
  • Get it