ATL: Il linguaggio dei supercomputer

Il calcolo ad alte prestazioni è necessario per un numero sempre crescente di compiti – come l’elaborazione delle immagini o varie applicazioni di deep learning su reti neurali – in cui si deve processare immense quantità di dati in tempi ragionevoli. È quindi evidente che si debba trovare un compromesso in questo tipo di operazione, tra velocità e affidabilità dei calcoli. Se si dà priorità all’affidabilità del risultato, allora questo andrà probabilmente a scapito della velocità e viceversa.

Ultimamente un team di ricercatori, basato principalmente al MIT, sta mettendo in discussione questo paradigma, sostenendo che si può, in qualche modo avere entrambe le caratteristiche. Hanno, infatti, messo a punto un nuovo linguaggio di programmazione scritto appositamente per il calcolo ad alte prestazioni, dice Amanda Liu, una studentessa del dottorato al secondo anno presso il MIT Computer Science and Artificial Intelligence Laboratory (CSAIL), “la velocità e la correttezza non devono competere fra loro, escludendosi a vicenda, ma possono essere entrambi ottenuti grazie ai programmi che scriviamo”.

Liu – insieme al dottor Gilbert Louis Bernstein dell’Università della California a Berkeley, al professore associato del MIT Adam Chlipala e al professore assistente del MIT Jonathan Ragan-Kelley – ha descritto il potenziale della loro recente creazione, “A Tensor Language” (ATL), presentandola il mese scorso alla conferenza Principles of Programming Languages a Philadelphia.

“Nel nostro linguaggio”, dice Liu, “il punto centrale è il ‘tensore’”. I tensori sono generalizzazioni di vettori e matrici. Mentre i vettori sono oggetti unidimensionali (spesso rappresentati da frecce) e le matrici sono familiari matrici bidimensionali di numeri, i tensori, invece, sono matrici n-dimensionali, che potrebbero assumere la forma di una matrice 3x3x3, per esempio, o qualcosa di dimensioni ancora maggiori. Questo è un concetto già conosciuto in geometria.

Lo scopo di un algoritmo o programma del computer è quello di avviare una particolare computazione. Ma, attenzione, lo stesso algoritmo può essere risolto in molti modi diversi.  “Una sconcertante varietà di diverse realizzazioni di codice”, afferma Liu, “e alcuni notevolmente più veloci di altri”. La motivazione principale dietro ATL è questa, spiega: “Dato che il calcolo ad alte prestazioni è così impegnativo in termini di risorse, si vuole essere in grado di modificare, o riscrivere, i programmi in una forma ottimale al fine di accelerare le cose. Spesso si inizia con un programma che è più facile da scrivere, ma che potrebbe non essere il modo più veloce per eseguirlo, così che sono necessari ulteriori aggiustamenti”.

Come esempio, supponiamo che un’immagine sia rappresentata da una matrice 100×100 di numeri, ognuno corrispondente a un pixel e si vuole ottenere un valore medio per questi numeri. Questo potrebbe essere fatto in due fasi distinte, determinando prima la media di ogni riga e poi ottenendo la media di ogni colonna. ATL permette di convertire tale calcolo in due fasi in un processo molto più veloce.

“Possiamo garantire che questa ottimizzazione dia dei risultati corretti utilizzando qualcosa chiamato assistente di prova”, dice Liu. A tal fine, il nuovo linguaggio del team si basa a sua volta su un linguaggio esistente, Coq, che contiene un sistema particolare che ha la capacità intrinseca di dimostrare le sue asserzioni in modo matematicamente rigoroso.

ATL è il primo, e finora l’unico, linguaggio che usa tensori e con ottimizzazioni formalmente verificate. Liu avverte, tuttavia, che ATL è ancora solo un prototipo – anche se promettente – che è stato testato su una serie di piccoli programmi. “Uno dei nostri obiettivi principali, guardando al futuro, è quello di migliorare la scalabilità di ATL, in modo che possa essere utilizzato per i programmi più grandi che vediamo nel mondo reale”, dice.