Tuilage sémantique
Vendredi 11 janvier, Salle de réunion LUG 2
Guillaume Iooss
Résumé:
Certains programmes d’algèbre linéaire (ou de théorie des graphes) manipulant des scalaires possèdent une version alternative manipulant des matrices, et utilisant des opérations matricielles à la place des opérations scalaires. Cette version (blockée) possède une structure identique à la version scalaire, tout en ayant une granularité plus important que la version initiale (scalaire) du programme.
On cherche donc à formaliser la transformation sémantique qui passe d’un programme scalaire à un programme blocké, nommée “tuilage sémantique”. Cette transformation peut être vu comme un blockage des données en matrices, puis un découpage sémantique des instructions d’un programme, afin de gagner en localité. Ses conditions d’applicabilités différent d’un tuilage conventionnel: quelques (rares) applications peuvent donc être tuilable sémantiquement, tout en admettant des dépendances ne permettant pas un tuilage conventionnel.
Plusieurs formalisations possibles de cette transformation sont en cours d’exploration: * Une première possibilité consiste à distinguer les opérations selon les blocs de données utilisés, afin de les isoler pour former des opérations matricielles.On essaye donc d’arriver sur un programme bloqué par transformations sémantiques successives du programme scalaire initial. * La seconde possibilité (plus brutale) consiste à substituer les données et opérations scalaires du programme initial par des données et des opérations matricielles “correspondantes” pour obtenir un programme bloqué candidat. Puis, il nous reste plus qu’à essayer de prouver l’équivalence entre le programme bloqué obtenu et la version scalaire initiale.
Dans les deux approches, un algorithme d’équivalence de programme est utilisé (dans le premier cas, pour reconnaître les opérations matricielles des blocks d’opérations que l’on forme / dans le second cas, pour prouver l’équivalence du programme scalaire avec le programme blocké). En particulier, un tel algorithme doit être capable de gérer les propriétés d’associativité et de commutativité d’un opérateur sur un nombre paramétrique de terme. Nous présenterons donc une extension de l’algorithme de Barthou-Feautrier-Redon afin de gérer (partiellement) de tels cas.