Formalisation du modèle polyhédrique: le problème des ...

Julien Narboux, Nicolas Magaud, Bruno Cuervo Parrino, Eric Violard

Description

• cours - matière potentielle : construction

Formalisation du modele polyhedrique: le probleme des depassements arithmetiques Bruno Cuervo Parrino Julien Narboux Eric Violard Nicolas Magaud Universite de Strasbourg - INRIA Camus Decembre 2011, St Hippolyte Nicolas Magaud (UdS) Decembre 2011, St Hippolyte 1 / 39

• probleme des depassements arithmetiques
• description du probleme solution
• boucles imbriquees
• formalisation du modele polyhedrique
• fusion de boucles deroulage de boucles echange de boucles inversions de boucles
• projet objectif

Sujets

• Construction
• Solution
• Cuervo
• Strasbourg
• Bouclé
• Échange

Informations

• Publié par: nosheng
• Nombre de lectures: 59
• Langue: Français

Extrait

Formalisation du modele polyhedrique: le probleme des
depassements arithmetiques
Bruno Cuervo Parrino Julien Narboux Eric Violard
Nicolas Magaud
Universite de Strasbourg - INRIA Camus
Decembre 2011, St Hippolyte
Nicolas Magaud (UdS) Decembre 2011, St Hippolyte 1 / 39Plan
1 Contexte
Le modele polyedrique
La compilation certi ee
2 Le probleme des depassements arithmetiques
Description du Probleme
Solution dans Polly proposee
3 Vers une formalisation en Coq
Nicolas Magaud (UdS) Decembre 2011, St Hippolyte 2 / 39Avertissement
Travail en cours de construction les preuves ne sont pas terminees.
Nicolas Magaud (UdS) Decembre 2011, St Hippolyte 3 / 39Motivations
Inutile de prouver un programme source si le compilateur est bugue.
Les compilateurs sont de plus en plus complexes.
Les parallelisants, speculatifs, . . . , sont particulierement
complexes.
Nicolas Magaud (UdS) Decembre 2011, St Hippolyte 4 / 39Projet
Objectif
Integration du modele polyedrique dans CompCert (Blazy, Leroy, Tristan)
A n de:
A moyen terme ameliorer la localite des donnees (spatiale et temporelle)
A plus long terme exhiber du parallelisme
Projet en collaboration avec Alexandre Pilkiewicz - INRIA Gallium.
Nicolas Magaud (UdS) Decembre 2011, St Hippolyte 5 / 39Modele polyedrique
Idees principales:
La plupart des calculs sont realises dans des boucles imbriquees.
Restriction a des problemes lineaires: on manipule des polyedres dans
nZ .
Nicolas Magaud (UdS) Decembre 2011, St Hippolyte 6 / 39Le cadre
On s’interdit :
for(i=0;i<n;i++)
for(j=0;j<m;j++)
{ x[i*i]=y[j+1]+y[j]; }
Exemple
Et aussi :for(i=0;i<n;i++)
for(i=0;i<n;i++)for(j=0;j<m;j++)
for(j=0;j<m;j++){
{ x[y[i]]=y[j+1]; }x[2*i+j]=y[j+1]+f(y[j]);
}
Ou encore :
for(i=0;i<n*n;i++)
for(j=0;j<m;j++)
{ x[i]=y[j+1]; i:=i+3; }
Nicolas Magaud (UdS) Decembre 2011, St Hippolyte 7 / 39Le cadre
Hypotheses
les acces aux tableaux sont lineaires en les parametres et les indices
de boucles
pas d’e ets de bords
les tableaux sont disjoints (pas d’alias)
Nicolas Magaud (UdS) Decembre 2011, St Hippolyte 8 / 39Quelques transformations de boucles
Pavage de boucles
Distribution et fusion de boucles
Deroulage de boucles
Echange de boucles
Inversions de boucles
Les transformation unimodulaires
Nicolas Magaud (UdS) Decembre 2011, St Hippolyte 9 / 39L’ordre d’execution
for(V1, L1, U1)
for(V2, L2, U2)
...
for(Vn, Ln, Un)
S1;
S2;
...
Sn;
S < Si exe jI J
ssi
I < J_ (I = J^ i < j)lex
c’est a dire
(I; i)< (J; j)lex
Nicolas Magaud (UdS) Decembre 2011, St Hippolyte 10 / 39