Optimisation de programmes annotés par des assertions

Pierre Amiranoff 1
1 A3 - Advanced analysis to code optimization
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France
Résumé : Dans les codes scientifiques, les traitements répétitifs prennent la forme de boucles qui monopolisent l'essentiel des ressources en temps et en mémoire du calculateur. Les techniques d'optimisation ciblent donc particulièrement ces boucles. Les techniques efficaces existantes ne sont pas généralisables à tous les programmes. Nous montrons sur des exemples que des propriétés sémantiques de haut niveau, qui disparaissent habituellement à l'implémentation, peuvent être mises en mémoire sous forme d'assertions, ce qui permet de valider une parallélisation de boucle. En effet, ces assertions expriment l'indépendance des références-mémoires internes à la boucle. Nous détaillons la procédures de preuve de ces assertions. Nous analysons un programme utilisé dans le domaine des maillages qui combine la restructuration de données avec la recherche et l'exploitation de celles-ci pour des applications diverses. Cette analyse nous conduit à construire un programme équivalent qui peut être parallélisé. Nous resituons notre exemple dans le cadre du modèle Entité-Relation des bases de données relationnelles. Nous instancions notre programme sur 3 exemples d'applications. Nous dégageons des classes de programmes suivant les modalités d'exploitation des résultats acquis lors de la phase de recherche. Ces classes se différencient selon le type de dépendances de données dans les boucles. Enfin, nous illustrons les possibilités de parallélisation par un programme emprunté à la géométrie et deux programmes inspirés de l'Arithmétique. Plus généralement, nous souhaitons contribuer à renforcer l'influence des méthodes de spécifications formelles dans le développement des Application- s Numériques.
Type de document :
Rapport
RR-3983, INRIA. 2000
Liste complète des métadonnées

https://hal.inria.fr/inria-00072664
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 10:31:59
Dernière modification le : jeudi 9 février 2017 - 15:03:52
Document(s) archivé(s) le : dimanche 4 avril 2010 - 21:20:22

Fichiers

Identifiants

  • HAL Id : inria-00072664, version 1

Collections

Citation

Pierre Amiranoff. Optimisation de programmes annotés par des assertions. RR-3983, INRIA. 2000. 〈inria-00072664〉

Partager

Métriques

Consultations de la notice

109

Téléchargements de fichiers

76