Normal view MARC view ISBD view

De la sémantique opérationnelle à la spécification formelle de compilateurs [Texte imprimé] : l'exemple des boucles en Esterel / par Olivier Tardieu ; sous la direction de Gérard Berry

Auteur principal : Tardieu, Olivier, 1976-...., AuteurAuteur secondaire : : Berry, Gérard, 1948-...., Directeur de thèseAuteur secondaire collectivité : , Paris, Organisme de soutenancePublication : [S.l.] : [s.n.], 2004Description : 1 vol. (130 p.) ; 30 cmRésumé : Esterel est un langage impératif synchrone pour la programmation de systèmes réactifs orientés contrôle. De façon à dériver une description formelle de compilateur Esterel à partir d’une sémantique opérationnelle du langage, nous proposons une nouvelle sémantique qui exclut les exécutions non déterministes. Puis nous nous concentrons sur les problèmes posés par la compilation des boucles. Les primitives du langage à l’exception de l’instruction « pause » s’exécutent sans consommer de temps logique. Par conséquent les boucles peuvent conduire à la répétition instantanée d’un même bloc de code, d’où de possibles blocages (répétition infinie) et des comportements difficiles à implémenter correctement (répétition finie). À l’aide d’une nouvelle instruction de saut non instantané « gotopause » et en combinant analyse statique et réécriture de code, nous spécifions un schéma de compilation des boucles à la fois portable, performant et sûr. Nous démontrons sa correction.; Esterel is a synchronous imperative design language for the specification of control-oriented reactive systems. In order to formally derive the specification of an Esterel compiler from the operational semantics of the language, we first describe a new semantics for Esterel that discards non-deterministic executions. Then, we show how to understand and solve the problems in compilers raised by the “loop” construct of Esterel. All primitive instructions except for “pause” execute in zero time. Thus, because of loops, a given piece of code may be executed several times in a single instant, potentially leading to complex (finite loop) or incorrect (infinite loop) behaviors. Using a new non-instantaneous jump instruction called “gotopause”, and combining program rewriting with static analysis techniques, we build a safe code generation scheme for loop structures that rejects incorrect loops and compiles correct loops very efficiently. We formalize and prove the correctness of this scheme..Bibliographie: Bibliogr. 86 réf..Thèse : .Sujet - Nom d'actualité : Logiciels -- Vérification ;Algorithmes -- Thèses et écrits académiques ;Algorithmes ;Temps réel (informatique) -- Thèses et écrits académiques ;Compilation (informatique) -- Thèses et écrits académiques Sujet : SEMANTIQUE ;LANGAGE ESTEREL ;COMPILATION ;Analyse statique ;Concurrence ;Langage ESTEREL ;Sémantique ;Transformation programme ;Transformation de programme Ressource en ligneAccès en ligne
Current location Call number Status Notes Date due Barcode
Bib. Paris
EMP 152.369 CCL.TH.1111 Available Thèse en ligne EMP74792D
Bib. Paris
EMP 152.368 CCL.TH.1111 Available Thèse en ligne EMP74791D
Centre de recherche en informatique
04 TAR Sur demande Thèse en ligne CRI05654D
Sophia Antipolis
EMS T-CMA-055 Sur demande Thèse en ligne

Publication autorisée par le jury

Bibliogr. 86 réf.

Thèse de doctorat Informatique temps réel, robotique et automatique Paris, ENMP 2004

Esterel est un langage impératif synchrone pour la programmation de systèmes réactifs orientés contrôle. De façon à dériver une description formelle de compilateur Esterel à partir d’une sémantique opérationnelle du langage, nous proposons une nouvelle sémantique qui exclut les exécutions non déterministes. Puis nous nous concentrons sur les problèmes posés par la compilation des boucles. Les primitives du langage à l’exception de l’instruction « pause » s’exécutent sans consommer de temps logique. Par conséquent les boucles peuvent conduire à la répétition instantanée d’un même bloc de code, d’où de possibles blocages (répétition infinie) et des comportements difficiles à implémenter correctement (répétition finie). À l’aide d’une nouvelle instruction de saut non instantané « gotopause » et en combinant analyse statique et réécriture de code, nous spécifions un schéma de compilation des boucles à la fois portable, performant et sûr. Nous démontrons sa correction.

Esterel is a synchronous imperative design language for the specification of control-oriented reactive systems. In order to formally derive the specification of an Esterel compiler from the operational semantics of the language, we first describe a new semantics for Esterel that discards non-deterministic executions. Then, we show how to understand and solve the problems in compilers raised by the “loop” construct of Esterel. All primitive instructions except for “pause” execute in zero time. Thus, because of loops, a given piece of code may be executed several times in a single instant, potentially leading to complex (finite loop) or incorrect (infinite loop) behaviors. Using a new non-instantaneous jump instruction called “gotopause”, and combining program rewriting with static analysis techniques, we build a safe code generation scheme for loop structures that rejects incorrect loops and compiles correct loops very efficiently. We formalize and prove the correctness of this scheme.

Powered by Koha