Extension paramétrée de compilateur certifié pour la programmation parallèle
Les applications informatiques sont de plus en plus présentes dans nos vies. Pour les applications critiques (médecine, transport, . . .), les conséquences d une erreur informatique ont un coût inacceptable, que ce soit sur le plan humain ou financier. Une des méthodes pour éviter la présence d erre...
Enregistré dans:
| Hovedforfatter: | |
|---|---|
| Andre forfattere: | , , , , , |
| Format: | Thèse numérique |
| Sprog: | Français |
| Udgivet: |
2015.
|
| Fag: | |
| Online adgang: | Accès au texte intégral https://theses.univ-orleans.fr/public/2015ORLE2071_va.pdf http://www.theses.fr/2015ORLE2071/abes https://theses.hal.science/tel-01371936 |
| Kommentar: |
Titre provenant de l'écran-titre Ecole(s) Doctorale(s) : École doctorale Mathématiques, Informatique, Physique Théorique et Ingénierie des Systèmes (Centre-Val de Loire ; 2012-....) Partenaire(s) de recherche : Laboratoire d'informatique fondamentale d'Orléans (Orléans ; 1987-....) (Laboratoire) Autre(s) contribution(s) : Jean-Michel Couvreur (Président du jury) ; Frédéric Loulergue, Jean-Michel Couvreur, Gaétan Hains, Ludovic Henrio, Frédéric Dabrowski, Pierre Courtieu (Membre(s) du jury) ; Gaétan Hains, Ludovic Henrio (Rapporteur(s)) |
| Autres localisations: | Voir dans le Sudoc |
| Variante du titre: | Parameterised extension of certified compiler for parallel programming |
| LEADER | 05096nam a22004697a 4500 | ||
|---|---|---|---|
| 001 | 600871 | ||
| 008 | 160926s2015 xxe ||| |||| 00| 0 fre d | ||
| 009 | PPN195299485 | ||
| 041 | 0 | |a fre |b fre |b eng | |
| 082 | |a 005.453 | ||
| 084 | |a 000 | ||
| 100 | 1 | |a Dailler, Sylvain, |d 1988- | |
| 240 | 1 | 0 | |a Parameterised extension of certified compiler for parallel programming |
| 245 | 1 | 0 | |a Extension paramétrée de compilateur certifié pour la programmation parallèle |c Sylvain Dailler ; sous la direction de Frédéric Loulergue. |
| 256 | |a Données textuelles | ||
| 260 | |c 2015. | ||
| 500 | |a Titre provenant de l'écran-titre | ||
| 500 | |a Ecole(s) Doctorale(s) : École doctorale Mathématiques, Informatique, Physique Théorique et Ingénierie des Systèmes (Centre-Val de Loire ; 2012-....) | ||
| 500 | |a Partenaire(s) de recherche : Laboratoire d'informatique fondamentale d'Orléans (Orléans ; 1987-....) (Laboratoire) | ||
| 500 | |a Autre(s) contribution(s) : Jean-Michel Couvreur (Président du jury) ; Frédéric Loulergue, Jean-Michel Couvreur, Gaétan Hains, Ludovic Henrio, Frédéric Dabrowski, Pierre Courtieu (Membre(s) du jury) ; Gaétan Hains, Ludovic Henrio (Rapporteur(s)) | ||
| 502 | |a Thèse de doctorat. Informatique. Orléans. 2015 | ||
| 520 | |a Les applications informatiques sont de plus en plus présentes dans nos vies. Pour les applications critiques (médecine, transport, . . .), les conséquences d une erreur informatique ont un coût inacceptable, que ce soit sur le plan humain ou financier. Une des méthodes pour éviter la présence d erreurs dans les programmes est la vérification déductive. Celle-ci s applique à des programmes écrits dans des langages de haut-niveau transformés, par des compilateurs, en programmes écrits en langage machine. Les compilateurs doivent être corrects pour ne pas propager d erreurs au langage machine. Depuis 2005, les processeurs multi-coeurs se sont répandus dans l ensemble des systèmes informatiques. Ces architectures nécessitent des compilateurs et des preuves de correction adaptées. Notre contribution est l extension modulaire d un compilateur vérifié pour un langage parallèle ciblant des architectures parallèles multi-coeurs. Les spécifications des langages (et leurs sémantiques opérationnelles) présents aux divers niveaux du compilateur ainsi que les preuves de la correction du compilateur sont paramétrées par des modules spécifiant des éléments de parallélisme tels qu un modèle mémoire faible et des notions de synchronisation et d ordonnancement entre processus légers. Ce travail ouvre la voie à la conception d un compilateur certifié pour des langages parallèles de haut-niveau tels que les langages à squelettes algorithmiques. | ||
| 520 | |a Nowadays, we are using an increasing number of computer applications. Errors in critical applications (medicine, transport, . . .) may carry serious health or financial issues. Avoiding errors in programs is a challenge and may be achieved by deductive verification. Deductive verification applies to program written in a high-level languages, which are transformed into machine language by compilers. These compilers must be correct to ensure the nonpropagation of errors to machine code. Since 2005, multicore processors have spread in all electronic devices. So, these architectures need adapted compilers and proofs of correctness. Our work is the modular extension of a verified compiler for parallel languages targeting multicore architectures. Specifications of these languages (and their operational semantics) needed at all levels of the compiler and proofs of correctness of this compiler are parameterized by modules specifying elements of parallelism such as a relaxed memory model and notions of synchronization and scheduling between threads. This work is the first step in the conception of a certified compiler for high-level parallel languages such as algorithmic skeletons. | ||
| 538 | |a Configuration requise : un logiciel capable de lire un fichier au format : PDF | ||
| 650 | |a Programmation parallèle (informatique) | ||
| 650 | |a Microprocesseurs multi-coeurs | ||
| 650 | |a Compilation (informatique) | ||
| 650 | |a Assistants de preuve | ||
| 650 | |a Débogage | ||
| 650 | |a Thèses et écrits académiques | ||
| 700 | 1 | |a Loulergue, Frédéric, |d 1973- |4 ths |4 opn | |
| 700 | 1 | |a Couvreur, Jean-Michel, |d 1959- |4 opn | |
| 700 | 1 | |a Hains, Gaétan, |d 1963- |4 opn | |
| 700 | 1 | |a Henrio, Ludovic, |d 1976-...., |c informaticien. |4 opn | |
| 700 | 1 | |a Dabrowski, Frédéric, |d 1976- |4 opn | |
| 700 | 1 | |a Courtieu, Pierre, |d 19..- |4 opn | |
| 710 | 2 | |a Université d'Orléans. |4 dgg | |
| 856 | 4 | |q PDF |s 1551430 |u http://www.theses.fr/2015ORLE2071/document |z Accès au texte intégral | |
| 856 | 4 | |u https://theses.univ-orleans.fr/public/2015ORLE2071_va.pdf | |
| 856 | 4 | |u http://www.theses.fr/2015ORLE2071/abes | |
| 856 | 4 | |u https://theses.hal.science/tel-01371936 | |
| 997 | |0 600871 |1 Thèse numérique |a Ressource numérique |b INSA |b ENSA |c 0/Bibliothèque numérique/ |c 1/Bibliothèque numérique/Autre ressource numérique/ | ||