Coloration avec préférences dans les graphes triangulés ...
19 pages
Catalan

Coloration avec préférences dans les graphes triangulés ...

-

Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

Description

Pr´esentation du probl`eme et de son cadre d’´etude
R´esolution du probl`eme
Conclusion et perspectives
Coloration avec pr´ef´erences dans les graphes
triangul´es
V´erification formelle de la r´esolution d’un probl`eme de graphes
´Sandrine Blazy, Benoˆıt Robillard et Eric Soutif
CEDRIC, ´equipes CPR et OC
9 Novembre 2007
´S. Blazy B. Robillard E. Soutif Journ´ees Graphes et Algorithmes 2007 Pr´esentation du probl`eme et de son cadre d’´etude
R´esolution du probl`eme
Conclusion et perspectives
Plan
1 Pr´esentation du probl`eme et de son cadre d’´etude
Cadre d’´etude
Allocation de registres
´Etat de l’art
2 R´esolution du probl`eme
D´emarche g´en´erale
Coloration avec pr´ef´erences et multicoupe minimale
´S. Blazy B. Robillard E. Soutif Journ´ees Graphes et Algorithmes 2007 Pr´esentation du probl`eme et de son cadre d’´etude Cadre d’´etude
R´esolution du probl`eme Allocation de registres
´Conclusion et perspectives Etat de l’art
Contexte d’´etude
Besoin de logiciels sursˆ (domaines s´ecuritaires)
⇒ D´eveloppement de m´ethodes formelles
Probl`eme La compilation n’est pas sureˆ
⇒ Besoin de compilateurs certifi´es
Besoin de code efficace
⇒ Recours `a la recherche op´erationnelle
´S. Blazy B. Robillard E. Soutif Journ´ees Graphes et Algorithmes 2007 Pr´esentation du probl`eme et de son cadre d’´etude Cadre d’´etude
R´esolution du probl`eme Allocation de registres
´Conclusion et perspectives Etat de l’art
Allocation de registres
Ex´ecution de programme
⇒ Acc`es m´emoire par le ...

Sujets

Informations

