Si je prends un exemple pour illustrer la chose. Dans la vidéo de la conférence sur JML (dont le lien était erroné, le voici), l'orateur expose sur un cas particulier une méthode d'analyse statique dite analyse polyédrique (vers la 40ème minute). Il conclue l'étude de cette exemple avec une diapo qui contient ce passage :
Juste un mot là-dessus : premièrement je n'ai pas encore vu la vidéo1.
L'analyse polyédrique a été proposée pour l'optimisation et la parallélisation en compilation depuis la fin des années 80 (voir ici par exemple pour un résumé du modèle). Lorsque j'ai décrit la technique à un pote bien plus avancé en maths que moi (faire une analyse de formes convexes dans un domaine discret), il a tout de suite pigé la difficulté (dans le domaine continu, c'est « trivial », mais dans le domaine discret, pas du tout), et a proposé de suite la première solution utilisée dans ce cas : utiliser un solveur de programmation linéaire entière (pas sûr de la traduction de integer linear programming solver). Et c'est ce qu'a fait Feautrier à l'époque (il a écrit PIP rien que pour ça).
Mais utiliser un solveur ILP mène à de sérieuses contraintes, entre autres que le temps de résolution des (in)équations augmente exponentiellement avec la complexité du nid de boucle à paralléliser/optimiser. De nos jours il y a enfin quelques compilateurs/transpilers qui sont relativement efficaces pour correctement compiler tout ça dans un temps raisonnable, et qui ne passent pas nécessairement par un solveur ILP (et donc le temps d'exploration des espaces d'itération est bien moins grand), mais même dans GCC qui a (avait?) une branche pour les optimisations suivant le modèle polyédrique, ce ne serait jamais activé par défaut.
Bref. Pour passer d'un modèle mathématique correct, et qui fonctionne sur des programmes/boucles jouet, à un compilateur qui peut compiler du « vrai » code (principalement scientifique), il a fallu attendre environ 20 ans (et sacrifier pas mal de thésards à l'autel du modèle polyédrique). Et malgré tout, ce n'est toujours pas intégré dans les compilateurs « mainstream » (tout au plus est-ce une option qu'il faut activer volontairement), car les résultats mathématiques ne se réduisent pas nécessairement en possibilité d'implémentation efficace.
Je suis en train de la télécharger, mais apparemment depuis les US ça prend 300 ans. ↩
[^] # Re: Solution à base de types variants en ADA
Posté par lasher . En réponse à la dépêche Sortie de GHC 8.0.2 et une petite histoire de typage statique. Évalué à 3.
Juste un mot là-dessus : premièrement je n'ai pas encore vu la vidéo1 .
L'analyse polyédrique a été proposée pour l'optimisation et la parallélisation en compilation depuis la fin des années 80 (voir ici par exemple pour un résumé du modèle). Lorsque j'ai décrit la technique à un pote bien plus avancé en maths que moi (faire une analyse de formes convexes dans un domaine discret), il a tout de suite pigé la difficulté (dans le domaine continu, c'est « trivial », mais dans le domaine discret, pas du tout), et a proposé de suite la première solution utilisée dans ce cas : utiliser un solveur de programmation linéaire entière (pas sûr de la traduction de integer linear programming solver). Et c'est ce qu'a fait Feautrier à l'époque (il a écrit PIP rien que pour ça).
Mais utiliser un solveur ILP mène à de sérieuses contraintes, entre autres que le temps de résolution des (in)équations augmente exponentiellement avec la complexité du nid de boucle à paralléliser/optimiser. De nos jours il y a enfin quelques compilateurs/transpilers qui sont relativement efficaces pour correctement compiler tout ça dans un temps raisonnable, et qui ne passent pas nécessairement par un solveur ILP (et donc le temps d'exploration des espaces d'itération est bien moins grand), mais même dans GCC qui a (avait?) une branche pour les optimisations suivant le modèle polyédrique, ce ne serait jamais activé par défaut.
Bref. Pour passer d'un modèle mathématique correct, et qui fonctionne sur des programmes/boucles jouet, à un compilateur qui peut compiler du « vrai » code (principalement scientifique), il a fallu attendre environ 20 ans (et sacrifier pas mal de thésards à l'autel du modèle polyédrique). Et malgré tout, ce n'est toujours pas intégré dans les compilateurs « mainstream » (tout au plus est-ce une option qu'il faut activer volontairement), car les résultats mathématiques ne se réduisent pas nécessairement en possibilité d'implémentation efficace.
Je suis en train de la télécharger, mais apparemment depuis les US ça prend 300 ans. ↩