La lecture en ligne est gratuite
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres
Télécharger Lire

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

De
49 pages
IntroductionPassage SSA↔ RTLOptimisations sur la forme SSAConclusionEtude semantique d’un langage intermediaire detype Static Single AssignmentBoris YakobowskiINRIA RocquencourtDEA Programmation13 Septembre 2004Boris Yakobowski Etude semantique d’un langage intermediaire de type SSAIntroductionPassage SSA↔ RTLOptimisations sur la forme SSAConclusionPlan1 IntroductionContexte du travailProblemes dans l’implementation actuelleContributions2 Passage SSA↔ RTLProprietes des fonctions en forme SSAPassage en forme SSASyntaxe du langage et semantiqueSortie de la forme SSA3 Optimisations sur la forme SSA e ectueesProprietes utilisees par les simpli cationsBoris Yakobowski Etude semantique d’un langage intermediaire de type SSAIntroductionContexte du travailPassage SSA↔ RTLProblemes dans l’implementation actuelleOptimisations sur la forme SSAContributionsConclusionPlan1 IntroductionContexte du travailProblemes dans l’implementation actuelleContributions2 Passage SSA↔ RTLProprietes des fonctions en forme SSAPassage en forme SSASyntaxe du langage et semantiqueSortie de la forme SSA3 Optimisations sur la forme SSA e ectueesProprietes utilisees par les simpli cationsBoris Yakobowski Etude semantique d’un langage intermediaire de type SSAIntroductionContexte du travailPassage SSA↔ RTLProblemes dans l’implementation actuelleOptimisations sur la forme SSAContributionsConclusionProjet(s) ...
Voir plus Voir moins

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

Un pour Un
Permettre à tous d'accéder à la lecture
Pour chaque accès à la bibliothèque, YouScribe donne un accès à une personne dans le besoin