• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 1
  • Tagged with
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • 1
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
1

De la sémantique opérationnelle à la spécification formelle de compilateurs: l'exemple des boucles en Esterel

Tardieu, Olivier 24 September 2004 (has links) (PDF)
Esterel est un langage impératif concurrent pour la programmation des systèmes réactifs. A l'exception de l'instruction "pause", les primitives du langage s'exécutent sans consommer de temps logique. L'exécution se décompose donc en une suite d'instants. Dans ce contexte, les boucles peuvent poser deux types de problèmes: d'une part une boucle instantanée peut bloquer l'écoulement du temps; d'autre part un bloc de code peut être traversé plusieurs fois au cours du même instant, conduisant à un comportement du programme dit "schizophrène". Les boucles instantanées sont proscrites par la sémantique. Elles doivent donc être détectées par les compilateurs et les programmes correspondants doivent être rejetés. Par ailleurs, la compilation efficace des programmes schizophrènes est difficile. Ainsi, alors que plusieurs compilateurs pour Esterel sont disponibles, les algorithmes employés pour compiler les boucles ne sont ni portables, ni formellement spécifiés, et encore moins prouvés. Dans ce document, nous étudions les boucles en Esterel, établissant une correspondance formelle entre la sémantique opérationnelle du langage et l'implémentation concrète d'un compilateur. Après avoir spécifié les problèmes posés par les boucles, nous développons des techniques d'analyse statique efficaces pour les détecter dans un code Esterel quelconque. Puis, de façon à guérir la schizophrénie, c'est à dire transformer efficacement les programmes schizophrènes en programmes non schizophrènes, nous introduisons dans le langage une nouvelle primitive appelée "gotopause". Elle permet de transférer le contrôle d'un point du programme à un autre de façon non instantanée, mais sans contrainte de localité. Elle préserve le modèle de concurrence synchrone d'Esterel. Nous décrivons un premier algorithme qui, en dépliant les boucles à l'aide de cette nouvelle instruction, produit pour tout programme Esterel correct un programme non schizophrène équivalent. Enfin, en combinant analyse statique et réécriture, nous obtenons un préprocesseur qui rejette les boucles instantanées et guérit la schizophrénie, à la fois portable et très efficace. Nous l'avons implémenté. De plus, grâce à une approche formelle de bout en bout, nous avons pu prouver la correction de ce préprocesseur.

Page generated in 0.1394 seconds