Publié par
Nombre de lectures 53
Langue Catalan
CEDRIC,e´quipesCPRetOCSandrineBlazy,BenoıˆtRobillardetE´ricSoutifVe´rificationformelledelare´solutiond’unproble`medegraphestriangule´sColorationavecpre´fe´rencesdanslesgraphes9Novembre20077002semhtiroglAtesehparGsee´nruoJfituoS.E´dralliboR.ByzalB.SsevitcepsreptenoisulcnoCeme`lborpudnoitulose´Redute´derdacnosedteeme`lborpudnoitatnese´rP
7002semhtiroglAtesehparGsee´nruoJfituoS.E´dralliboR.ByzalB.S2Re´solutionduproble`meDe´marchege´ne´raleColorationavecpre´fe´rencesetmulticoupeminimale1Pre´sentationduproble`meetdesoncadred’e´tudeCadred’e´tudeAllocationderegistresE´tatdelartnalPsevitcepsreptenoisulcnoCeme`lborpudnoitulose´Redute´derdacnosedteeme`lborpudnoitatnese´rP
CsevitcepsreptenoisulcnoCeme`lborpudnoitulose´Redute´derdacnosedteeme`lborpudnoitatnese´rPBesoindecodeefficaceProble`meLacompilationn’estpassˆuree´msellemrofsedohtDe´veloppementdeBesoindelogicielssuˆrs(domainesse´curitaires)Contexted’e´tude7002semhtiroglAtesehparGsee´nruoJfituoS.E´dralliboR.ByzalB.Sellennoitare´poehcrehcerala`sruoceRse´itrecsruetalipmocednioseBtraledtatE´sertsigerednoitacollAedute´derda
ituoS.E´dralliboR.ByzalB.S)ediparse`ccaPassagea`unnombrelimite´deregistresKQuellesvariablessontdansquelsregistresa`toutmomentdel’exe´cutionduprogramme?aAllocationderegistres`eloadetstore)gAcce`sme´moirepaaExe´cutiondeprogrammekAllocationderegistrescotsedsenoz(sertsigeredecnetsixEsnoitcurtsni(ruessecorpelrtraledtatE´sertsigerednoitacollAedute´derdaCsevitcepsreptenoisulcnoCeme`lborpudnoitulose´Redute´derdacnosedteeme`lborpudnoitatnese´rP7002semhtiroglAtesehparGsee´nruoJf
7002semhtiroglAtesehparGsee´nruoJfituoS.E´dralliboR.ByzalB.Ssetnere´idsrueluocedse´time´rtxedecnere´fe´rpedseteˆrasedsdiopsedemmosaSommets=VariablesduprogrammeDeuxtypesd’areˆtes1Areˆtesd’interf´erence(v1,v2)siv1etv2nepeuventeˆtredanslemeˆmeregistre2Areˆtesdepre´fe´rence(v1,v2)s’ilseraitpre´fe´rablequev1etv2soientdanslemeˆmeregistrelMode´lisationparungraphed’interfe´rence(construitgraˆcea`uneanalysedugraphedeflotdecontrˆole)tMod´elisationparunproble`medecolorationnasiminimnoitaroloc-KenurevuorTelbairaveuqahcruopertsigeredxiohC=ehpargudnoitaroloc-KtraledtatE´sertsigerednoitacollAedute´derdaCsevitcepsreptenoisulcnoCeme`lborpudnoitulose´Redute´derdacnosedteeme`lborpudnoitatnese´rP
7002semhtiroglAtesehparGsee´nruoJfituoS.E´dralliboR.ByzalB.SsedstraledtatE´sertsigerednoitacollAedute´derdaCsevitcepsreptenoisulcnoCeme`lborpudnoitulose´Redute´derdacnosedteeme`lborpudnoitatnese´rPTrouveruneK-colorationminimisantlasommedespoidareˆtesdepre´fe´renced’extre´mite´sdecouleursdiffe´rentesK-colorationdugraphe=Choixderegistrepourchaquevariable1Areˆtesd’interfe´rence(v1,v2)siv1etv2nepeuventeˆtredanslemeˆmeregistre2Areˆtesdepre´fe´rence(v1,v2)s’ilseraitpre´fe´rablequev1etv2soientdanslemeˆmeregistreDeuxtypesd’areˆtesSommets=VariablesduprogrammeMode´lisationparungraphed’interf´erence(construitgraˆcea`uneanalysedugraphedeflotdecontroˆle)Mode´lisationparunproble`medecoloration
tacollAedute´derdaCsevitcepsreptenoisulcnoCeme`lborpudnoitulose´Redute´derdacnosedteeme`lborpudnoitatnese´rPExempleedgraphed’interfe´rence7002semhtiroglAtesehparGsee´nruoJfituoS.E´dralliboR.ByzalB.StraledtatE´sertsigerednoi
GrundetHack(2007):algorithmedecoupes(pourgraphecolorable)Proble`meNPMajorite´desgraphesd’interfe´rencetriangule´s(95%)7002semhtiroglAtesehparGsee´nruoJfituoS.E´dralliboR.ByzalB.Secnere´fretnidehpargelrusseuqitsirueH)7002(se´lugnairtsehpargselsnadelicid-traledtatE´traledtatE´sertsigerednoitacollAedute´derdaCsevitcepsreptenoisulcnoCeme`lborpudnoitulose´Redute´derdacnosedteeme`lborpudnoitatnese´rP
elaminimepuocitlumtesecnere´fe´rpcevanoitaroloCelare´ne´gehFusion=TrouveruneK-colorationcVidage=Rendrelegraphed’interfe´renceK-colorablerDe´compositionduproble`meaDe´marchege´ne´raleme´DsevitcepsreptenoisulcnoCeme`lborpudnoitulose´Redute´derdacnosedteeme`lborpudnoitatnese´rP7002semhtiroglAtesehparGsee´nruoJfituoS.E´dralliboR.ByzalB.S...noisufteegadiVnoN2lamitpotatluse´RnoisuFiuO1e´tilibaroloc-KedtseT)dnamruogogla(sehpargsecsnadelaimonylopnoitaroloCtnevuossulpele´lugnairtecnere´fretnidehparG
7002semhtiroglAtesehparGsee´nruoJfituoS.E´dralliboR.ByzalB.Slamitpotatluse´RDe´compositionduproble`me)Vidage=Rendrelegraphed’interfe´renceK-colorabledFusion=TrouveruneK-colorationnGraphed’interfe´rencetriangule´leplussouventamTestdeK-colorabilite´r2NonVidageetfusion...u1OuiFusionoDe´marchege´ne´ralegogla(sehpargsecsnadelaimonylopnoitaroloCelaminimepuocitlumtesecnere´fe´rpcevanoitaroloCelare´ne´gehcrame´DsevitcepsreptenoisulcnoCeme`lborpudnoitulose´Redute´derdacnosedteeme`lborpudnoitatnese´rP
rPApprocheneuedxspmet7002semhtiroglAtesehparGsee´nruoJfituoS.E´dralliboR.ByzalB.Selaminimepuocitlumtesecnere´fe´rpcevanoitaroloCelare´ne´gehcrame´DsevitcepsreptenoisulcnoCeme`lborpudnoitulose´Redute´derdacnosedteeme`lborpudnoitatnese´