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

De
Publié par

BorisYakobowskiDEAProgrammation´Etudesemantique´ d’unlangageintermediair´ edetypeStaticSingleAssignmentsous la direction de Xavier LeroyStageeffectue´ a` l’INRIARocquencourtdeAvrila` Septembre2004Tabledesmatier` esIntroduction 4Contextedecetravail . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5Notations 6´1 Langageintermediaire 71.1 Syntaxedulangage . . . . . . . . . . . . . . . . . . . . . . . . . . . 71.2 Semantique´ operationnelle´ . . . . . . . . . . . . . . . . . . . . . . . 81.3 Chemind’execution´ . . . . . . . . . . . . . . . . . . . . . . . . . . . 91.4 Fonctionscorrectes . . . . . . . . . . . . . . . . . . . . . . . . . . . 111.5 Raisonnementsurlesfonctions . . . . . . . . . . . . . . . . . . . . . 121.5.1 Notiond’equi´ valenceobservationnelle . . . . . . . . . . . . . 121.5.2 Principesdepreuves . . . . . . . . . . . . . . . . . . . . . . 122 Semantique´ deSSA 142.1 NotionsdeSSA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142.2 Fonctions φdanslelangageRTL . . . . . . . . . . . . . . . . . . . . 152.3 Propriet´ es´ delaformeSSA . . . . . . . . . . . . . . . . . . . . . . . 163 PassageenformeSSA 173.1 Idees´ gen´ erales´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 173.2 Renommaged’unbloc . . . . . . . . . . . . . . . . . . . . . . . . . 183.3 Insertiondesfonctions φ . . . . . . . . . . . . . . . . . . . . . . . . 203.4 Commentaires . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 223.4 ...
Publié le : samedi 24 septembre 2011
Lecture(s) : 18
Nombre de pages : 39
Voir plus Voir moins

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’ensemble des listes (ordonnees)´
d’el´ ements´ de E. La liste vide est notee´ []. La liste constituee´ de e puis des el´ ements´
´de l est notee´ [e;l]; on abrege` [e ;[...;[e ;l]]] en [e ;...;e ;l]. Etant donne´ une liste l1 n 1 n
de longueur|l|, son nieme` el´ ement´ (1≤ n≤|l|) est l.(n). La liste l[n := e] est eg´ ale a` l,
saufpourl’el´ ement´ nquiest e.Laconcatenation´ surleslistesestnotee´ @.
2On definit´ un predicat´ d’appartenance syntaxiqueA sur les el´ ements´ d’ensembles
construits (par exemple les listes). Ainsi on ecrira´ eA l si et seulement si e est un des
el´ ements´ de l ousi eapparaˆıtdansundesel´ ements´ de l.
De meme,ˆ on definit´ une operation´ de substitution syntaxique, notee´ eg´ alement
0 00 0 00e[e := e ],quiremplacetouteslesoccurrencesde e dans epar e .
2Nontype.´
6Chapitre1
Langageintermediair´ e
Danscettepartieondecrit´ lelangageintermediaire´ surlequelonvaraisonnerpour
lespreuves.Celangageestunlangage3adresses,ouRTL(RegisterTransferLangage)
´pourunprocesseurRISC:touteslesoperationsdecalculsefontsurlesregistres,eton
ajoutedeuxinstructions load et storepouracceder´ a` lamemoire.´
Dans le cadre de l’etude´ de SSA, on peut ne pas definir´ tout le langage assembleur
du processeur, qui n’a pas grand inter´ et.ˆ Pour cela on se contente de supposer l’exis
tence d’un ensemble d’operateurs´ binaires, qui contient par exemple les operations´
arithmetiques´ usuelles(addition,multiplication...).
1.1 Syntaxedulangage
Le langage est present´ e´ Fig. 1.1. Une fonction RTL est constituee´ d’une fonction
partielle de l’ensemble des etiquettes´ dans celui des blocs, et d’un nombre de pa
rametres.` Par convention, les registres r a` r d’une fonction a` n arguments sont les1 n
parametres` delafonction.
On definit´ des fonctions d’acces` aux el´ ements´ d’un bloc par I(I, j) = I et
B(I, j) = j. Par ailleurs, etant´ donne´ F = (B,n), on confond la plupart du temps
F et B.
Une fonction est dite coher´ ente lorsque toutes les etiquettes´ apparaissant dans une
instruction de branchement font partie du domaine de la fonction : Coherent(F) ≡
∀l,lA F =⇒ l∈ D(F).Danslasuiteonneconsidere` quedesfonctionscoherentes.´
Par convention, on suppose que l est toujours le premier bloc d’une fonction a`init
etreˆ execut´ e.´ On suppose eg´ alement qu’aucune instruction de branchement n’a pour
´destination l . Enfin, on suppose l’existence d’une etiquette l telle que quelle queinit ,
soit F, l < D(f).
,
´Etant donne´ une fonction F, on designe´ par F.l.n la nieme` instruction lineaire´ du
blocdontl’etiquette´ estlsicettederniere` existe,etl’instructiondebranchementsinon.
Par homogen´ eit´ e,´ on note F.l.ω l’instruction de saut du bloc dont l’etiquette´ est l. La
variable τ parcourt l’ensemble Loc des valeurs de la forme l.n, avec = n∈ N∪{ω};
7´Boris Yakobowski — Etude semantique´ d’un langage intermediaire´ de type SSA 8
i∈LinInstrs ::=() (NO)
| r μ (C)
| r μ?μ (O)
l∈Labels
| r F(μ,..,μ) (C)
?∈Ops
| r [μ] (L)
r∈Regs
| [μ] μ (S)
v∈Vals
j∈BranchInstrs::=→| μ (R)
μ∈Regs∪Vals
| l (J)
ι∈Instrs= LinInstrs∪?| μ : l,l (CJ)
BranchInstrs
b∈Blocks = List(LinInstrs)×BranchInstrs
LabelsF∈Functions = Blocks ×N
F.1.1–Syntaxedulangage
on appelle ces valeurs emplacements. On note τ = l .1; et τ(F) l’ensemble des• init
emplacementscorrespondantsa` desinstructionsdelafonction F.
Ondefinit´ RDefetRUse(registresdefinis´ etregistresutilises)´ par:
RDef(r ...)={r} RDef([μ] ...)=∅ RDef(j)=∅
RUse(r e)={r rA e} RUse([μ ] μ)={r rA μ }∪{r rA μ}m m
?RUse(→| μ)={r rA μ} RUse( l)=∅ RUse( μ : l ,l )={r rA μ}T F
Ondefinit´ eg´ alementRDefetRUseentantquesous ensemblesde Instrspar:
RDef(r)={ι r∈ RDef(ι)} RUse(r)={ι r∈ RUse(ι)}
1.2 Semantique´ operationnelle´
On modelise´ l’etat´ des registres et de la memoire´ a` un instant t de l’execution´
par des fonctions totales, mais a` image dans Vals∪{B}; on noteR la fonc B
tion qui a` tout registre associe B. B est une valeur d’erreur, qui correspond a`
l’arretˆ prematur´ e´ d’une fonction (division par 0, acces` a` une zone memoire´ non ini
tialisee.´ ..). Les operateurs´ sont donc vus comme des fonctions totales de Vals×Vals
dansVals∪{B}.Onetend´ lesregistresauxel´ ements´ deValsenposantR(v)= v
La semantique´ operationnelle´ est donnee´ sous la forme de predicats´ d’ev´ aluations
mutuellementrecursifs,´ surlesinstructions(Fig.1.2)etlesblocsdefonctions(Fig1.3).
Le resultat´ de l’execution´ d’une fonction est un etat´ memoire´ et une valeur de retour;
l’etat´ finaldesregistresestignore.´Z
´Boris Yakobowski — Etude semantique´ d’un langage intermediaire´ de type SSA 9
R(μ)= v
SNO SC
hR,M,l ,()i→hR,Mi hR,M,l ,r μi→hR[r := v],Mi− −
R(μ )= v R(μ )= v v ?v = v1 1 2 2 1 2
SO
hR,M,l ,r μ ?μi→hR[r := v],Mi− 1 2
0
R(μ)= v M(v)= v
SL
0hR,M,l ,r [μ]i→hR[r := v ],Mi−
R(μ )= v R(μ)= vm m
SS
hR,M,l ,[μ ] μi→hR,M[v := v]i− m m
0∀n,R(μ )= v hM,(v ,...,v ),F)⇒hM ,vin n 1 n
SC
0hR,M,l ,r F(μ ,...,μ )i→hR[r := v],Mi− 1 n
∗hR,M,l ,[]i→ hR,Mi−
0 0 0 0 ∗ 00 00hR,M,l ,ii→hR ,Mi hR ,M ,l ,Li→ hR ,M i− −
∗ 00 00
hR,M,l ,[i;L]i→ hR ,M i−
R(μ)= v, 0 R(μ)= 0
SCJT SCJF
? ?hR, μ : l ,l i l hR, μ : l ,l i lT F T T F F
R(μ)= v
SJ SR
hR, li l hR,→| μi→| v
F.1.2–Semantique´ operationnelle´ pourlesinstructions.
Une difference´ notable par rapport aux semantiques´ usuelles est qu’on memorise´
l’etiquette´ du bloc duquel on “arrive”. Cette information n’est pas utile pour les ins
tructionsqu’onpresente´ danscettepartie,maisserautilisee´ parlesfonctionsenforme
SSA.
1.3 Chemind’execution´
Onpeutrepresenter´ statiquementl’execution´ d’unefonctionparlalistedesinstruc
tions qui sont execut´ ees´ dynamiquement. Pour cela, etant´ donne´ une fonction F et un
emplacement,ondefinit´ unenotiond’emplacementssuccesseurs,quimodelisent´ leflotZ
´Boris Yakobowski — Etude semantique´ d’un langage intermediaire´ de type SSA 10
∗ 0 0 0 0hR,M,F,l ,I(F(l))→ hR ,Mi hR ,B(F(l))i l−
SBJ
0 0 0hR,M,F,l ,li€hR ,M ,li−
∗hR,M,F,l ,li€ hR,M,l ,li− −
0 0 0 0 0 0 ∗ 00 00 00 000
hR,M,F,l ,li€hR ,M ,li hR ,M ,F,l,li€ hR ,M ,l ,l i−
∗ 00 00 00 000hR,M,F,l ,li€ hR ,M ,l ,l i−
∗ 0 0 0hR,M,l ,I(F(l)i→ hR ,Mi hR ,B(F(l))i→| v−
SBR
0hR,M,F,l ,li€|hM ,vi−
∗ 0 0 0hR [r := v ,...,r := v ],M,F,l ,l i€ hR ,M ,l,liB 1 1 n n , init
0 0 0 00hR ,M ,F,l,li€|hM ,vi
SE
00hM,(v ,...,v ),Fi⇒hM ,vi1 n
F.1.3–Semantique´ operationnelle´ pourlesblocsetlesfonctions
decontroleˆ delafonction.
(
{l.(n+1)} Si F.l.(n+1)∈ LinInstrs
s (l.n)=F 0 0{l .1 l A F.l.ω} Si F.l.n∈ BranchInstrs
0 0Onditquedeuxemplacementsτetτ sesuivent dans F siτ ∈ s (τ),etonappelleF
chemin dans F une liste de tels emplacement. La variable I parcourt l’ensemble des
chemins; SoitPath le sous ensemble de Path constitue´ des chemins passant par
τ ,...,τ1 n
τ ,...,τ .1 n
´ ´ ´ ´ ´Etant donne un element I de Path , un entier n tel que n≤|I|, un etat initial des
τ•
F FregistresR et un etat´ initial de la memoire´ M, on noteR (resp.R ) l’etat´ des
+ −I,n I,n
1registres apres` (resp. avant) l’execution´ des n premieres` instructions de I; on definit´
F F F F FsimilairementM etM .Onabiensurˆ leseg´ alites´ R =RetR =R (de
+ − − + −I,n I,n I,1 I,n I,n+1
memeˆ pourlamemoire).´
On dit qu’un emplacement τ domine (resp. domine strictement) statiquement un
0 0 0emplacement τ (note´ τ≺ τ , resp. τ τ ) si, dans tout chemin partant de τ , une•
0occurrence de τ est necessairement´ prec´ ed´ ee´ (resp. prec´ ed´ ee´ strictement) par une oc
currencede τ:
0 0 0 0 0 0
0τ≺ τ (resp. τ τ )≡∀I∈ Path ,I.(n )= τ =⇒ ∃n≤ n (resp. n < n ) I.(n)= τ
τ
1Onetend´ →auxinstructionsdesaut,enconsiderant´ quel’etat´ delamemoire´ etdesregistresestinchange´
apres` l’execution´ d’uneinstructiondebranchement

Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.