Dissertations / Theses: 'Compilation (informatique)'

7

Moreau, Pierre-Étienne. "Compilation de règles de réécriture et de stratégies non-déterministes." Nancy 1, 1999. http://www.theses.fr/1999NAN10121.

Full text

Abstract:

Les techniques de réécriture ont été développées depuis les années 1970 et appliquées en particulier au prototypage des spécifications formelles algébriques et à la démonstration de propriétés liées à la vérification de programmes. ELAN est un système qui permet de spécifier et d'exécuter des résolveurs de contraintes, des démonstrateurs et plus généralement tout processus décrit par des règles de transformation. Il possède des opérateurs associatifs-commutatifs (AC) et un langage de stratégies qui permettent une gestion fine de l'exploration d'un arbre de recherche et une manipulation aisée d'opérateurs mathématiques tels que les connecteurs booléens, les opérateurs arithmétiques ou les opérateurs de composition parallèle par exemple. Ces deux notions améliorent grandement l'expressivité du langage mais introduisent un double non-déterminisme lié à la possibilité d'appliquer plusieurs règles, de différentes façons, sur un terme donné. Cela rend difficile et généralement peu efficace leur implantation. L'objectif principal de cette thèse est d'étudier des techniques de compilation qui améliorent l'efficacité de ce type de langages. Nous proposons un nouvel algorithme, à base d'automates déterministes, pour compiler efficacement le filtrage syntaxique. Nous définissons ensuite différentes classes de règles pour lesquelles nous proposons un algorithme efficace de filtrage AC. Cet algorithme utilise une structure de données compacte et les automates définis précédemment, ce qui améliore considérablement les performances du processus de normalisation dans son ensemble. [. . . ]

APA, Harvard, Vancouver, ISO, and other styles

8

Arcangeli, Jean-Paul. "Définition et mise en oeuvre d'une stratégie de compilation pour l'implantation des langages d'acteurs : application à PLASMA." Toulouse 3, 1990. http://www.theses.fr/1990TOU30126.

Full text

Abstract:

La compilation est une strategie alternative pour l'implantation des langages d'acteurs qui, classiquement sont interpretes. Le compilateur complete l'environnement de programmation plasma, mais l'interprete est conserve pour le developpement et la mise au point. Le compilateur subvient aux besoins de performances: il traite des applications debogues avant leur exploitation. Le programme objet, est integre a l'interprete de base de plasma, donnant ainsi un nouvel interprete etendu aux acteurs de l'application compilee. Ces derniers s'exploitent alors comme s'ils s'agissaient d'acteurs primitifs. Ainsi, la strategie de compilation peut s'assimiler a une curryfication de l'interpretation. Le langage de la machine virtuelle lila, qui supporte l'interprete plasma, est le langage intermediaire du processus de compilation. Il offre un ensemble de primitives bien adaptees a la gestion de plasma, et il est de nouveau suffisamment eleve pour assurer la portabilite des logiciels engendres. La traduction des programmes lila en langage machine assure leur efficacite. Le compilateur est specialise dans la gestion des environnements et du controle: filtrage, fermetures, et transmissions de messages avec ou sans continuation. Un filtre est compile en un code lineaire, quelle que soit sa structure initiale: la structure de controle du filtrage n'est plus la recursivite mais la sequence et les branchements. Les fermetures compilees sont des arborescences: le script compile est une sequence de code lila, partage par toutes les instances d'un modele, et referencant un environnement compile specifique. De cette facon, les instances creees dynamiquement en phase d'exploitation sont structurees de la meme facon que les acteurs compiles du programme source. Enfin, la compilation des transmissions permet la programmation applicative et imperative, ainsi que les passages ou les captures de continuation. Ainsi, les applications comp

APA, Harvard, Vancouver, ISO, and other styles

9

Fernández, de Retana Yon. "Vers la compilation vérifiée de Sea of Nodes : propriétés et raisonnement sémantiques." Thesis, Rennes 1, 2018. http://www.theses.fr/2018REN1S020/document.

Full text

Abstract:

Les compilateurs optimisants pour les langages de programmation sont devenus des logiciels complexes et donc une source de bugs. Ceci peut être dangereux dans le contexte de systèmes critiques comme l'avionique ou la médecine. Cette thèse s'inscrit dans le cadre de la compilation vérifiée optimisante dont l'objectif est d'assurer l'absence de tels bugs. Plus précisément, nous étudions sémantiquement une représentation intermédiaire SSA (Single Static Assignment) particulière, Sea of Nodes, utilisée notamment dans le compilateur optimisant HotSpot pour Java. La propriété SSA a déjà été étudiée d'un point de vue sémantique sur des représentations simples sous forme de graphe de flot de contrôle, mais le sujet des dépendances entre instructions a seulement été effleuré depuis une perspective formelle. Cette thèse apporte une étude sémantique de transformations de programmes sous forme Sea of Nodes, intégrant la flexibilité en termes de dépendances de données entre instructions. En particulier, élimination de zero-checks redondants, propagation de constantes, retour au bloc de base séquentiel et destruction de SSA sont étudiés. Certains des sujets abordés, dont la formalisation d'une sémantique pour Sea of Nodes, sont accompagnés d'une vérification à l'aide de l'assistant de preuve Coq Optimizing compilers for programming languages have become complex software, and they are hence subject to bugs. This can be dangerous in the context of critical systems such as avionics or health care. This thesis is part of research work on verified optimizing compilers, whose objective is to ensure the absence of such bugs. More precisely, we semantically study a particular SSA intermediate representation, Sea of Nodes, which is notably used in the optimizing compiler HotSpot for Java. The SSA property has already been studied from a semantic point of view on simple intermediate representations in control flow graph form, but the subject of dependencies between instructions has just been skimmed from a formal perspective. This thesis brings a semantic study of transformations of programs in Sea of Nodes form, integrating the flexibility regarding data dependencies between instructions. In particular, redundant zero-check elimination, constant propagation, transformation back to sequential basic block, and SSA destruction are studied. Some of the approached topics, including the formalization of a semantics for Sea of Nodes, are accompanied by a verification using the Coq proof assistant

APA, Harvard, Vancouver, ISO, and other styles

10

Carribault, Patrick. "Contribution to the compilation of irregular programs for complex architectures." Versailles-St Quentin en Yvelines, 2007. http://www.theses.fr/2007VERS0012.

Full text

Abstract:

Contribution à la compilation de programmes irréguliers pour des architecturescomplexesLes architectures multicoeurs sont omniprésentes dans les processeurs généralistes et embarqués. Plusieurs flôts d'instructions (threads) sont exécutés, augmentant le parallélisme, évitant des contentions de ressources. L'execution concurrente d'un thread est déterminant pour le temps d'execution de l'application. Ainsi, l'exploitation fine d'un coeur est indispensable afin de découvrir du parallelisme d'instructions (ILP) au sein d'un flot d'instructions. Cette thèse traite de l'optimisation monocoeur de codes irréguliers comportant du parallélisme "caché". Nous avons conçus des transformations permettant d'augmenter leur ILP : Deep Jam convertissant du parallelisme à gros grain,restructuration des arbres de décisions et une plateforme d'ordonnancement d'instructions unifiant les dépendences de données et les contraintes de ressources complexes. Des accélérations par rapport à des techniques et compilateurs de pointe ont été obtenues sur Itanium 2 Contribution to the Compilation of Irregular Programs for Complex ArchitecturesMulticore architectures are ubiquitous in general purpose and embedded systems. Modern processors execute several instruction flows (threads) increasing the parallelism and accommodating for resource stalls. Both the execution of a thread and its interaction with the others shape the overall performance of an application. Thus, an accurate exploitation of a single core is mandatory: it leads to the necessity to discover the instruction-level parallelism (ILP) within an instruction flow. This thesis focuses on the monocore optimization of irregular codes hoseparallelism is "hidden" behind complex control flow. We designedtransformations to increase their ILP: Deep Jam converting coarse-grain parallelism, decision tree reshaping and an instruction-scheduling framework unifying data dependences and complex resource constraints. Everytransformation leads to significant speedups on a wide issue architecture(Itanium), compared to state-of-the-art techniques and compilers

APA, Harvard, Vancouver, ISO, and other styles

11

Dang, Alexandre. "Compilation sécurisée pour la protection de la mémoire." Thesis, Rennes 1, 2019. http://www.theses.fr/2019REN1S111.

Full text

Abstract:

Cette thèse porte sur la sécurité des programmes et particulièrement en utilisant la compilation pour parvenir à ses fins. La compilation correspond à la traduction des programmes sources écrits par des humains vers du code machine lisible par nos systèmes. Nous explorons les deux manières possible de faire de la compilation sécurisée : la sécurisation et la préservation. Premièrement, nous avons développé CompCertSFI, un compilateur qui sécurise des modules en les isolant dans des zones mémoires restreintes appelées bac à sable. Ces modules sont ensuite incapables d'accéder à des zones mémoires hors de leur bac à sable, ce qui empêche un module malveillant de corrompre d'autres entités du système. Sur le sujet de la préservation, nous avons défini une notion de Préservation de Flot d'Information qui s'applique aux transformations de programme. Cette propriété, lorsqu'elle est appliquée, permet de s'assurer qu'un programme ne devienne moins sécurité durant sa compilation. Notre propriété de préservation est spécifiquement conçus pour préserver les protections contre les attaques de type canaux cachés. Cette nouvelle catégorie d'attaque utilise des médiums physique comme le temps ou la consommation d'énergie qui ne sont pas pris en compte par les compilateurs actuels Our society has been growingly dependent on computer systems and this tendency will not slow down in the incoming years. Similarly, interests over cybersecurity have been increasing alongside the possible consequences brought by successful attacks on these systems. This thesis tackles the issue of security of systems and especially focuses on compilation to achieve its goal. Compilation is the process of translating source programs written by humans to machine code readable by our systems. We explore the two possible behaviours of a secure compiler which are enforcement and preservation. First, we have developed CompCertSFI, a compiler which enforces the isolation of modules into closed memory areas called sandboxes. These modules are then unable to access memory regions outside of their sandbox which prevents any malicious module from corrupting other entities of the system. On the topic of security preservation, we defined a notion of Information Flow Preserving transformation to make sure that a program does get less secure during compilation. Our property is designed to preserve security against side-channel attacks. This new category of attacks uses physical mediums such as time or power consumption which are taken into account by current compilers

APA, Harvard, Vancouver, ISO, and other styles

12

Pop, Antoniu. "Leveraging streaming for deterministic parallelization : an integrated language, compiler and runtime approach." Paris, ENMP, 2011. http://www.theses.fr/2011ENMP0090.

Full text

Abstract:

