Optimisation de programmes annotés par des assertions
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.