Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
Bien que les utilisateurs de calcul haute performance (HPC) soient plus intéressés par les performances brutes, les coûts de stockage et la consommation d'énergie sont devenus des préoccupations importantes. Ces dernières années, l'utilisation du réglage de la précision pour améliorer les métriques de performance est devenu une nouvelle tendance pour économiser les ressources sur les processeurs disponibles. Ce processus est appelé réglage de précision (precision tuning). Dans cette thèse, nous introduisons une nouvelle technique de réglage de précision radicalement différente de celles existantes. Notre approche est basée sur une modélisation sémantique de la propagation des erreurs numériques à travers le programme. Cela génère un système de contraintes dont la solution minimale donne le meilleur réglage de précision du programme. En se basant sur une approche d'analyse statique, nous formulons le problème du réglage de précision avec deux méthodes différentes. La première méthode combine une analyse d'erreurs en avant et en arrière. Ensuite, nos analyses sont exprimées sous la forme d'un ensemble de contraintes linéaires vérifiées par un solveur SMT. La deuxième méthode consiste à générer un problème de programmation linéaire en nombres entiers (ILP) à partir du code source du programme. Cela se fait en raisonnant sur le bit de poids fort et le nombre de bits significatifs des valeurs des variables. La solution entière à ce problème, calculée en temps polynomial par un solveur de programmation linéaire classique, donne une optimisation des types de données en nombre de bits. Un ensemble plus fin d'équations sémantiques est également proposé dans cette thèse. Il utilise la méthode d'itération sur les politiques pour trouver les nouvelles précisions. Les deux méthodes ont été implémentées dans un outil appelé, POP. Nous proposons dans cette thèse une évaluation détaillée des performances de POP sur plusieurs exemples couvrant divers domaines d'application tels que les systèmes embarqués, l'Internet des objets ...