Un nou llenguatge de programació per a ordinadors d’alt rendiment | Notícies del MIT

La informàtica d’alt rendiment és necessària per a un nombre cada vegada més gran de tasques, com ara el processament d’imatges o diverses aplicacions d’aprenentatge profund a les xarxes neuronals, on s’han d’explorar munts immensos de dades i fer-ho amb una rapidesa raonable, o en cas contrari podria ser ridícul. quantitats de temps. Es creu àmpliament que, en la realització d’operacions d’aquest tipus, hi ha intercanvis inevitables entre velocitat i fiabilitat. Si la velocitat és la màxima prioritat, segons aquesta visió, és probable que la fiabilitat en patirà, i viceversa.

No obstant això, un equip d’investigadors, basat principalment al MIT, està posant en dubte aquesta noció, afirmant que, de fet, es pot tenir-ho tot. Amb el nou llenguatge de programació, que han escrit específicament per a la informàtica d’alt rendiment, diu Amanda Liu, estudiant de doctorat de segon any del MIT Computer Science and Artificial Intelligence Laboratory (CSAIL), “la velocitat i la correcció no han de competir. . En canvi, poden anar junts, de la mà, en els programes que escrivim”.

Liu, juntament amb Gilbert Louis Bernstein postdoc de la Universitat de Califòrnia a Berkeley, el professor associat del MIT Adam Chlipala i el professor adjunt del MIT Jonathan Ragan-Kelley, van descriure el potencial de la seva creació recentment desenvolupada, “A Tensor Language” (ATL), el mes passat a la conferència Principis dels llenguatges de programació a Filadèlfia.

“Tot el que hi ha a la nostra llengua”, diu Liu, “està dirigit a produir un sol nombre o un tensor”. Els tensors, al seu torn, són generalitzacions de vectors i matrius. Mentre que els vectors són objectes unidimensionals (sovint representats per fletxes individuals) i les matrius són matrius bidimensionals de nombres familiars, els tensors són nomatrius -dimensionals, que podrien prendre la forma d’una matriu de 3x3x3, per exemple, o alguna cosa de dimensions encara més altes (o inferiors).

L’objectiu d’un algorisme o programa informàtic és iniciar un càlcul particular. Però hi pot haver moltes maneres diferents d’escriure aquest programa: “una varietat desconcertant de realitzacions de codi diferents”, com van escriure Liu i els seus coautors en el seu document de conferència que es publicarà aviat, algunes considerablement més ràpides que altres. La raó principal d’ATL és aquesta, explica: “Atès que la informàtica d’alt rendiment requereix tant de recursos, voleu poder modificar o reescriure els programes en una forma òptima per accelerar les coses. Sovint s’inicia amb un programa que és més fàcil d’escriure, però potser no és la manera més ràpida d’executar-lo, de manera que encara calen més ajustos”.

Com a exemple, suposem que una imatge està representada per una matriu de 100 x 100 números, cadascun corresponent a un píxel, i voleu obtenir un valor mitjà per a aquests números. Això es podria fer en un càlcul en dues etapes determinant primer la mitjana de cada fila i després obtenint la mitjana de cada columna. ATL té un conjunt d’eines associat, el que els informàtics anomenen un “marc”, que podria mostrar com aquest procés de dos passos es podria convertir en un procés d’un sol pas més ràpid.

“Podem garantir que aquesta optimització és correcta utilitzant una cosa que es diu assistent de prova”, diu Liu. Amb aquest objectiu, el nou llenguatge de l’equip es basa en un llenguatge existent, Coq, que conté un assistent de prova. L’assistent de prova, al seu torn, té la capacitat inherent de demostrar les seves afirmacions d’una manera matemàticament rigorosa.

Coq tenia una altra característica intrínseca que el feia atractiu per al grup basat en el MIT: els programes escrits en ell, o les seves adaptacions, sempre acaben i no poden funcionar per sempre en bucles interminables (com pot passar amb els programes escrits en Java, per exemple). “Executem un programa per obtenir una única resposta: un nombre o un tensor”, sosté Liu. “Un programa que no s’acabi mai seria inútil per a nosaltres, però la terminació és una cosa que obtenim gratuïtament fent ús de Coq”.

El projecte ATL combina dos dels principals interessos de recerca de Ragan-Kelley i Chlipala. Ragan-Kelley fa temps que s’ha preocupat per l’optimització dels algorismes en el context de la informàtica d’alt rendiment. Chlipala, per la seva banda, s’ha centrat més en la verificació formal (com en les matemàtiques) d’optimitzacions algorítmiques. Això representa la seva primera col·laboració. Bernstein i Liu es van incorporar a l’empresa l’any passat i ATL és el resultat.

Ara és el primer, i fins ara l’únic, llenguatge tensor amb optimitzacions verificades formalment. Liu adverteix, però, que ATL encara és només un prototip, encara que prometedor, que s’ha provat en diversos programes petits. “Un dels nostres objectius principals, mirant cap al futur, és millorar l’escalabilitat d’ATL, de manera que es pugui utilitzar per als programes més grans que veiem al món real”, diu.

En el passat, les optimitzacions d’aquests programes normalment s’havien fet a mà, de manera molt més ad hoc, que sovint implicava assaig i error i, de vegades, una gran quantitat d’errors. Amb ATL, afegeix Liu, “la gent podrà seguir un enfocament molt més basat en principis per reescriure aquests programes, i fer-ho amb més facilitat i més seguretat de la correcció”.

.

Leave a Comment

Your email address will not be published. Required fields are marked *