La performance des unités de calcul séquentiel a atteint des limites technologiques qui ont conduit à une transition de la tendance à l'accélération des calculs séquentiels vers une augmentation exponentielle du nombre d'unités de calcul par microprocesseur. Ces nouvelles architectures ne permettent d'augmenter la vitesse de calcul que proportionnellement au parallélisme qui peut être exploité, soit via le modèle de programmation soit par un compilateur optimiseur. Cependant, la disponibilité du parallélisme en soi ne suffit pas à améliorer les performances si un grand nombre de processeurs sont en compétition pour l'accès à la mémoire. Le modèle de streaming répond à ce problème et représente une solution viable pour l'exploitation des architectures à venir. Cette thèse aborde le streaming comme un modèle général de programmation parallèle, plutôt qu'un modèle dédié à une classe d'applications, en fournissant une extension pour le streaming à un langage standard pour la programmation parallèle avec mémoire partagée, OpenMP. Un nouveau modèle formel est développé, dans une première partie, pour étudier les propriétés des programmes qui font appel au streaming, sans les restrictions qui sont généralement associées aux modèles de flot de données. Ce modèle permet de prouver que ces programmes sont déterministes à la fois fonctionnellement et par rapport aux deadlocks, ce qui est essentiel pour la productivité des programmeurs. La deuxième partie de ce travail est consacrée à l'exploitation efficace de ce modèle, avec support logiciel à l'exécution et optimisations de compilation, à travers l'implantation d'un prototype dans le compilateur GCC As single processing unit performance has reached a technological limit, the power wall, the past decade has seen a shift from the prevailing trend of increasing single-threaded performance to an exponentially growing number of processing units per chip. Higher performance returns on these newer architectures are contingent on the amount of parallelism that can be efficiently exploited in applications, either exposed through parallel programming or by parallelizing compilers. However, uncovering raw parallelism is insufficient if a host of cores vie for limited off-chip memory bandwidth. Mitigating the memory wall, the stream-computing model provides an important solution for exploiting upcoming architectures. This thesis explores streaming as a general-purpose parallel programming paradigm, rather than a model dedicated to a class of applications, by providing a highly expressive stream-computing extension to a de facto standard for shared memory programming, OpenMP. We rely on a new formal framework to investigate the properties of streaming programs, without the restrictions usually attached to dataflow models, and we prove that such programs benefit from deadlock and functional determinism, key assets in the productivity race. In a second part, we focus on the efficient exploitation of our model, with optimized runtime support and compiler optimizations, through an implementation in the GCC compiler

APA, Harvard, Vancouver, ISO, and other styles

13

Lelait, Sylvain. "Contribution à l'allocation de registres dans les boucles." Orléans, 1996. http://www.theses.fr/1996ORLE2039.

Full text

Abstract:

La génération de code est un des problèmes majeurs dans les compilateurs modernes en raison de l'évolution rapide des processeurs et de l'introduction de parallélisme interne entre instructions appelé parallélisme à grain fin. Nous nous sommes intéressés à la partie la plus sensible des programmes à savoir les boucles. En effet ce sont les instructions les plus exécutées dans un programme, et c'est donc là que les gains les plus significatifs du point de vue temps d'exécution peuvent être réalises. Dans notre cas, l'allocation de registres intervient après une phase d'ordonnancement des instructions par pipeline logiciel. Notre but a été d'étudier les interactions entre l'allocation de registres et le déroulage de boucles. Après avoir élaboré des heuristiques de coloriage pour les graphes d'intervalles circulaires, qui sont les graphes d'interférences issus du problème de l'allocation de registres dans les boucles, nous les avons comparées aux heuristiques existantes. Nous avons également pu observer le comportement du nombre chromatique de ces graphes en fonction du déroulage des boucles. Après cette étape où les insuffisances des graphes d'interférences usuels sont apparues, nous introduisons un nouveau graphe, baptise meeting graph, qui nous permet de résoudre le problème du déroulage optimal de la boucle. Après une étude des propriétés intrinsèques à ce graphe, nous présentons un algorithme complet d'allocation de registres incluant la gestion du code de vidage, ainsi qu'une méthode de minimisation du déroulage. Nous concluons ces applications du meeting graph par une application à une machine particulière, la cydra 5, pourvue d'un système original de registres. Nous proposons pour finir d'étendre notre méthode aux boucles multiples et avec conditionnelles.

APA, Harvard, Vancouver, ISO, and other styles

14

Ouy, Julien Talpin Jean-Pierre. "Génération de code asynchrone dans un environnement polychrone pour la production de systèmes GALS." [S.l.] : [s.n.], 2008. ftp://ftp.irisa.fr/techreports/theses/2008/ouy.pdf.

Full text

APA, Harvard, Vancouver, ISO, and other styles

15

Ouy, Julien. "Génération de code asynchrone dans un environnement polychrone pour la production de systèmes GALS." Rennes 1, 2008. ftp://ftp.irisa.fr/techreports/theses/2008/ouy.pdf.

Full text

Abstract:

Cette thèse propose une méthode de description et de mise en oeuvre de systèmes issus du modèle globalement asynchrone localement synchrone (GALS). Dans ce but, nous proposons tout d’abord une réinterprétation du modèle polychrone, modèle issu du synchrone et adapté pour gérer la concurrence d’instants en plus de la séquentialité. Après avoir observé des exemples de réseaux GALS nous en faisons l’analyse pour extraire les qualités que l’on attend d’un tel système et qu’il faut inclure dans notre travail. Avec ces nouveaux objectifs, nous proposons un schéma de synthèse de système basée sur la composition de processus élémentaires. Cette composition de processus est articulée autour de deux propriétés qui garantissent que ces processus peuvent fonctionner aussi bien de manière synchrone qu’asynchrone : la polyendochronie et l’isochronie. Ces propriétés sont obtenues sur les processus élémentaires lors de leur construction à partir des spécifications Signal idoines. Elles sont conservées jusqu’au système final grâce à leur compositionnabilité. Enfin, nous utilisons la propriété d’endochronie faible, garantie par la polyendochronie pour développer une technique de compilation des processus polyendochrones. Cette technique permet de compiler individuellement les composants pour ensuite les rassembler avec des communications asynchrones The purpose of this thesis is to offer a method for the correct description and the implementation of globally asynchronous locally synchronous systems (GALS). Therefore, we present an interpretation of the polychronous model of computation. More than the synchronous model, it permits to describe concurrency as well as sequentiality. Then, we observe and analyze different implementations of GALS systems to extract properties that we expect of such systems. We propose a method to synthesize systems by composition of basic processes. This composition uses two properties to ensure the equivalence between its synchronous and its asynchronous behaviours: Polyendochrony and Isochrony. Those two properties are compositional and are obtained by the basic processes from their appropriate Signal specifications. At last, we present a way to generate compiled code from poyendochronous processes already having the property of weak-endochrony. With this technique, it becomes possible to separately compile processes and then assemble them with asynchronous channels

APA, Harvard, Vancouver, ISO, and other styles

16

Floc'h, Antoine. "Compilation optimisante pour processeurs extensibles." Phd thesis, Université Rennes 1, 2012. http://tel.archives-ouvertes.fr/tel-00726420.

Full text

Abstract:

