Étude sémantique d'un langage intermédiaire de type Static Single Assignment

Boris Yakobowski

Informations

• Publié par: Zuim
• Nombre de lectures: 34
• Langue: Français

Extrait

Introduction
Passage SSA↔ RTL
Optimisations sur la forme SSA
Conclusion
Etude semantique d’un langage intermediaire de
type Static Single Assignment
Boris Yakobowski
INRIA Rocquencourt
DEA Programmation
13 Septembre 2004
Boris Yakobowski Etude semantique d’un langage intermediaire de type SSAIntroduction
Passage SSA↔ RTL
Optimisations sur la forme SSA
Conclusion
Plan
1 Introduction
Contexte du travail
Problemes dans l’implementation actuelle
Contributions
2 Passage SSA↔ RTL
Proprietes des fonctions en forme SSA
Passage en forme SSA
Syntaxe du langage et semantique
Sortie de la forme SSA
3 Optimisations sur la forme SSA e ectuees
Proprietes utilisees par les simpli cations
Boris Yakobowski Etude semantique d’un langage intermediaire de type SSAIntroduction
Contexte du travail
Passage SSA↔ RTL
Problemes dans l’implementation actuelle
Optimisations sur la forme SSA
Contributions
Conclusion
Plan
1 Introduction
Contexte du travail
Problemes dans l’implementation actuelle
Contributions
2 Passage SSA↔ RTL
Proprietes des fonctions en forme SSA
Passage en forme SSA
Syntaxe du langage et semantique
Sortie de la forme SSA
3 Optimisations sur la forme SSA e ectuees
Proprietes utilisees par les simpli cations
Boris Yakobowski Etude semantique d’un langage intermediaire de type SSAIntroduction
Contexte du travail
Passage SSA↔ RTL
Problemes dans l’implementation actuelle
Optimisations sur la forme SSA
Contributions
Conclusion
Projet(s) d’accueil
Projet Cristal
Travaille a la conception, a l’implementation et a l’etablissement
des fondements theoriques des langages de programmation
fortement types.
ARC Concert
Cherche a determiner s’il est faisable de realiser un compilateur
optimisant qui soit certi e (avec une preuve Coq d’equivalence
semantique entre le code source et le code machine engendre).
Boris Yakobowski Etude semantique d’un langage intermediaire de type SSAIntroduction
Contexte du travail
Passage SSA↔ RTL
Problemes dans l’implementation actuelle
Optimisations sur la forme SSA
Contributions
Conclusion
Projet(s) d’accueil
Projet Cristal
Travaille a la conception, a l’implementation et a l’etablissement
des fondements theoriques des langages de programmation
fortement types.
ARC Concert
Cherche a determiner s’il est faisable de realiser un compilateur
optimisant qui soit certi e (avec une preuve Coq d’equivalence
semantique entre le code source et le code machine engendre).
Boris Yakobowski Etude semantique d’un langage intermediaire de type SSA/

h

o
O
h



/
O
o

Introduction
Contexte du travail
Passage SSA↔ RTL
Problemes dans l’implementation actuelle
Optimisations sur la forme SSA
Contributions
Conclusion
optimisations de bouclesGFED
typage
C simplie Cminor
traduction
explicitation de registres
selection d’instructions
spilling etRTL avec RTL avec
reloadingregistres reels registres virtuels@ABC
linearisation
optimisations data ow
Assembleur
PowerPC BCED ordonnancement d’instructions
Boris Yakobowski Etude semantique d’un langage intermediaire de type SSAIntroduction
Contexte du travail
Passage SSA↔ RTL
Problemes dans l’implementation actuelle
Optimisations sur la forme SSA
Contributions
Conclusion
Problemes dans l’implementation actuelle
Performances insu santes
Les optimisations actuellement e ectuees sont a base de data- ow ,
et sont peu e caces algorithmiquement.
Forme SSA
En forme SSA, toutes les optimisations actuellement e ectuees
dans Concert peuvent ˆetre faites en un temps lineaire.
Boris Yakobowski Etude semantique d’un langage intermediaire de type SSAIntroduction
Contexte du travail
Passage SSA↔ RTL
Problemes dans l’implementation actuelle
Optimisations sur la forme SSA
Contributions
Conclusion
Problemes dans l’implementation actuelle
Performances insu santes
Les optimisations actuellement e ectuees sont a base de data- ow ,
et sont peu e caces algorithmiquement.
Forme SSA
En forme SSA, toutes les optimisations actuellement e ectuees
dans Concert peuvent ˆetre faites en un temps lineaire.
Boris Yakobowski Etude semantique d’un langage intermediaire de type SSAo

h

/

/

h


O
O
o
Introduction
Contexte du travail
Passage SSA↔ RTL
Problemes dans l’implementation actuelle
Optimisations sur la forme SSA
Contributions
Conclusion
optimisations de bouclesGFED
typage
C simpli