Un calcul haute performance est nécessaire pour un nombre toujours croissant de tâches – telles que le traitement d’images ou diverses applications d’apprentissage en profondeur sur des réseaux de neurones – où il faut parcourir d’énormes piles de données et le faire assez rapidement, sinon cela pourrait prendre ridicule quantités de temps. Il est largement admis que, dans la réalisation d’opérations de ce type, il existe des compromis inévitables entre rapidité et fiabilité. Si la vitesse est la priorité absolue, selon ce point de vue, la fiabilité en souffrira probablement, et vice versa.
Cependant, une équipe de chercheurs, basée principalement au MIT, remet cette notion en question, affirmant qu’on peut, en fait, tout avoir. Avec le nouveau langage de programmation, qu’ils ont écrit spécifiquement pour le calcul haute performance, explique Amanda Liu, doctorante en deuxième année au Laboratoire d’informatique et d’intelligence artificielle du MIT (CSAIL), « la vitesse et l’exactitude n’ont plus à rivaliser . Au lieu de cela, ils peuvent aller de pair, main dans la main, dans les programmes que nous écrivons.
Liu – avec l’Université de Californie à Berkeley postdoc Gilbert Louis Bernstein, le professeur agrégé du MIT Adam Chlipala et le professeur adjoint du MIT Jonathan Ragan-Kelley – ont décrit le potentiel de leur création récemment développée, “A Tensor Language” (ATL), le mois dernier à la conférence Principles of Programming Languages à Philadelphie.
“Tout dans notre langue”, dit Liu, “vise à produire soit un nombre unique, soit un tenseur”. Les tenseurs, à leur tour, sont des généralisations de vecteurs et de matrices. Alors que les vecteurs sont des objets unidimensionnels (souvent représentés par des flèches individuelles) et que les matrices sont des tableaux de nombres bidimensionnels familiers, les tenseurs sont n-des tableaux dimensionnels, qui pourraient prendre la forme d’un tableau 3x3x3, par exemple, ou quelque chose de dimensions encore plus élevées (ou inférieures).
Tout l’intérêt d’un algorithme ou d’un programme informatique est d’initier un calcul particulier. Mais il peut y avoir de nombreuses façons différentes d’écrire ce programme – “une variété déconcertante de différentes réalisations de code”, comme l’ont écrit Liu et ses coauteurs dans leur article de conférence qui sera bientôt publié – certaines beaucoup plus rapides que d’autres. La principale raison d’être de l’ATL est la suivante, explique-t-elle : “Étant donné que le calcul haute performance est si gourmand en ressources, vous voulez pouvoir modifier ou réécrire les programmes dans une forme optimale afin d’accélérer les choses. On commence souvent avec un programme qui est le plus facile à écrire, mais ce n’est peut-être pas le moyen le plus rapide de l’exécuter, de sorte que d’autres ajustements sont encore nécessaires.
Par exemple, supposons qu’une image soit représentée par un tableau de nombres 100×100, chacun correspondant à un pixel, et que vous souhaitiez obtenir une valeur moyenne pour ces nombres. Cela pourrait être fait dans un calcul en deux étapes en déterminant d’abord la moyenne de chaque ligne, puis en obtenant la moyenne de chaque colonne. ATL a une boîte à outils associée – ce que les informaticiens appellent un “cadre” – qui pourrait montrer comment ce processus en deux étapes pourrait être converti en un processus en une étape plus rapide.
“Nous pouvons garantir que cette optimisation est correcte en utilisant ce qu’on appelle un assistant de preuve”, déclare Liu. À cette fin, le nouveau langage de l’équipe s’appuie sur un langage existant, Coq, qui contient un assistant de preuve. L’assistant de preuve, à son tour, a la capacité inhérente de prouver ses assertions d’une manière mathématiquement rigoureuse.
Coq avait une autre caractéristique intrinsèque qui le rendait attrayant pour le groupe basé sur le MIT : les programmes écrits dedans, ou des adaptations de celui-ci, se terminent toujours et ne peuvent pas s’exécuter indéfiniment sur des boucles sans fin (comme cela peut arriver avec des programmes écrits en Java, par exemple). “Nous exécutons un programme pour obtenir une réponse unique – un nombre ou un tenseur”, affirme Liu. “Un programme qui ne se termine jamais nous serait inutile, mais la résiliation est quelque chose que nous obtenons gratuitement en utilisant Coq.”
Le projet ATL combine deux des principaux intérêts de recherche de Ragan-Kelley et Chlipala. Ragan-Kelley s’intéresse depuis longtemps à l’optimisation des algorithmes dans le contexte du calcul haute performance. Chlipala, quant à lui, s’est davantage concentré sur la vérification formelle (comme dans le cas d’une vérification mathématique) des optimisations algorithmiques. Il s’agit de leur première collaboration. Bernstein et Liu ont été intégrés à l’entreprise l’année dernière, et ATL en est le résultat.
Il se présente maintenant comme le premier, et jusqu’à présent le seul, langage tenseur avec des optimisations formellement vérifiées. Liu prévient cependant qu’ATL n’est encore qu’un prototype – bien que prometteur – qui a été testé sur un certain nombre de petits programmes. “L’un de nos principaux objectifs, pour l’avenir, est d’améliorer l’évolutivité d’ATL, afin qu’il puisse être utilisé pour les programmes plus importants que nous voyons dans le monde réel”, dit-elle.
Dans le passé, les optimisations de ces programmes étaient généralement effectuées à la main, de manière beaucoup plus ponctuelle, ce qui impliquait souvent des essais et des erreurs, et parfois beaucoup d’erreurs. Avec ATL, ajoute Liu, “les gens pourront suivre une approche beaucoup plus fondée sur des principes pour réécrire ces programmes – et le faire avec une plus grande facilité et une plus grande assurance d’exactitude”.
.