Les processeurs à jeu d'instructions spécifiques (ASIP) constituent un compromis entre les performances d'un circuit matériel dédié et la flexibilité d'un processeur programmable. Ces processeurs spécialisés peuvent être composés d'un processeur généraliste dont le jeu d'instructions est étendu par des instructions spécifiques à une ou plusieurs applications et qui sont exécutées sur une extension matérielle. On parle alors de processeurs extensibles. Si le coût de conception et de vérification de telles architectures est considérablement réduit en comparaison à une conception complète, la complexité est en partie reportée sur l'étape de compilation. En effet, le jeu d'instructions d'un processeur extensible est à la fois une entrée et une sortie du processus de compilation. Cette thèse propose plusieurs contributions pour guider le processus de conception de telles architectures à travers des techniques d'optimisations adaptées aux processeurs extensibles. La première de ces contributions consiste à sélectionner et à ordonnancer les instructions spécialisées VLIW en résolvant un unique problème d'optimisation de programmation par contraintes (CP). D'autre part, nous proposons une technique originale qui traite de l'interaction entre l'optimisation de code et l'extension de jeu d'instructions. Le principe est de transformer automatiquement le code original des nids de boucles d'un programme (à l'aide du modèle polyédrique) afin de sélectionner des instructions spécialisées vectorisables et dont les données temporaires, produites lors d'une itération de boucle, sont mémorisées sur l'extension matérielle du processeur.

APA, Harvard, Vancouver, ISO, and other styles

17

Brifault, Karine Geneviève. "Contribution à la compilation dynamique pour des jeux d'instructions multimédia." Versailles-St Quentin en Yvelines, 2005. http://www.theses.fr/2005VERS0002.

Full text

Abstract:

Compilation is a constantly evolving field, the participants of which are trying to take into account the improvement in CPU architectures. However, exploiting those new possibilities prove to be more and more difficult, as the complexity of CPU constantly increases, while the delay before each release of a new product range decreases. Present compilers are not yet able to take easily and efficiently advantage of the new possibilities offered. Indeed, most developpement languages have not yet implemented the fonctionnalities of the new instructions sets, which have proven to be able to significantly accelerate graphic applications or scientific computations. Those gaps in compiler technology prevent the programmers from easily optimizing their applications at minimal cost. During this thesis work, we studied optimization of multimedia applications on heterogeneous architectures from the point of view of compilation, in order to define a global framework for improvements. >From there, we geared our research towards the definition and implementation of a minimalist code generator : the compilet. Once the contribution of our compilets validated, and our experiments completed, we brought our research further by stufying and implementing a software cache adapted to dynamic code generation. In the future, we propose to pursue in this study, while expanding it to all relevant architectures and automating its use La compilation est un domaine en constant mouvement dont les acteurs cherchent à prendre en compte l'évolution permanente des architectures. Toutefois, il devient de plus en plus difficile d'exploiter les nouvelles ressources issues de cette évolution car la complexité des processeurs augmente et les temps de mise sur le marché de nouvelles gammes par les constructeurs se réduisent. Les compilateurs actuels ne sont pas encore en mesure d'exploiter facilement et efficacement toutes les possibilités offertes. En effet, la majeure partie des langages de programmation n'a toujours pas intégré les fonctionnalités des nouveaux jeux d'instructions, qui sont pourtant en mesure d'accélérer significativement les applications graphiques ou les calculs scientifiques. Ces lacunes des compilateurs ôtent aux développeurs du secteur des possibilités d'optimisation des applications à moindre coût. Au cours de ce travail de thèse, nous nous sommes intéressés à la problématique de l'optimisation des applications multimédia sur des architectures hétérogènes du point de vue de la compilation, afin de définir le cadre général des optimisations à apporter. De là, nous avons orienté notre recherche vers la définition et l'implémentation d'un générateur de code dynamique minimaliste, la compilette. Une fois la validation de l'apport de nos compilettes effectuée et nos expérimentations réalisées, nous avons pu approfondir cette recherche par l'étude et l'implémentation d'un cache logiciel adapté à la génération de code dynamique. A l'avenir, nous envisageons de poursuivre son étude, et de travailer à l'étendre sur toutes les architectures concernée, ainsi qu'à automatiser sa mise en place

APA, Harvard, Vancouver, ISO, and other styles

18

Baghdadi, Mohamed Riyadh. "Improving tiling, reducing compilation time, and extending the scope of polyhedral compilation." Electronic Thesis or Diss., Paris 6, 2015. http://www.theses.fr/2015PA066368.

Full text

Abstract:

Les processeurs multi-coeurs sont maintenant largement utilisés presque partout en informatique: ordinateurs de bureau, ordinateurs portables et accélérateurs tels que les GPGPU (General Purpose Graphics Processing Units). La difficulté de la programmation des systèmes parallèles est considérée comme un problème majeur qui va empêcher l'exploitation de leurs capacités dans le futur. Pour exploiter la puissance des processeurs multi-coeurs et les hiérarchies complexes de mémoire, il y a une grande nécessité pour utiliser des outils de parallélisation et d'optimisation automatique de code. L'optimisation polyédrique est un axe de recherche qui a comme but de résoudre ces problèmes. C'est est une représentation algébrique du programme et un ensemble d'analyses, de transformations et d'algorithmes de génération de code qui permettent à un compilateur de raisonner sur des transformations avancées de nids de boucle. Dans cette thèse, nous abordons certaines des limites du modèle polyédrique. Nous nous intéréssons particulièrement à trois problèmes et nous proposons des solutions pratiques à ces trois problèmes. Le premier problème est lié à la capacité d'appliquer l'optimisation de tuilage sur un code qui contient des fausses dépendances. Nous proposons une téchnique qui permet d'ignorer certaines fausses dépendences et donc qui permet d'appliquer l'optimisation de tuilage qui n'est pas possible sinon. Le second problème est lié au temps de compilation qui peut être trés long pour certains programmes. Nous proposons une téchnique qui transforme la représentation originale du programme à une nouvelle representation dans laquelle il y a moins d'instructions. L'optimisation de cette nouvelle représentation du programme est moins couteuse en terme de temps de compilation en comparaison avec l'optimisation de la représentation originale du programme. Le troisième problème est lié à deux limites: la première limite concerne la possibilité d'utiliser la compilation polyédrique sur des programmes qui ne resepectent pas les restrictions classiques du modèle polyédrique (un programme peut être représenté de façon précise dans le modèle polyédrique s'il ne contient pas des conditionnelles non-affines, des bornes de boucles non-affines et des accés non-affines). La seconde limite est liée à l'aptitude des outils à générer un code performant dans les performances se rapprochent des performances du code écrit à la main. Pour éviter ces deux limites, nous proposons un language de programmation que l'on appelle PENCIL, c'est un sous-ensemble de GNU C99 avec des règles de programmation spécifiques et quelques extensions. L'utilisation de ce sous-ensemble et l'utilisation de ces extensions permettent aux compilateurs de mieux exploiter le parallélisme et de mieux optimiser le code Multi-core processors are now in widespread use in almost all areas of computing: desktops, laptops and accelerators such as GPGPUs (General Purpose Graphics Processing Units). To harness the power of multi-core processors and complex memory hierarchies, the need for powerful compiler optimizations and especially loop nest transformations is now in high demand. The polyhedral optimization framework is showing promising results in addressing such a problem. It's an algebraic program representation and a set of analyses, transformations and code generation algorithms that enable a compiler to reason about advanced loop nest transformations addressing most of the parallelism and locality-enhancing challenges.In this thesis we address some of the limitations of the polyhedral framework. We address three problems and propose practical solutions to these three problems.The first problem is related to the ability to apply tiling on code that has false dependences (loop nest tiling is an optimization that changes the order of execution of statements in a loop nest in order to enhance data locality; false dependences are induced by the reuse of a single memory location to store multiple values during the life of the program). To preserve the validity of loop nest transformations and parallelization, data-dependences need to be analyzed. Memory dependences come in two varieties: true dependences (a.k.a. flow dependences) and false dependences (a.k.a. output and anti dependences). While true dependences must be satisfied in order to preserve the correct order of computations. False dependences reduce the degrees of freedom for loop transformations. In particular, loop tiling is severely limited in the presence of these dependences. While array expansion, a transformation that transforms scalars into arrays and arrays into higher dimensional arrays, removes all false dependences, the overhead of this transformation on memory and the detrimental impact on register-level reuse can be catastrophic. We propose and evaluate a compilation technique to safely ignore a large number of false dependences in order to enable loop nest tiling in the polyhedral model. It is based on the precise characterization of interferences between live range intervals, and it does not incur any scalar or array expansion.The second problem is related to the long compilation time that one may experience when using polyhedral tools to optimize a program. Particularly, the long execution time of the Pluto affine scheduling algorithm. The Pluto affine scheduling algorithm is the algorithm that is responsible for changing the schedule (order of execution) of statements in order to optimize the code (maximize parallelism and data locality). Reducing the execution time of this affine scheduling algorithm enhances the overall compilation time. We introduce and evaluate a technique called offline statement clustering. It is a practical technique designed to reduce the execution time of the Pluto affine scheduling algorithm without much loss in optimization opportunities. Using this technique, the statements of the program are clustered into macro-statements, the Pluto affine scheduling algorithm is then used to schedule the macro-statements instead of scheduling the original statements of the program. Since the number of macro-statements is less than the number of statements in the original program, scheduling the macro-statements is in general faster than scheduling the original statements of the program. We present the statement clustering algorithm, we show how offline statement clustering integrates transparently with the work-flow of a state-of-the-art polyhedral compiler and present two heuristics for choosing how statements should be clustered together. We show experimentally that statement clustering can reduce the scheduling time by a factor of 8x (in median) without a significant loss in optimization opportunities

APA, Harvard, Vancouver, ISO, and other styles

19

Pompougnac, Hugo. "Spécification et compilation de réseaux de neurones embarqués." Electronic Thesis or Diss., Sorbonne université, 2022. http://www.theses.fr/2022SORUS436.

Full text

Abstract:

Dans cette thèse, nous proposons une approche pour spécifier et compiler conjointement les aspects Calcul Haute Performance (HPC) et Temps-Réel Embarqué (RTE) d’un même système. Notre approche est fondée sur une intégration formelle, algorithmique et outillée entre deux formalismes sous-tendant une bonne partie des travaux en HPC et en RTE : le formalisme SSA et le langage flot de données synchrone Lustre. Le formalisme SSA est au cœur de bon nombre de compilateurs HPC, dont ceux employés par les frameworks d'apprentissage machine tels TensorFlow ou PyTorch. Le langage Lustre est au cœur des processus de mise en œuvre de systèmes embarqués critiques dans l’avionique, ou encore le rail In this thesis, we propose an approach for the joint specification and compilation of both High-Performance Computing (HPC) and Real-Time Embedded (RTE) aspects of a system. Our approach is based on a formal, algorithmic and tooled integration between two formalisms underlying a large part of works in HPC and RTE fields: the SSA formalism and the synchronous dataflow language Lustre. The SSA formalism is a key component of many HPC compilers, including those used by Machine Learning frameworks such as TensorFlow or PyTorch. The Lustre language is a key component of implementation processes of critical embedded systems in avionics or rail transportation

APA, Harvard, Vancouver, ISO, and other styles

20

Ait, Bensaid Samira. "Formal Semantics of Hardware Compilation Framework." Electronic Thesis or Diss., université Paris-Saclay, 2023. http://www.theses.fr/2023UPASG085.

Full text

Abstract:

Les analyses statiques de pire temps d’exécution sont utilisées pour garantir les délais requis pour les systèmes critiques. Afin d’estimer des bornes précises sur ces temps d’exécution, ces analyses temporelles nécessitent des considérations sur la (micro)- architecture. Habituellement, ces modèles de micro-architecture sont construits à la main à partir des manuels des processeurs. Cependant, les initiatives du matériel libre et les langages de description de matériel de haut niveau (HCLs), permettent de réaborder la problématique de la génération automatique de ces modèles de micro-architecture, et plus spécifiquement des modèles de pipeline. Nous proposons un workflow qui vise à construire automatiquement des modèles de chemin de données de pipeline à partir de conceptions de processeurs décrites dans des langages de contruction de matériel (HCLs). Notre workflow est basé sur la chaine de compilation matériel Chisel/FIRRTL. Nous construisons au niveau de la représentation intermédiaire les modèles de pipeline du chemin de données. Notre travail vise à appliquer ces modèles pour prouver des propriétés liées à la prédictibilité temporelle. Notre méthode repose sur la vérification formelle. Les modèles générés sont ensuite traduits en modèles formels et intégrés dans une procédure existante basée sur la vérification de modèles pour détecter les anomalies de temps. Nous utilisons le langage de modélisation et de vérification TLA+ et expérimentons notre analyse avec plusieurs processeurs RISC-V open-source. Enfin, nous faisons progresser les études en évaluant l’impact de la génération automatique à l’aide d’une série de critères synthétiques Static worst-case timing analyses are used to ensure the timing deadlines required for safety-critical systems. In order to derive accurate bounds, these timing analyses require precise (micro-)architecture considerations. Usually, such micro-architecture models are constructed by hand from processor manuals.However, with the open-source hardware initiatives and high-level Hardware Description Languages (HCLs), the automatic generation of these micro-architecture models and, more specifically, the pipeline models are promoted. We propose a workflow that aims to automatically construct pipeline datapath models from processor designs described in HCLs. Our workflow is based on the Chisel/FIRRTL Hardware Compiler Framework. We build at the intermediate representation level the datapath pipeline models. Our work intends to prove the timing properties, such as the timing predictability-related properties. We rely on the formal verification as our method. The generated models are then translated into formal models and integrated into an existing model checking-based procedure for detecting timing anomalies. We use TLA+ modeling and verification language and experiment with our analysis with several open-source RISC-V processors. Finally, we advance the studies by evaluating the impact of automatic generation through a series of synthetic benchmarks

APA, Harvard, Vancouver, ISO, and other styles

21

Reilles, Antoine. "Réécriture et compilation de confiance." Electronic Thesis or Diss., Vandoeuvre-les-Nancy, INPL, 2006. http://www.theses.fr/2006INPL084N.

Full text

Abstract:

La plupart des processus informatiques mettent en jeu la notion de transformation, en particulier la compilation. Nous nous intéressons dans cette thèse à fournir des outils et des méthodes, utilisant la réécriture, permettant d'accroître la confiance que l'on peut placer dans ces processus. Nous développons dans un premier temps un cadre permettant de valider la compilation de constructions de filtrage, produisant une preuve formelle de la validité de la compilation, ainsi qu'un témoin de cette preuve, à chaque exécution du compilateur. Afin de permettre l'écriture sûre de transformations complexes, nous proposons un générateur de structures de données efficaces intégrant des invariants algébriques, et un langage de stratégies permettant de contrôler l'application des transformations. Ces résultats constituent donc une avancée vers la constitution de methodes génériques sûres pour le développement de transformations de confiance Most computer processes involve the notion of transformation, in particular the compilation processes. We interest in this thesis in providing tools and methods, based on rewriting, giving the opportunity to increase the confidence we can place into those processes. We develop first a framework used to validate the compilation of matching constructs, building a formal proof of the validity of the compilation process along with a witness of this proof, for each run of the compiler. Then, in order to allow one to write safely complex transformations, we propose a tool that generates an efficient data structure integrating algebraic invariants, as well as a strategy language that enables to control the application of transformations. Those results can be seen as a first step towards the constitution of generic and safe methods for the development of trustworthy transformations

APA, Harvard, Vancouver, ISO, and other styles

22

Soula, Julien. "Principe de compilation d'un langage de traitement de signal." Lille 1, 2001. https://pepite-depot.univ-lille.fr/RESTREINT/Th_Num/2001/50376-2001-325.pdf.

Full text

Abstract:

Les applications de traitements de signal (TS) qu'on trouve notamment dans les chaines sonar, ont des caractéristiques algorithmiques bien particulières. Afin de répondre aux besoins de spécification et de standardisation de celles-ci, Thomson Marconi Sonar (TMS) a développé un langage orienté TS : ARRAY-OL (Array Oriented Language). Il permet de spécifier l'algorithme de calcul et les dépendances de données sans se soucier des problèmes de placement et d'ordonnancement. Nos travaux se situent au niveau de la compilation d'applications spécifiées en ARRAY-OL visant autant les stations de travail classiques que des machines dédiées à ARRAY-OL. La préexistence d'un support d'exécution ARRAY-OL nous a conduit à préférer une méthode de compilation par transformation des applications au niveau du langage plutôt que des stratégies d'implémentation directes. Pour mettre en place ces transformations, nous avons utilisé un formalisme approprié à la description du langage ARRAY-OL les opérateurs de distribution de tableaux (ODT). Ils nous ont permis de décrire formellement les transformations qui consiste à produire une ou plusieurs hiérarchies, à partir d'une séquence de tâches et de contrôler le grain de celles-ci. (. . . )Enfin l'environnement graphique GASPARD rend accessible ces outils à tous, et notamment aux développeurs d'applications TS, en permettant la création, la transformation et la compilation multi-plateformes d'applications ARRAY-OL de manière totalement graphique et interactive.

APA, Harvard, Vancouver, ISO, and other styles

23

Raimondi, Gautier. "Secure compilation against side channel attacks." Electronic Thesis or Diss., Université de Rennes (2023-....), 2023. http://www.theses.fr/2023URENS094.

Full text

Abstract:

De par leur omniprésence, la sécurité des systèmes informatiques est un enjeu majeur. Dans cette thèse, nous visons à garantir une sécurité contre un certain type d'attaque : les attaques par canal caché temporel. Ces attaques utilisent le temps d'exécution d'un programme pour déduire des informations sur le système. En particulier, on dit d'un programme qu'il est constant-time lorsqu'il n'est pas sensible à ce type d'attaques. Cela passe par des contraintes sur le programmes, qui ne doit ni réaliser de décisions en utilisant de valeurs secrètes, ni utiliser un de ces secrets pour accéder à la mémoire. Nous présentons dans ce document une méthode permettant de garantir la propriété constant-time d'un programme. Cette méthode est une transformation à haut niveau, suivi d'une compilation par Jasmin pour préserver la propriété. Nous présentons également la preuve de la sécurité et de la préservation sémantique de cette méthode Given their ubiquity, the security of computer systems is a major issue. In this thesis, we aim to guarantee security against a certain type of attack: timing side-channel attacks. These attacks use the execution time of a program to deduce information about the system. In particular, a program is said to be constant-time when it is not sensitive to this type of attack. This requires constraints on the program, which must neither make decisions using secret values, nor use one of these secrets to access memory. In this document, we present a method for guaranteeing the constant-time property of a program. This method is a high-level transformation, followed by compilation using Jasmin to preserve the property. We also present a proof of the security and semantic preservation of this method

APA, Harvard, Vancouver, ISO, and other styles

24

Lazure, Dominique. "Programmation géométrique à parallélisme de données : modèle, langage et compilation." Lille 1, 1995. http://www.theses.fr/1995LIL10021.

Full text

Abstract:

Le parallélisme de données permet l'exploitation efficace des machines massivement parallèles, en particulier lorsque le nombre d'unités de calcul dépasse le millier. Le programmeur manipule simultanément un grand nombre de données, en leur appliquant un traitement unique séquentiellement décrit. L'algorithmique scientifique accède au parallélisme par ce biais : la majorité des applications numériques intensives sont d'ores et déjà programmées en utilisant le paradigme du parallélisme de données. Nous proposons une approche géométrique de ce modèle de programmation. Les structures de données définies par l'utilisateur sont regroupées et alignées au sein d'une entité abstraite, référentiel de toute manipulation: l'hyper-espace. L'adoption d'une sémantique des expressions basée sur ce référentiel permet d'offrir au programmeur deux vues clairement distinctes : la vue microscopique permet l'expression du parallélisme de calcul ; la vue macroscopique permet les communications parallèles à travers l'hyper-espace par une modélisation à base de primitives géométriques. Cette séparation est importante pour la phase de génération de code. Nous montrons que l'hyper-espace est une information dont l'exploitation par le compilateur autorise l'introduction de nouvelles techniques d'optimisation du code exécutable. En particulier, l'allocation mémoire des objets est issue de l'attribution des ressources physiques aux points de l'hyper-espace. Le temps d'évaluation d'une expression est optimise par un abaissement sensible du temps d'accès aux données. La gestion de la boucle de virtualisation peut aussi profiter de la modélisation géométrique qui autorise la diminution du nombre d'itérations nécessaires au traitement d'une expression. Ces résultats sont illustres par des mesures de performances issues de l'atelier de développement produit durant cette thèse. Enfin, cette étude est étendue vers un domaine plus large. La problématique de la programmation hétérogène est abordée par l'association d'un hyper-espace à une machine du réseau hétérogène. L'étude de l'adéquation du modèle aux structures creuses a permis de proposer une approche originale du traitement de l'irrégularité des données, qui fournit au programmeur l'abstraction totale de la phase de compression.

APA, Harvard, Vancouver, ISO, and other styles

25

Borgna, Agustín. "Vers une formalisation d'une chaîne de compilation pour un ordinateur quantique." Electronic Thesis or Diss., Université de Lorraine, 2023. http://www.theses.fr/2023LORR0016.

Full text

Abstract:

L'avènement des ordinateurs quantiques capables de résoudre des problèmes irréalisables sur des ordinateurs classiques a motivé le développement de nouveaux langages et outils de programmation pour l'informatique quantique. Cependant, l'état de l'art actuel en matière de programmation quantique n'en est qu'à ses débuts. Dans cette thèse, nous présentons une série d'approches novatrices de différents aspects du processus de compilation quantique basé sur le calcul ZX. Tout d'abord, nous introduisons une nouvelle représentation intermédiaire pour les programmes quantiques capable d'encoder la récursion bornée et les structures de circuits répétés de manière compacte, basée sur les familles de l'extension Scalable du calcul ZX. Nous présentons ensuite un algorithme de compilation pour les circuits hybrides contenant à la fois des portes quantiques et classiques, basé sur l'optimisation de circuits purs de Duncan et al. Enfin, nous définissons le problème de la détection des sections de circuits quantiques qui peuvent être traduites en logique classique, et nous introduisons un algorithme heuristique pour le résoudre The advent of quantum computers capable of solving problems that are untractable on classical computers has motivated the development of new programming languages and tools for quantum computing. However, the current state of the art in quantum programming is still in its infancy. In this thesis, we present a series of novel approaches to different aspects of the quantum compilation process based on the ZX calculus. First, we introduce a new intermediate representation for quantum programs capable of encoding bounded recursion and repeated circuit structures in a compact way, based on families of the Scalable extension to the ZX calculus. We then present a compilation algorithm for hybrid circuits containing both quantum and classical gates, based on the pure circuit optimization by Duncan et al. Finally, we define the problem of detecting sections of a quantum circuit that can translated to classical logic, and introduce an heuristic algorithm to solve it

APA, Harvard, Vancouver, ISO, and other styles

26

Cros, Hervé. "Compilation et apprentissage dans les réseaux de contraintes." Montpellier 2, 2003. http://www.theses.fr/2003MON20171.

Full text

APA, Harvard, Vancouver, ISO, and other styles

27

Fournerie, Laurent. "Compilation et exécution multiflot de programmes fonctionnels parallèles sur calculateurs à mémoires distribuées." Toulouse, ENSAE, 1999. http://www.theses.fr/1999ESAE0009.

Full text

Abstract:

L'objectif de cette thèse est de proposer un environnement de programmation efficace et portable pour l'exécution parallèle de programmes fonctionnels paresseux. Ce travail s'inscrit dans une démarche qui vise à montrer l'intérêt et la validité de la programmation fonctionnelle paresseuse pour une meilleure exploitation des calculateurs parallèles sur des applications réelles. Outre leurs qualités importantes pour la programmation comme leur puissance d'expression, les langages fonctionnels possèdent en effet des propriétés intéressantes pour le calcul parallèle : l'unicité du résultat quel que soit le nombre de processus mis en jeu, par exemple, est une caractéristique fondamentale. Dans ce travail, nous avons défini un schéma de compilation vers un code intermédiaire dont la particularité est de concilier l'efficacité séquentielle avec les contraintes d'un environnement parallèle, puis un modèle d'exécution pour un environnement distribué qui repose sur une gestion multiflot du calcul capable de recouvrir la latence du réseau de communication. Les travaux présentés dans ce document ont donné lieu à la réalisation du système MaRS, composé d'un compilateur, d'un micro-noyau et d'un débogueur séquentiel. Un programme MaRS est destiné à être exécuté indifféremment sur des systèmes mono-processeurs ou multi-processeurs. Les tâches parallèles sont explicitement désignées en utilisant une simple annotation, mais la gestion du parallélisme est totalement transparente pour le programmeur, comme par exemple la gestion des données, la distribution des tâches ou la gestion dynamique des flots de calcul. Ainsi, le même programme, une fois compilé pour une plate-forme, peut s'exécuter indifféremment sur des partitions ayant un nombre de noeuds différents. Actuellement opérationnel sur plusieurs plate-formes, le système a permis le développement d'applications conséquentes et a montré sa capacité à réutiliser des codes existants tout en fournissant de réels gains d'efficacité.

APA, Harvard, Vancouver, ISO, and other styles

28

Kenmei, Youta Bénédicte Ramelie Clauss Philippe. "Génération de programmes modèles pour la représentation et l'analyse de profils d'exécution le modèle périodique-linéaire /." Strasbourg : Université Louis Pasteur, 2006. http://eprints-scd-ulp.u-strasbg.fr:8080/580/01/KENMEI_YOUTA2006.pdf.

Full text

APA, Harvard, Vancouver, ISO, and other styles

29

Carbon, Alexandre. "Accélération matérielle de la compilation à la volée pour les systèmes embarqués." Paris 6, 2013. http://www.theses.fr/2013PA066511.

Full text

Abstract:

Développée depuis le début des années 60, la compilation dynamique connaît un essor considérable depuis une quinzaine d’année. Cet essor est essentiellement lié à deux aspects : le dynamisme croissant des applications et l’explosion de la demande en solutions de virtualisation. Le transfert de ces problématiques dans le domaine de l’embarqué a conduit à éprouver les technologies de compilation dynamique sur des ressources de calculs spartiates. Toutefois, la gestion de ces algorithmes complexes et irréguliers par des architectures simples (exécution dans l’ordre, peu ou pas de spéculation, hiérarchies mémoire limitées), pose un important problème de passage à l’échelle en termes de performances. En conséquence, les solutions de compilation dynamique sont moins attractives dans ce domaine. Alors que de nombreuses optimisations logicielles ont déjà été proposées dans l’état de l’art, nous proposons, dans le cadre de cette thèse, de mettre en place des accélérations matérielles couplées au processeur en charge de la compilation dynamique afin d’en accroître les performances. Basées sur le compilateur du cadriciel LLVM (LLC), nos analyses ont permis d’identifier deux points critiques en performances : la gestion des tableaux associatifs et de l’allocation dynamique de la mémoire, et la gestion du graphe des instructions à compiler. Deux accélérations ont ainsi été proposées. Concernant la gestion des tableaux associatifs, nous obtenons des gains atteignant 25 % sur LLC pour un surcoût silicium représentant moins de 1. 4 % de la surface du processeur associé Developed since the 60s, JIT compilation is widely used since 15 years. This is the consequence of two main phenomena: the increasing dynamism of applications and the increasing demand concerning virtualization. The transfer of these issues to the embedded domain leads to experience JIT compilation on small and sparse resources. However, the management of JIT compilation algorithms’ complexity and irregularity on small resources (in-order processors, limited speculation, limited memory hierarchies) leads to important scaling-down problems in terms of performance. As a consequence, JIT compilation solutions are less attractive in this domain. While several software optimizations have been already proposed in the literature, we propose in this thesis the development of hardware accelerations coupled to the processor in charge of the JIT compilation. The final aim is to propose a more efficient solution in terms of performance with respect to embedded constraints. Based on the LLVM framework compiler (LLC), our experiments highlight two critical points in terms of performance: the associative array and dynamic memory allocation management and the instruction graph handling for instructions to compile and optimize. Two accelerators have been proposed in this way. Concerning the management of associative arrays, we obtain gains up to 25 % on LLC with an area overhead under 1. 4 % of the associated processor

APA, Harvard, Vancouver, ISO, and other styles

30

Charfi, Smaoui Asma. "Compilation optimisée des modèles UML." Phd thesis, Université Paris Sud - Paris XI, 2011. http://tel.archives-ouvertes.fr/tel-00659360.

Full text

Abstract:

Cette thèse s'inscrit dans le cadre de la mise en œuvre de l'ingénierie dirigée par les modèles (IDM) pour le développement des systèmes embarquées. Ces systèmes ayant généralement des ressources limitées (mémoire et/ou calculs), exigent que le code généré soit le plus optimisé possible. L'objectif de cette thèse est de produire à partir d'un modèle spécifié dans le langage UML, un code assembleur plus compact que le code assembleur produit par les compilateurs de code. Malgré l'évolution croissante des compilateurs optimisés, les compilateurs les plus répandus comme le GCC (Gnu Compiler Collection) sont incapables d'effectuer certains types d'optimisations qu'il est possible d'effectuer à un plus haut niveau d'abstraction dans une phase de pré-génération de code. En effet, certaines informations (liées à la sémantique d'exécution du langage UML) sont perdues lors de la génération de code. Ces informations, utiles pour les optimisations de haut niveau, sont invisibles par le compilateur de code vue qu'il prend toutes les informations liées au système modélisé à partir du code généré. Nous proposons ainsi une nouvelle approche dirigée par les modèles pour le développement des systèmes à ressources limitées, qui élimine l'étape de la génération de code en remplaçant cette étape par une compilation directe des modèles. Nous avons développé le premier compilateur de modèles UML (GUML : le front-end UML pour le compilateur GCC) qui génère directement de l'assembleur (sans passer par un langage de programmation) à partir des modèles UML. GUML permet de compiler les classes, les activités et les machines à états UML. Il permet de générer, en compilant certaines machines à états, un code assembleur plus compact que le code assembleur produit par GCC. Deux optimisations de GCC sont améliorées : l'élimination de code mort et l'élimination des expressions redondantes.

APA, Harvard, Vancouver, ISO, and other styles

31

Chevalier, Yannick. "Résolution de problèmes d'accessiblité pour la compilation et la validation de protocoles cryptographiques." Nancy 1, 2003. http://www.theses.fr/2003NAN10181.

Full text

Abstract:

La généralisation de transactions commerciales et des services sur des supports non-sécurisés a rendu nécessaire l'utilisation de protocoles permettant de garantir aux participants la confidentialité des données aussi bien que l'identification des correspondants. De nombreux protocoles proposés se sont révélés incorrects. Leur importance économique a motivé l'introduction de méthodes formelle pour la détection d'erreurs. Dans cette thèse, nous nous intéressons aux problèmes liés à l'analyse automatique de ces protocoles. Nous donnons une sémantique opérationnelle aux spécifications de haut niveau habituellement utilisées, étendons le cadre standard de l'analyse pour prendre en compte les propriétés des opérateurs algébriques pour la recherche de failles et considérons le problème de la vérification de protocoles. Nous réduisons ces problèmes à des problèmes d'accessibilité pour des systèmes de transitions définis par des règles de réécriture sur des ensembles. Cette réduction permet de donner la complexité de ces problèmes, et est une première étape vers une résolution par des outils entièrement automatiques Commercial transactions and services over insecure networks have lead to the use of security protocols. These protocols ought to provide both data confidentiality and participants authentication, but many of those proposed up to date have turned out to be flawed. Their economical importance has motivated the introduction of formal verification. In this dissertation, we investigate the problems raised by the automatic analysis of such protocols. We give an operationnal semantics to high-level protocol specifications, extend the standard Dolev-Yao framework to algebraic operators and finally consider the problem of protocol verification. We reduce these problems to reachability problems. This reduction is a first steptoward the implementation of an automatic analysis tool

APA, Harvard, Vancouver, ISO, and other styles

32

Bodin, Bruno. "Analyse d'Applications Flot de Données pour la Compilation Multiprocesseur." Phd thesis, Université Pierre et Marie Curie - Paris VI, 2013. http://tel.archives-ouvertes.fr/tel-00922578.

Full text

Abstract:

Les systèmes embarqués sont des équipements électroniques et informatiques, soumis à de nombreuses contraintes et dont le fonctionnement doit être continu. Pour définir le comportement de ces systèmes, les modèles de programmation dataflows sont souvent utilisés. Ce choix de modèle est motivé d'une part, parce qu'ils permettent de décrire un comportement cyclique, nécessaire aux systèmes embarqués ; et d'autre part, parce que ces modèles s'apprêtent à des analyses qui peuvent fournir des garanties de fonctionnement et de performance essentielles. La société Kalray propose une architecture embarquée, le MPPA. Il est accompagné du langage de programmation ΣC. Ce langage permet alors de décrire des applications sous forme d'un modèle dataflow déjà très étudié, le modèle Cyclo-Static Dataflow Graph(CSDFG). Cependant, les CSDFG générés par ce langage sont souvent trop complexes pour permettre l'utilisation des techniques d'analyse existantes. L'objectif de cette thèse est de fournir des outils algorithmiques qui résolvent les différentes étapes d'analyse nécessaires à l'étude d'une application ΣC, mais dans un temps d'exécution raisonnable, et sur des instances de grande taille. Nous étudions trois problèmes d'analyse distincts : le test de vivacité, l'évaluation du débit maximal, et le dimensionnement mémoire. Pour chacun de ces problèmes, nous fournissons des méthodes algorithmiques rapides, et dont l'efficacité a été vérifiée expérimentalement. Les méthodes que nous proposons sont issues de résultats sur les ordonnancements périodiques ; elles fournissent des résultats approchés et sans aucune garantie de performance. Pour pallier cette faiblesse, nous proposons aussi de nouveaux outils d'analyse basés sur les ordonnancements K-périodiques. Ces ordonnancements généralisent nos travaux d'ordonnancement périodiques et nous permettrons dans un avenir proche de concevoir des méthodes d'analyse bien plus efficaces.

APA, Harvard, Vancouver, ISO, and other styles

33

Cognard, Lucile. "Modélisation du comportement dynamique des processeurs pour la génération automatique de réordonnanceurs de code." Orléans, 1995. http://www.theses.fr/1995ORLE2038.

Full text

APA, Harvard, Vancouver, ISO, and other styles

34

Cayot, Robert-Olivier. "Récupération automatique d'erreurs syntaxiques en analyse discriminante rétrograde." Nice, 2001. http://www.theses.fr/2001NICE5690.

Full text

APA, Harvard, Vancouver, ISO, and other styles

35

Baghdadi, Mohamed Riyadh. "Improving tiling, reducing compilation time, and extending the scope of polyhedral compilation." Thesis, Paris 6, 2015. http://www.theses.fr/2015PA066368/document.

Full text

Abstract:

Les processeurs multi-coeurs sont maintenant largement utilisés presque partout en informatique: ordinateurs de bureau, ordinateurs portables et accélérateurs tels que les GPGPU (General Purpose Graphics Processing Units). La difficulté de la programmation des systèmes parallèles est considérée comme un problème majeur qui va empêcher l'exploitation de leurs capacités dans le futur. Pour exploiter la puissance des processeurs multi-coeurs et les hiérarchies complexes de mémoire, il y a une grande nécessité pour utiliser des outils de parallélisation et d'optimisation automatique de code. L'optimisation polyédrique est un axe de recherche qui a comme but de résoudre ces problèmes. C'est est une représentation algébrique du programme et un ensemble d'analyses, de transformations et d'algorithmes de génération de code qui permettent à un compilateur de raisonner sur des transformations avancées de nids de boucle. Dans cette thèse, nous abordons certaines des limites du modèle polyédrique. Nous nous intéréssons particulièrement à trois problèmes et nous proposons des solutions pratiques à ces trois problèmes. Le premier problème est lié à la capacité d'appliquer l'optimisation de tuilage sur un code qui contient des fausses dépendances. Nous proposons une téchnique qui permet d'ignorer certaines fausses dépendences et donc qui permet d'appliquer l'optimisation de tuilage qui n'est pas possible sinon. Le second problème est lié au temps de compilation qui peut être trés long pour certains programmes. Nous proposons une téchnique qui transforme la représentation originale du programme à une nouvelle representation dans laquelle il y a moins d'instructions. L'optimisation de cette nouvelle représentation du programme est moins couteuse en terme de temps de compilation en comparaison avec l'optimisation de la représentation originale du programme. Le troisième problème est lié à deux limites: la première limite concerne la possibilité d'utiliser la compilation polyédrique sur des programmes qui ne resepectent pas les restrictions classiques du modèle polyédrique (un programme peut être représenté de façon précise dans le modèle polyédrique s'il ne contient pas des conditionnelles non-affines, des bornes de boucles non-affines et des accés non-affines). La seconde limite est liée à l'aptitude des outils à générer un code performant dans les performances se rapprochent des performances du code écrit à la main. Pour éviter ces deux limites, nous proposons un language de programmation que l'on appelle PENCIL, c'est un sous-ensemble de GNU C99 avec des règles de programmation spécifiques et quelques extensions. L'utilisation de ce sous-ensemble et l'utilisation de ces extensions permettent aux compilateurs de mieux exploiter le parallélisme et de mieux optimiser le code Multi-core processors are now in widespread use in almost all areas of computing: desktops, laptops and accelerators such as GPGPUs (General Purpose Graphics Processing Units). To harness the power of multi-core processors and complex memory hierarchies, the need for powerful compiler optimizations and especially loop nest transformations is now in high demand. The polyhedral optimization framework is showing promising results in addressing such a problem. It's an algebraic program representation and a set of analyses, transformations and code generation algorithms that enable a compiler to reason about advanced loop nest transformations addressing most of the parallelism and locality-enhancing challenges.In this thesis we address some of the limitations of the polyhedral framework. We address three problems and propose practical solutions to these three problems.The first problem is related to the ability to apply tiling on code that has false dependences (loop nest tiling is an optimization that changes the order of execution of statements in a loop nest in order to enhance data locality; false dependences are induced by the reuse of a single memory location to store multiple values during the life of the program). To preserve the validity of loop nest transformations and parallelization, data-dependences need to be analyzed. Memory dependences come in two varieties: true dependences (a.k.a. flow dependences) and false dependences (a.k.a. output and anti dependences). While true dependences must be satisfied in order to preserve the correct order of computations. False dependences reduce the degrees of freedom for loop transformations. In particular, loop tiling is severely limited in the presence of these dependences. While array expansion, a transformation that transforms scalars into arrays and arrays into higher dimensional arrays, removes all false dependences, the overhead of this transformation on memory and the detrimental impact on register-level reuse can be catastrophic. We propose and evaluate a compilation technique to safely ignore a large number of false dependences in order to enable loop nest tiling in the polyhedral model. It is based on the precise characterization of interferences between live range intervals, and it does not incur any scalar or array expansion.The second problem is related to the long compilation time that one may experience when using polyhedral tools to optimize a program. Particularly, the long execution time of the Pluto affine scheduling algorithm. The Pluto affine scheduling algorithm is the algorithm that is responsible for changing the schedule (order of execution) of statements in order to optimize the code (maximize parallelism and data locality). Reducing the execution time of this affine scheduling algorithm enhances the overall compilation time. We introduce and evaluate a technique called offline statement clustering. It is a practical technique designed to reduce the execution time of the Pluto affine scheduling algorithm without much loss in optimization opportunities. Using this technique, the statements of the program are clustered into macro-statements, the Pluto affine scheduling algorithm is then used to schedule the macro-statements instead of scheduling the original statements of the program. Since the number of macro-statements is less than the number of statements in the original program, scheduling the macro-statements is in general faster than scheduling the original statements of the program. We present the statement clustering algorithm, we show how offline statement clustering integrates transparently with the work-flow of a state-of-the-art polyhedral compiler and present two heuristics for choosing how statements should be clustered together. We show experimentally that statement clustering can reduce the scheduling time by a factor of 8x (in median) without a significant loss in optimization opportunities

APA, Harvard, Vancouver, ISO, and other styles

36

Carcenac, Julien-Laurent. "Motifs arborescents pour données semi-structureés XML : compilation et applications." Université de Marne-la-Vallée, 2006. http://www.theses.fr/2006MARN0312.

Full text

Abstract:

La quantité de données disponibles au format XML, en tant que fichiers ou à travers les services web, pose le problème de sa manipulation. Exalead, société éditrice de logiciels de recherche, a choisi de développer pour ses propres besoins un langage de programmation "orienté-XML", le langage ExaScript. Ce langage unifie le modèle objet des langages de programmation impératifs et le modèle XML. En considérant les documents XML comme des objets, des manipulations de base viennent naturellement : construction d'un objet, accès et modification d'un champ. . . Toutefois, le paradigme de programmation impérative ne possède pas de primitive de manipulation avancée pour les objets complexes comme les arborescences XML. L'appariement de motif nous a paru le mécanisme le plus adapté pour exprimer des contraintes sur les objets XML et en sélectionner des sous-parties. La capacité de manipulation repose alors sur la simplicité de ces motifs et sur leur expressivité. Les contraintes imposées par ces motifs se doivent de capturer l'"essence" du XML en prenant en considération ses différents aspects : à la fois document textuel, arborescence étiquetée, chaîne de caractères. Cette thèse propose une algèbre de motifs arborescents adaptée au traitement des données semi-structurées XML. Cette algèbre a pour particularité d'unifier plusieurs aspects : lexical, grammatical, structurel et booléen. Nous établissons un schéma de compilation hiérarchique fondé sur des structures compilées simples : les évaluateurs booléens, les automates de caractères et une variante des automates classiques, les automates de classes d'identifiants. Nous présentons différentes applications réalisées à partir de notre algèbre de motifs et leurs implications sur les systèmes de recherche. Plusieurs applications de traitement du langage naturel, comme l'appariement de motifs linguistiques ou les outils de veille, peuvent être construites à partir d'un sous-ensemble de notre algèbre. Enfin, nous présentons l'intégration de cette algèbre dans le langage ExaScript, ainsi que son utilisation à des fins de détourage de pages interne

APA, Harvard, Vancouver, ISO, and other styles

37

Amini, Mehdi. "Transformations de programme automatiques et source-à-source pour accélérateurs matériels de type GPU." Phd thesis, Ecole Nationale Supérieure des Mines de Paris, 2012. http://pastel.archives-ouvertes.fr/pastel-00958033.

Full text

Abstract:

Depuis le début des années 2000, la performance brute des cœurs des processeurs a cessé son augmentation exponentielle. Les circuits graphiques (GPUs) modernes ont été conçus comme des circuits composés d'une véritable grille de plusieurs centaines voir milliers d'unités de calcul. Leur capacité de calcul les a amenés à être rapidement détournés de leur fonction première d'affichage pour être exploités comme accélérateurs de calculs généralistes. Toutefois programmer un GPU efficacement en dehors du rendu de scènes 3D reste un défi.La jungle qui règne dans l'écosystème du matériel se reflète dans le monde du logiciel, avec de plus en plus de modèles de programmation, langages, ou API, sans laisser émerger de solution universelle.Cette thèse propose une solution de compilation pour répondre partiellement aux trois "P" propriétés : Performance, Portabilité, et Programmabilité. Le but est de transformer automatiquement un programme séquentiel en un programme équivalent accéléré à l'aide d'un GPU. Un prototype, Par4All, est implémenté et validé par de nombreuses expériences. La programmabilité et la portabilité sont assurées par définition, et si la performance n'est pas toujours au niveau de ce qu'obtiendrait un développeur expert, elle reste excellente sur une large gamme de noyaux et d'applications.Une étude des architectures des GPUs et les tendances dans la conception des langages et cadres de programmation est présentée. Le placement des données entre l'hôte et l'accélérateur est réalisé sans impliquer le développeur. Un algorithme d'optimisation des communications est proposé pour envoyer les données sur le GPU dès que possible et les y conserver aussi longtemps qu'elle ne sont pas requises sur l'hôte. Des techniques de transformations de boucles pour la génération de code noyau sont utilisées, et même certaines connues et éprouvées doivent être adaptées aux contraintes posées par les GPUs. Elles sont assemblées de manière cohérente, et ordonnancées dans le flot d'un compilateur interprocédural. Des travaux préliminaires sont présentés au sujet de l'extension de l'approche pour cibler de multiples GPUs.

APA, Harvard, Vancouver, ISO, and other styles

38

Bachir, Mounira. "Minimisation du facteur de déroulage de boucle dans une allocation périodique de registres." Versailles-St Quentin en Yvelines, 2010. http://www.theses.fr/2010VERS0065.

Full text

Abstract:

La génération de code est un des problèmes majeurs dans les compilateurs modernes en raison de l'évolution rapide des processeurs et de l'introduction de parallélisme interne entre instructions appelé parallélisme à grain fin. Nous nous sommes intéressés a la partie la plus sensible des programmes à savoir les boucles. De nos jours, une phase d'ordonnancement des instructions appelé pipeline logiciel est devenue indispensable pour optimiser le code des boucles. Cette technique apporte des contraintes supplémentaires car des instructions de plusieurs itérations peuvent s'entremêler. Au sein de cette thèse, nous nous focalisons sur un objectif clair : comment générer un code compact pour une boucle ordonnancée avec la technique du pipeline logicielle? Le pipeline logiciel permet de générer des boucles hautement optimisées pour la vitesse d'exécution, mais au prix d'une forte expansion de code généré par le déroulage de la boucle engendré par la phase d'allocation périodique des registres. Minimiser ce degré de déroulage constitue notre objectif de recherche dans le volet de la minimisation de la taille de code sans perte de performance. Le déroulage de boucles doit être appliqué lorsque les variables de la boucle pipelinée logiciellement, sont en vie pendant plus d'une itération, ce qui accroît la taille du code. Le déroulage influence aussi les besoins en registres. Les outils SIRA et le Meeting Graph, développés dans cette optique, sont des environnements destinée à l'allocation périodique des registres. SIRA réalise l'allocation périodique des registres pour les boucles avant la phase du pipeline logiciel par contre le Meeting Graph réalise l'allocation périodique des registres pour les boucles après la phase du pipeline logiciel. Cependant, le degré de déroulage proposé, par ces deux méthodes, peut être très grand: Dans un premier volet, cette thèse propose de le minimiser après avoir formulé le problème. Notre solution mathématique montre comment calculer le degré de déroulage minimal en utilisant les registres restants après la phase d'allocation périodique des registres. Nous avons implémenté cette solution dans SIRA et le Meeting Graph qui proposent dorénavant une allocation périodique de registres avec un degré de déroulage minimal. Les statistiques sur les résultats de nos expériences montrent qu'en pratique le degré de déroulage minimal trouvé par notre solution est acceptable. Comme ces résultats ne prennent en compte qu'un seul type de registre, nous avons aussi généralisé cette solution pour des processeurs qui ont plusieurs types de registres. Nous avons appliqué la solution sur les codes de ST-Microelectronics, après avoir intégré la nouvelle version de SIRA dans le LAO (compilateur de ST-Microelectronics). Cependant, quelques degrés de déroulage restent grands. Pour pallier ce problème, la deuxième partie de cette thèse étudie la minimisation du degré de déroulage par le rajout de move operations sans compromettre le parallélisme entre instructions. Une étude expérimentale sur plusieurs boucles, montre que la technique de renommage de registres sans altérer les performances, minimise le degré de déroulage des boucles This thesis addresses the problem of generating compact code from software pipelined loops. Although software pipelining is a powerful technique to extract fine-grain parallelism, it generates lifetime intervals spanning multiple loop iterations. These intervals require periodic register allocation (also called variable expansion), which in turn yields a code generation challenge. We are looking for the minimal unrolling factor enabling the periodic register allocation of software pipelined kernels. This challenge is generally addressed through one of: (1) hardware support in the form of rotating register files, which solve the unrolling problem but are expensive in hardware; (2) register renaming by inserting register moves, which increase the number of operations in the loop, and may damage the schedule of the software pipeline and reduce throughput; (3) post-pass loop unrolling that does not compromise throughput but often leads to impractical code growth. The latter approach relies on the proof that MAXLIVE registers are sufficient for periodic register allocation ; yet the only heuristic to control the amount of post-pass loop unrolling does not achieve this bound or leads to undesired register spills. This thesis gathers our extensive research results on the open problem of minimal loop unrolling allowing a software-only code generation that does not trade the optimality of the initiation interval (II) for the compactness of the generated code. At the first part of this thesis, we propose to use the remaining free registers after periodic register allocation to relax the constraints on register reuse. We show that the problem of minimal loop unrolling arises either before or after software pipelining, either with a single or with multiple register types. We provide a formal problem definition for each situation, and we propose and study a dedicated algorithm for each problem. These solutions are implemented within an industrial-strength compiler for a VLIW embedded processor from STMicroelectronics (ST2xx processor family). Our large-scale experiments on multiple benchmarks family (LAO, FFMPEG, MEDIABENCH, SPEC2000, SPEC2006) demonstrate the effectiveness of the proposed unroll degree minimisation, both in terms of code size and in terms of initiation intervals, along with satisfactory compilation times. Nevertheless, some loops still require high unrolling degrees even after our minimisation. At the second part of this thesis, we study, for these occasional high unrolling degrees, the potential for live range splitting to reduce kernel loop unrolling with details of how to introduce new move instructions without inscreasing II. In fact, extra move instructions can be added where the software pipelining schedule leaves some free units to carry the information between the splitted variables. Concerning the experimental evaluation, we carefully studied the efficiency of this method in standalone context. The different experiments show that the exhaustive solution for splitting variables produce dramatic positive results

APA, Harvard, Vancouver, ISO, and other styles

39

Fau, Simon. "Systèmes de cryptocalculs, compilation et support d’exécution." Thesis, Lorient, 2016. http://www.theses.fr/2016LORIS398/document.

Full text

Abstract:

Notre approche dans cette thèse était d'identifier où le chiffrement complètement homomorphe (FHE) pouvait être utilisé pour le domaine des sciences informatiques et de construire une plate-forme expérimentale qui nous permette de tester des algorithmes de traitement de l'information manipulant des données chiffrées. La première partie de cette thèse est consacrée à l'état de l'art. Nous présentons d'abord les systèmes de chiffrement homomorphes conçus avant 2008, puis nous présentons ceux adressant la problématique du chiffrement complètement homomorphe. Nous décrivons plusieurs méthodes de chiffrement d'intérêt pour cette thèse et discutons de leurs implémentations FHE. Enfin, nous présentons des circuits de Yao car ils peuvent résoudre des problèmes similaires que le FHE et nous parlons brièvement du chiffrement fonctionnel (FE). La deuxième partie de cette thèse présente nos contributions. Nous commençons par expliquer comment le FHE peut être utile dans divers scénarios et décrivons plusieurs cas d'utilisation pratique identifiés au cours de la thèse. Ensuite, nous décrivons notre approche pour effectuer des calculs sur des données chiffrées à l'aide du FHE et expliquons comment nous avons pu développer une plate-forme pour l'exécution dans le domaine chiffré d'une large gamme d'algorithmes en s'appuyant seulement sur l'addition et la multiplication homomorphes. Nous détaillons ensuite notre solution pour effectuer des requêtes privées sur une base de données chiffrées en utilisant le chiffrement homomorphe. Dans un dernier chapitre, nous présentons nos résultats expérimentaux Our approach in this thesis was to identify where FHE could be used in computer science and to build an experimental platform that allow us to test real-life algorithm running on homomorphically-encrypted data. The first part of this thesis is dedicated to the state of the art. We first present homomorphic encryption schemes designed before 2008 and then move to the Fully Homomorphic Encryption period. We describe several schemes of interest for this thesis and discuss FHE implementations. Finally, we present Yao’s garbled circuits as they can solve similar problems as FHE and briefly talk about Functional Encryption (FE). The second part of this thesis is for our contributions to the subject. We begin by explaining how FHE can be useful in various scenarios and try to provide practical use cases that we identified during the thesis. Then, we describe our approach to perform computations on encrypted data using FHE and explain how we were able to build on just the homomorphic addition and multiplication a platform for the execution in the encrypted domain of a wide range of algorithms. We then detail our solution for performing private queries on an encrypted database using homomorphic encryption. In a final chapter, we present our experimental results

APA, Harvard, Vancouver, ISO, and other styles

40

Didier, Keryan. "Contributions to the safe and efficient parallelisation of hard real-time systems." Electronic Thesis or Diss., Sorbonne université, 2019. http://www.theses.fr/2019SORUS485.

Full text

Abstract:

L'implémentation de systèmes temps-réel implique de nombreuses étapes qui sont jusqu'aujourd'hui faites manuellement. La complexité de tels systèmes et celle des plateformes matérielles sur lesquelles ils s'exécutent rendent de plus en plus difficile d'assurer la correction de ces étapes de conception (en particulier dans de cadre d'exécutions sur plateformes multi-cœurs). Cela rend l'automatisation de tout le processus d'implémentation inévitable. Cette thèse propose une méthode de parallélisation automatique de systèmes temps-réel. La méthode rapproche les domaines du temps-réel et de la compilation en intégrant les étapes de parallélisation, d'ordonnancement, d'allocation mémoire et de génération de code autour d'une analyse et d'un modèle temporel précis qui s'appuient sur des hypothèses fortes sur la plateforme d'exécution et la forme du code généré. Cette thèse propose également un modèle d'implémentation pour du logiciel flot-de-données multithreadé. En utilisant la même base formelle que précédemment (les formalismes flot-de-données synchrones), un modèle représente une implémentation multithreadé dans un langage comme Lustre, étendu avec des annotations de mapping. Cette modélisation permet un raisonnement formel de toutes les décisions d'implémentation et nous proposons une approche vers la preuve de correction de leur fonctionnalité en rapport à leurs spécifications The implementation of hard real-time systems involves a lot of steps that are traditionally manual. The growing complexity of such systems and hardware platforms on which they are executed makes increasingly difficult to ensure the correctness of those steps, in particular for the timing properties of the system on multi-core platform. This leads to the need for automation of the whole implementation process. In this thesis, we provide a method for automatic parallel implementation of real-time systems. The method bridge the gap between real-time systems implementation and compilation by integrating parallelization, scheduling, memory allocation, and code generation around a precise timing model and analysis that rely on strong hypothesis on the execution platform and the form of the generated code. The thesis also provides an implementation model for dataflow multithreaded software. Using the same formal ground as the first contribution, the dataflow synchronous formalisms, the model represents multithreaded implementations in a Lustre-like language extended with mapping annotations. This model allows formal reasoning on the correctness of all the mapping decisions used to build the implementation. We propose an approach toward the proof of correctness of the functionality of the implementation with respect to the functional specifications

APA, Harvard, Vancouver, ISO, and other styles

41

Josset, François-Xavier. "Spécification et compilation d'un langage de haut niveau pour l'optimisation combinatoire : CLAIRE vers Java." Versailles-St Quentin en Yvelines, 2002. http://www.theses.fr/2002VERS010V.

Full text

Abstract:

Après une longue hégémonie des langages procéduraux, la programmation orientée-objet s'impose progressivement comme la technologie d'excellence pour le génie logiciel. Le développement de telles applications reste cependant délicat, tant les problèmes traités peuvent être complexes et hétérogènes, et les langages de programmation orientée-objet parfois mal appropriés. De nouveaux outils et de nouvelles méthodes d'aide au développement sont régulièrement proposés, ainsi que des langages de plus en plus ouverts et performants. Cette thèse s'inscrit dans le cadre de la spécifification et de la compilation de CLAIRE, un langage de programmation orientée-objet de haut niveau, offrant des objets réflexifs, des types étendus, des fonctions paramétriques et polymorphes, des ensemnles concrets et abstraits, des règles de production et des primitives pour le raisonnement hypothétique. Ce langage, plus spécialement dédié à l'écriture d'algorithmes hybrides pour les problèmes d'optimisation combinatoire, vient avec un environnement de programmation complet réconciliant expresivité et efficacité. CLAIRE étant une plate-forme de développement amenée à évoluer, une nouvelle version est proposée avec des collections originales, un riche système de types permettant un typage fort, sûr et flexible, et la possibilité de générer des programmes Java lisibles et maintenables. De plus, un outil de calculs statiques de métriques permet d'établir la qualité des applications CLAIRE, d'identifier leurs faiblesses et de visualiser graphiquement les améliorations réalisées au cours des différentes versions. La combinaison entre la nouvelle plate-forme et l'outil de mesures de qualité assure une plus grande maîtrise des développements en CLAIRE.

APA, Harvard, Vancouver, ISO, and other styles

42

Heydemann, Karine. "Schéma global de compilation sous contraintes pour la recherche de compromis entre la taille d'une application et sa performance." Rennes 1, 2004. http://www.theses.fr/2004REN10148.

Full text

Abstract:

L'enjeu de la conception des systèmes enfouis est de réaliser un produit attractif pour un coût minimum. Techniquement il s'agit d'obtenir une performance maximale avec unetaille de code minimale. La génération du code des applications doit gérer deux objectifs généralement antagonistes : accroître les performances et réduire la taille descodes. Nous montrons dans cette thèse que des stratégies de compilation globales et efficaces sont nécessaires pour maximiser la performance sous contraintes de taille et inversement pour minimiser la taille sous contrainte de performances. Nous proposons ensuite un algorithme général de calcul automatique de compromis. Finalement, nous montrons que l'ensemble des techniques proposées permet de trouver des compromis de bonne qualité, répondant ainsi aux besoins de la mise en oeuvre des applications enfouies.

APA, Harvard, Vancouver, ISO, and other styles

43

Dumont, Philippe Boulet Pierre. "Spécification multidimensionnelle pour le traitement du signal systématique." Villeneuve d'Ascq : Université des sciences et technologies de Lille, 2007. https://iris.univ-lille1.fr/dspace/handle/1908/363.

Full text

Abstract:

Reproduction de : Thèse de doctorat : Informatique : Lille 1 : 2005. N° d'ordre (Lille 1) : 3756. Résumé en français et en anglais. Titre provenant de la page de titre du document numérisé. Bibliogr. p. 119-122.

APA, Harvard, Vancouver, ISO, and other styles

44

Nganyewou, Tidjon Lionel. "Modélisation formelle des systèmes de détection d'intrusions." Electronic Thesis or Diss., Institut polytechnique de Paris, 2020. http://www.theses.fr/2020IPPAS021.

Full text

Abstract:

L'écosystème de la cybersécurité évolue en permanence en termes du nombre, de la diversité, et de la complexité des attaques. De ce fait, les outils de détection deviennent inefficaces face à certaines attaques. On distingue généralement trois types de système de détection d'intrusions: détection par anomalies, détection par signatures et détection hybride. La détection par anomalies est fondée sur la caractérisation du comportement habituel du système, typiquement de manière statistique. Elle permet de détecter des attaques connues ou inconnues, mais génère aussi un très grand nombre de faux positifs. La détection par signatures permet de détecter des attaques connues en définissant des règles qui décrivent le comportement connu d'un attaquant. Cela demande une bonne connaissance du comportement de l'attaquant. La détection hybride repose sur plusieurs méthodes de détection incluant celles sus-citées. Elle présente l'avantage d'être plus précise pendant la détection. Des outils tels que Snort et Zeek offrent des langages de bas niveau pour l'expression de règles de reconnaissance d'attaques. Le nombre d'attaques potentielles étant très grand, ces bases de règles deviennent rapidement difficiles à gérer et à maintenir. De plus, l'expression de règles avec état dit stateful est particulièrement ardue pour reconnaître une séquence d'événements. Dans cette thèse, nous proposons une approche stateful afin d'identifier des attaques complexes. Nous considérons l'approche diagramme état-transition hiérarchique, en utilisant les ASTDs. Les ASTDs permettent de représenter de façon graphique et modulaire une spécification, ce qui facilite la maintenance et la compréhension des règles. Nous étendons la notation ASTD avec de nouvelles fonctionnalités pour représenter des attaques complexes. Ensuite, nous spécifions plusieurs attaques avec la notation étendue et exécutons les spécifications obtenues sur des flots d'événements à l'aide d'un interpréteur pour identifier des attaques. Nous évaluons aussi les performances de l'interpréteur avec des outils industriels tels que Snort et Zeek. Puis, nous réalisons un compilateur afin de générer du code exécutable à partir d'une spécification ASTD, capable d'identifier efficacement les séquences d'événements The cybersecurity ecosystem continuously evolves with the number, the diversity, and the complexity of cyber attacks. Generally, we have three IDS types: anomaly-based detection, signature-based detection, and hybrid detection. Anomaly detection is based on the usual behavior description of the system, typically in a static manner. It enables detecting known or unknown attacks, but generating also a large number of false positives. Signature based detection enables detecting known attacks by defining rules that describe known attacker's behavior. It needs a good knowledge of attacker behavior. Hybrid detection relies on several detection methods including the previous ones. It has the advantage of being more precise during detection. Tools like Snort and Zeek offer low level languages to represent rules for detecting attacks. The number of potential attacks being large, these rule bases become quickly hard to manage and maintain. Moreover, the representation of stateful rules to recognize a sequence of events is particularly arduous. In this thesis, we propose a stateful approach to identify complex attacks. We consider the hierarchical state-transition diagram approach, using the ASTDs. ASTDs allow a graphical and modular representation of a specification that facilitates maintenance and understanding of rules. We extend the ASTD notation with new features to represent complex attacks. Next, we specify several attacks with the extended notation and run the resulting specifications on event streams using an interpreter to identify attacks. We also evaluate the performance of the interpreter with industrial tools such as Snort and Zeek. Then, we build a compiler in order to generate executable code from an ASTD specification, able to efficiently identify sequences of events

APA, Harvard, Vancouver, ISO, and other styles

45

Lomüller, Victor. "Générateur de code multi-temps et optimisation de code multi-objectifs." Thesis, Grenoble, 2014. http://www.theses.fr/2014GRENM050/document.

Full text

Abstract:

La compilation est une étape indispensable dans la création d'applications performantes.Cette étape autorise l'utilisation de langages de haut niveau et indépendants de la cible tout en permettant d'obtenir de bonnes performances.Cependant, de nombreux freins empêchent les compilateurs d'optimiser au mieux les applications.Pour les compilateurs statiques, le frein majeur est la faible connaissance du contexte d'exécution, notamment sur l'architecture et les données utilisées.Cette connaissance du contexte se fait progressivement pendant le cycle de vie de l'application.Pour tenter d'utiliser au mieux les connaissances du contexte d'exécution, les compilateurs ont progressivement intégré des techniques de génération de code dynamique.Cependant ces techniques ne se focalisent que sur l'utilisation optimale du matériel et n'utilisent que très peu les données.Dans cette thèse, nous nous intéressons à l'utilisation des données dans le processus d'optimisation d'applications pour GPU Nvidia.Nous proposons une méthode utilisant différents moments pour créer des bibliothèques adaptatives capables de prendre en compte la taille des données.Ces bibliothèques peuvent alors fournir les noyaux de calcul les plus adapté au contexte.Sur l'algorithme de la GEMM, la méthode permet d'obtenir des gains pouvant atteindre 100~\% tout en évitant une explosion de la taille du code.La thèse s'intéresse également aux gains et coûts de la génération de code lors de l'exécution, et ce du point de vue de la vitesse d'exécution, de l'empreinte mémoire et de la consommation énergétique.Nous proposons et étudions 2 approches de génération de code à l'exécution permettant la spécialisation de code avec un faible surcoût.Nous montrons que ces 2 approches permettent d'obtenir des gains en vitesse et en consommation comparables, voire supérieurs, à LLVM mais avec un coût moindre Compilation is an essential step to create efficient applications.This step allows the use of high-level and target independent languages while maintaining good performances.However, many obstacle prevent compilers to fully optimize applications.For static compilers, the major obstacle is the poor knowledge of the execution context, particularly knowledge on the architecture and data.This knowledge is progressively known during the application life cycle.Compilers progressively integrated dynamic code generation techniques to be able to use this knowledge.However, those techniques usually focuses on improvement of hardware capabilities usage but don't take data into account.In this thesis, we investigate data usage in applications optimization process on Nvidia GPU.We present a method that uses different moments in the application life cycle to create adaptive libraries able to take into account data size.Those libraries can therefore provide more adapted kernels.With the GEMM algorithm, the method is able to provide gains up to 100~\% while avoiding code size explosion.The thesis also investigate runtime code generation gains and costs from the execution speed, memory footprint and energy consumption point of view.We present and study 2 light-weight runtime code generation approaches that can specialize code.We show that those 2 approaches can obtain comparable, and even superior, gains compared to LLVM but at a lower cost

APA, Harvard, Vancouver, ISO, and other styles

46

Alkhodre, Ahmad Badreddin. "Développement formel de systèmes temps réel à l'aide de SDL et IF ( Compilation pour système temps réel )." Lyon, INSA, 2004. http://theses.insa-lyon.fr/publication/2004ISAL0052/these.pdf.

Full text

Abstract:

Un système temps réel est un système qui interagit avec un environnement physique en remplissant souvent des missions critiques (une faute du système peut avoir des conséquences graves). Il sera dit correct s'il possède les bonnes fonctionnalités réalisées à temps (contraintes temporelles imposées par l’environnement ou par l’utilisateur). La validation fonctionnelle et temporelle de ces systèmes est une nécessité forte (fournisse des résultats fiables). Dans le cadre des implémentations à base d’exécutifs multitâche temps réel, le travail présenté dans cette thèse tente d’apporter une approche complète formelle de la suite spécification, conception et implémentation. Dans ce cadre, il porte aussi un intérêt particulier à une méthode de validation de la transformation entre le modèle de contraintes et le modèle d'exécution. Nous formalisons plus particulièrement des phases de spécification et la conception en utilisant le langage formel SDL. Ensuite, nous précisons explicitement les contraintes temps réel à nos modèles en utilisant le langage IF. Enfin, nous montrons formellement comment la correction du développement d’une application est prouvée Real Time system (RTS) is a system which interacts strongly with a physical process. It is subject to strong reliability and real time constraints and to ensure the respect of the real time constraints, it is necessary o use formal languages and techniques. SDL seems to be a good candidate for the RTS development: it is a formal standardized language dedicated to distribute systems. Moreover, several works have been done to extend its use for Real Time and dedicated systems. On the basis of the SDL language, this thesis proposed a framework for the specification, design and behavioural validation of a Real-Time System supported by multitasking real-time operating systems. The specification and a design stages are formalized on the basis of the SDL specialization. To explicit the real time constraints, a precise semantic is given thanks to the IF language. Afterwards, it is shown how the correctness of an application can be formally checked

APA, Harvard, Vancouver, ISO, and other styles

47

Ramananandro, Tahina. "Les objets en C + + : sémantique formelle mécanisée et compilation vérifiée." Phd thesis, Université Paris-Diderot - Paris VII, 2012. http://tel.archives-ouvertes.fr/tel-00769044.

Full text

Abstract:

C++ est un des langages de programmation les plus utilisés en pratique, y compris pour le logiciel embarqué critique. C'est pourquoi la vérication de programmes écrits en C++ devient intéressante, en particulier via l'utilisation de méthodes formelles. Pour cela, il est nécessaire de se fonder sur une sémantique formelle de C++. De plus, une telle sémantique formelle peut être validée en la prenant comme base pour la spécication et la preuve d'un compilateur C++ réaliste, afin d'établir la confiance dans les techniques usuelles des compilateurs C++. Dans cette thèse, nous nous focalisons sur le modèle objet de C++. Nous proposons une sémantique formelle de l'héritage multiple en C++ comprenant les structures imbriquées à la C, sur laquelle s'appuie notre étude de la représentation concrète des objets avec optimisations des bases vides, à travers des conditions suffisantes que nous prouvons correctes vis-à-vis des accès aux champs et des opérations polymorphes. Puis nous spécifions un algorithme de représentation en mémoire fondé sur l'ABI pour Itanium, et une extension de cet algorithme avec optimisations des champs vides, et nous prouvons qu'ils satisfont nos conditions. Nous obtenons alors un compilateur vérifié et réaliste d'un sous-ensemble de C++ vers un langage à trois adresses et accès mémoire de bas niveau. Rajoutant à notre sémantique la construction et la destruction d'objets, nous étudions leurs interactions avec l'héritage multiple. Cela nous permet de formaliser la gestion de ressources, notamment le principe RAII (resource acquisition is initialization) via l'ordre de construction et destruction des sous-objets. Nous étudions aussi les effets sur les opérations polymorphes telles que la sélection de fonction virtuelle pendant la construction et la destruction, en généralisant la notion de type dynamique. Nous obtenons alors un compilateur vérifié pour notre sémantique étendue, notamment en prouvant la correction de l'implémentation des changements de types dynamiques. Toutes nos spécifications et preuves sont formalisées en Coq.

APA, Harvard, Vancouver, ISO, and other styles

48

Maroneze, André Oliveira. "Certified Compilation and Worst-Case Execution Time Estimation." Thesis, Rennes 1, 2014. http://www.theses.fr/2014REN1S030/document.

Full text

Abstract:

Les systèmes informatiques critiques - tels que les commandes de vol électroniques et le contrôle des centrales nucléaires - doivent répondre à des exigences strictes en termes de sûreté de fonctionnement. Nous nous intéressons ici à l'application de méthodes formelles - ancrées sur de solides bases mathématiques - pour la vérification du comportement des logiciels critiques. Plus particulièrement, nous spécifions formellement nos algorithmes et nous les prouvons corrects, à l'aide de l'assistant à la preuve Coq - un logiciel qui vérifie mécaniquement la correction des preuves effectuées et qui apporte un degré de confiance très élevé. Nous appliquons ici des méthodes formelles à l'estimation du Temps d'Exécution au Pire Cas (plus connu par son abréviation en anglais, WCET) de programmes C. Le WCET est une propriété importante pour la sûreté de fonctionnement des systèmes critiques, mais son estimation exige des analyses sophistiquées. Pour garantir l'absence d'erreurs lors de ces analyses, nous avons formellement vérifié une méthode d'estimation du WCET fondée sur la combinaison de deux techniques principales: une estimation de bornes de boucles et une estimation du WCET via la méthode IPET (Implicit Path Enumeration Technique). L'estimation de bornes de boucles est elle-même décomposée en trois étapes : un découpage de programmes, une analyse de valeurs opérant par interprétation abstraite, et une méthode de calcul de bornes. Chacune de ces étapes est formellement vérifiée dans un chapitre qui lui est dédiée. Le développement a été intégré au compilateur C formellement vérifié CompCert. Nous prouvons que le résultat de l'estimation est correct et nous évaluons ses performances dans des ensembles de benchmarks de référence dans le domaine. Les contributions de cette thèse incluent la formalisation des techniques utilisées pour estimer le WCET, l'outil d'estimation lui-même (obtenu à partir de la formalisation), et l'évaluation expérimentale des résultats. Nous concluons que le développement fondé sur les méthodes formelles permet d'obtenir des résultats intéressants en termes de précision, mais il exige des précautions particulières pour s'assurer que l'effort de preuve reste maîtrisable. Le développement en parallèle des spécifications et des preuves est essentiel à cette fin. Les travaux futurs incluent la formalisation de modèles de coût matériel, ainsi que le développement d'analyses plus sophistiquées pour augmenter la précision du WCET estimé Safety-critical systems - such as electronic flight control systems and nuclear reactor controls - must satisfy strict safety requirements. We are interested here in the application of formal methods - built upon solid mathematical bases - to verify the behavior of safety-critical systems. More specifically, we formally specify our algorithms and then prove them correct using the Coq proof assistant - a program capable of mechanically checking the correctness of our proofs, providing a very high degree of confidence. In this thesis, we apply formal methods to obtain safe Worst-Case Execution Time (WCET) estimations for C programs. The WCET is an important property related to the safety of critical systems, but its estimation requires sophisticated techniques. To guarantee the absence of errors during WCET estimation, we have formally verified a WCET estimation technique based on the combination of two main methods: a loop bound estimation and the WCET estimation via the Implicit Path Enumeration Technique (IPET). The loop bound estimation itself is decomposed in three steps: a program slicing, a value analysis based on abstract interpretation, and a loop bound calculation stage. Each stage has a chapter dedicated to its formal verification. The entire development has been integrated into the formally verified C compiler CompCert. We prove that the final estimation is correct and we evaluate its performances on a set of reference benchmarks. The contributions of this thesis include (a) the formalization of the techniques used to estimate the WCET, (b) the estimation tool itself (obtained from the formalization), and (c) the experimental evaluation. We conclude that our formally verified development obtains interesting results in terms of precision, but it requires special precautions to ensure the proof effort remains manageable. The parallel development of specifications and proofs is essential to this end. Future works include the formalization of hardware cost models, as well as the development of more sophisticated analyses to improve the precision of the estimated WCET

APA, Harvard, Vancouver, ISO, and other styles

49

Reilles, Antoine. "Réécriture et compilation de confiance." Thesis, Vandoeuvre-les-Nancy, INPL, 2006. http://www.theses.fr/2006INPL084N/document.

Full text

Abstract:

La plupart des processus informatiques mettent en jeu la notion de transformation, en particulier la compilation. Nous nous intéressons dans cette thèse à fournir des outils et des méthodes, utilisant la réécriture, permettant d'accroître la confiance que l'on peut placer dans ces processus. Nous développons dans un premier temps un cadre permettant de valider la compilation de constructions de filtrage, produisant une preuve formelle de la validité de la compilation, ainsi qu'un témoin de cette preuve, à chaque exécution du compilateur. Afin de permettre l'écriture sûre de transformations complexes, nous proposons un générateur de structures de données efficaces intégrant des invariants algébriques, et un langage de stratégies permettant de contrôler l'application des transformations. Ces résultats constituent donc une avancée vers la constitution de methodes génériques sûres pour le développement de transformations de confiance Most computer processes involve the notion of transformation, in particular the compilation processes. We interest in this thesis in providing tools and methods, based on rewriting, giving the opportunity to increase the confidence we can place into those processes. We develop first a framework used to validate the compilation of matching constructs, building a formal proof of the validity of the compilation process along with a witness of this proof, for each run of the compiler. Then, in order to allow one to write safely complex transformations, we propose a tool that generates an efficient data structure integrating algebraic invariants, as well as a strategy language that enables to control the application of transformations. Those results can be seen as a first step towards the constitution of generic and safe methods for the development of trustworthy transformations

APA, Harvard, Vancouver, ISO, and other styles

50

Plaice, John. "Sémantique et compilation de LUSTRE, un langage déclaratif synchrone." Grenoble INPG, 1988. http://www.theses.fr/1988INPG0032.

Full text

Abstract:

Le langage étudie est un langage de programmation des systèmes temps réel fonde sur une interprétation synchrone des réseaux a flux de données. Son compilateur a été conçu entièrement à partir de descriptions formelles de la sémantique du langage. L'originalité principale du compilateur est qu'il tient d'une part aux vérifications statiques de cohérence temporelle et d'autre part à la génération de code séquentiel, par synthèse du contrôle sous forme d'automate fini

APA, Harvard, Vancouver, ISO, and other styles

Dissertations / Theses on the topic 'Compilation (informatique)'

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles