Skip to Main content Skip to Navigation
Reports

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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00072664
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 10:31:59 AM
Last modification on : Wednesday, September 16, 2020 - 4:57:21 PM
Long-term archiving on: : Sunday, April 4, 2010 - 9:20:22 PM

Identifiers

  • HAL Id : inria-00072664, version 1

Collections

Citation

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

Share

Metrics

Record views

127

Files downloads

114