Etude semantique d'un langage intermediaire de type Static Single Assignment

Boris Yakobowski

Informations

• Publié par: Fiwyong
• Nombre de lectures: 21
• Langue: Français

Extrait

BorisYakobowski
DEAProgrammation
´Etudesemantique´ d’un
langageintermediair´ edetype
StaticSingleAssignment
sous la direction de Xavier Leroy
Stageeffectue´ a` l’INRIARocquencourt
deAvrila` Septembre2004Tabledesmatier` es
Introduction 4
Contextedecetravail . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
Notations 6
´1 Langageintermediaire 7
1.1 Syntaxedulangage . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.2 Semantique´ operationnelle´ . . . . . . . . . . . . . . . . . . . . . . . 8
1.3 Chemind’execution´ . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.4 Fonctionscorrectes . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.5 Raisonnementsurlesfonctions . . . . . . . . . . . . . . . . . . . . . 12
1.5.1 Notiond’equi´ valenceobservationnelle . . . . . . . . . . . . . 12
1.5.2 Principesdepreuves . . . . . . . . . . . . . . . . . . . . . . 12
2 Semantique´ deSSA 14
2.1 NotionsdeSSA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.2 Fonctions φdanslelangageRTL . . . . . . . . . . . . . . . . . . . . 15
2.3 Propriet´ es´ delaformeSSA . . . . . . . . . . . . . . . . . . . . . . . 16
3 PassageenformeSSA 17
3.1 Idees´ gen´ erales´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
3.2 Renommaged’unbloc . . . . . . . . . . . . . . . . . . . . . . . . . 18
3.3 Insertiondesfonctions φ . . . . . . . . . . . . . . . . . . . . . . . . 20
3.4 Commentaires . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
3.4.1 Restrictionsurladefinition´ desregistres . . . . . . . . . . . . 22
4 TransformationssurlaformeSSA 23
4.1 Substitutiontextuelle . . . . . . . . . . . . . . . . . . . . . . . . . . 23
4.2 Propagationdeconstantesetdecopies . . . . . . . . . . . . . . . . . 24
4.3 Simplificationd’instructions φ . . . . . . . . . . . . . . . . . . . . . 25
´4.4 Eliminationdecodemort . . . . . . . . . . . . . . . . . . . . . . . . 26
4.5 Algorithmegen´ eral´ parlistedetachesˆ . . . . . . . . . . . . . . . . . 27
4.5.1 Algorithmegen´ eral´ . . . . . . . . . . . . . . . . . . . . . . . 27
4.5.2 Instanciation . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Propagationdeconstantesouderegistres . . . . . . . . . . . 28
2´Boris Yakobowski — Etude semantique´ d’un langage intermediaire´ de type SSA 3
Suppressiondecodemort . . . . . . . . . . . . . . . . . . . 28
Simplificationdesinstructions φ . . . . . . . . . . . . . . . . 28
Autresalgorithmes . . . . . . . . . . . . . . . . . . . . . . . 29
“Melange”´ desalgorithmes . . . . . . . . . . . . . . . . . . . 29
´4.6 Eliminationdessous expressionscommunes . . . . . . . . . . . . . . 29
4.6.1 Ordredeparcours . . . . . . . . . . . . . . . . . . . . . . . . 31
4.6.2 Remarques . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
4.7 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
4.7.1 Separation´ devariables . . . . . . . . . . . . . . . . . . . . . 32
4.7.2 Optimisationsconditionnelles . . . . . . . . . . . . . . . . . 32
5 SortiedelaformeSSA 34
5.1 Algorithme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
5.2 Remarques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
6 Discussion 36
6.1 Travauxconnexes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
6.2 FormalisationenCoq . . . . . . . . . . . . . . . . . . . . . . . . . . 36
6.3 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
Bibliographie 38Introduction
La forme SSA (static single assignment) est une forme intermediaire´ de compila
tion, dans laquelle chaque variable d’une fonction ne peut etreˆ assignee´ statiquement
qu’uneseulefois.
En forme SSA, certaines informations sur une fonction peuvent etreˆ obtenues plus
facilement, et prennent moins d’espace. C’est typiquement le cas des reaching defini
´tions,quilient lesdefinitionsd’une variable et les emplacements dans le code qu’elles
atteignent. Dans une fonction “traditionnelle”, ces informations prennent une place en
2O(n ), n etant´ la taille de la fonction; en forme SSA, la place necessaire´ (ainsi que le
tempsnecessaire´ pourlesgen´ erer)´ sonten O(n).
Parailleurs,denombreuxalgorithmesd’optimisationssontplusefficacesenforme
SSA,aumoinsauniveaucomplexite.´ Deplus,lesoptimisationssonteg´ alementparfois
plusefficaces.
Toutefois,bienquelaformeSSAsoitdeplusenplusutilisee´ danslescompilateurs
1modernes , sa semantique´ est mal comprise. Par exemple, apres` certaines transforma
tions,lesalgorithmesutilises´ poursortirdelaformeSSAgen´ eraient´ uncodeincorrect,
quin’avaitpaslememeˆ comportementqueleprogrammed’origine.
De fac¸on gen´ erale,´ un programme en forme SSA doit verifier´ certaines conditions,
quisontsouventinsuffisammentmisesenavantdanslestextesderef´ erence.´ Dememe,ˆ
touteslesoptimisationsnesontpaslicitesenformeSSA.
Danscedocument,onintroduitunesemantique´ SSApourunlangageintermediaire´
detypeRTL(registertransferlangage).Onenonce´ lespropriet´ es´ qu’unefonctiondoit
verifier´ pouretreˆ enformeSSA,etonpropose:
– UnalgorithmetransformantunefonctionRTLenunefonctionSSAequi´ valente.
– Plusieurs algorithmes d’optimisation sur les fonctions en forme SSA (propaga
tiondeconstantes,suppressiondecopies,suppressiondecodemort,elimination´
desous expressionscommunes).
– Un algorithme transformant une fonction en forme SSA en une fonction RTL
´equivalente.
Ces algorithmes etant´ a` terme destines´ a` etreˆ incorpores´ dans un compilateur op
timisant prouve,´ nous nous sommes efforces´ de choisir les solutions les plus adaptees´
a` la preuve formelle (souvent les plus simples et les plus decomposables´ possibles);
1Laversion3.5deGCC,lecompilateurlibreduprojetGNU,devraitutiliserlaformeSSApourcertaines
desesoptimisations.
4´Boris Yakobowski — Etude semantique´ d’un langage intermediaire´ de type SSA 5
toutefois nous pensons qu’aucun de nos choix n’est vraiment redhibitoire´ compare´ a`
desalgorithmesplusev´ olues.´
Lebutdutravailpresent´ e´ icietait´ donctriple:
1. Trouverunesemantique´ acceptablepourSSA.
2. Trouver dans la litterature´ ou inventer des algorithmes travaillant sur des fonc
tionsenformeSSA,etpreserv´ antlasemantique.´
3. Prouverlacorrectionde ces algorithmes, en gardant a` l’esprit la necessit´ e´ de les
prouverformellementensuite.
Contextedecetravail
Ce stage a et´ e´ encadre´ par Xavier Leroy, dans le projet Cristal; toutefois ce travail
`s’inscritplusparticulierementdanslecadredel’ARCConcert.
L’equipe´ Cristal travaille a` la conception de langages de programmation et a` leur
formalisation, avec pour objectif principal d’accroˆıtre la robustesse des applications
informatiquesetlarapidite´ deleurdev´ eloppement.Ceux cisontaccrusparl’utilisation
de langages de programmation expressifs et surs,ˆ et les recherches menees´ au projet
Cristal ont pour objectif de proposer de tels langages ainsi que d’etudier´ formellement
leurspropriet´ es.´ L’equipe´ Cristalsecomposeactuellementde7chercheurspermanents,
3chercheursdetach´ es,´ et1doctorant.
L’action de recherche cooperati´ ve Concert a pour objectif principal de determiner´
s’ilestfaisable,dansl’etat´ actueldesconnaissances,derealiser´ uncompilateurrealiste´
qui soit certifie,´ c’est a dire` accompagn e´ d’une preuve Coq d’equi´ valence semantique´
entre le code source et le code machine engendre.´ C’est une action concertee´ entre le
CNAM I.I.E.,etlesprojetsCristal,Lemme,Mimosa,OasisetMir o´ del’INRIA.
Dans le cadre de l’action Concert, ce stage a pour but d’etudier´ d’ev´ entuelles sim
plifications algorithmiques sur les optimisations faites par le compilateur. Ces optimi
sations sont actuellement effectuees´ par des algorithmes de data flow, dont l’e fficacite´
laissea` desirer´ ;laformeSSA,parlessimplificationsqu’ellegen´ ere,` pourraitpermettre
des’affranchirdecesproblemes.`
Toutefois, un des objectifs du stage est eg´ alement de voir si ces simplifications
ne s’accompagnent pas d’une plus grande complexite´ lors de l’implementation´ et de
l’ecriture´ despreuvesdecorrection.
Une version preliminaire´ de ce travail a et´ e´ present´ ee´ lors d’une reunion´ Concert
ayanteulieuaumoinsdeJuin2004.Notations
Dans tout le document, certains noms de variables sont implicitement quantifies´
suruntype;quandc’estlecas,ons’autorisea` nepasquantifierexplicitementdansles
formules.Parexemple,lalettrenvariesurl’ensembleNdesentiersnaturels;lesautres
conventionsserontintroduitesaufureta` mesure.
On note D(f) et CD(f) le domaine et le codomaine d’une fonction,◦ la
composition de deux fonctions, et f| la restriction de f au domaine D. La fonctionD
valant f saufen vou` ellevaut eestnotee´ f[v := e].Lafonctionconstanteeg´ alea` eest
notee´ ( 7→ e),l’identite´ Id.
´Etant donne´ un ensemble E, on note List(E) l’e