, стверджує, що розробляє прототип нової мови програмування.){kind=link}
High-performance computing is nodig om steeds meer taken op te lossen - zoals beeldverwerking of verschillende deep learning-toepassingen op neurale netwerken - waarbij je enorme hoeveelheden gegevens moet verwerken en dit snel genoeg moet doen, anders kan het ongelooflijk veel tijd kosten. tijd. Er wordt algemeen aangenomen dat bij het uitvoeren van dergelijke bewerkingen een compromis tussen snelheid en betrouwbaarheid onvermijdelijk is. Volgens deze denkwijze, als snelheid een prioriteit is, zal de betrouwbaarheid eronder lijden en vice versa.
Een groep onderzoekers, voornamelijk gevestigd aan het Massachusetts Institute of Technology (MIT), betwist dit idee echter met het argument dat je eigenlijk alles kunt hebben. Volgens Amanda Liu, een tweedejaars student aan het Computer Science and Artificial Intelligence Laboratory (CSAIL) van het MIT, met een nieuwe programmeertaal die ze speciaal voor high-performance computing hebben geschreven, "hoeft snelheid en correctheid niet te concurreren. Integendeel, ze kunnen samengaan, zij aan zij, in de programma's die we schrijven." Liu en haar team spraken vorige maand op de Principles of Programming Languages-conferentie in Philadelphia over het potentieel van hun nieuw gecreëerde A Tensor Language (ATL).
"Alles in onze taal", zegt Liu, "is erop gericht een enkel getal of een tensor te krijgen." Tensoren zijn op hun beurt een generalisatie van vectoren en matrices. Terwijl vectoren eendimensionale objecten zijn (vaak weergegeven door individuele pijlen) en matrices bekende tweedimensionale reeksen getallen zijn, zijn tensoren n-dimensionale reeksen die bijvoorbeeld de vorm kunnen aannemen van een 3×3×3 reeks, of zelfs hogere (of lage) dimensie.
De essentie van een computeralgoritme of programma is het initiëren van een bepaalde berekening. Maar er kunnen veel verschillende manieren zijn om dit programma te schrijven -- "een verrassende verscheidenheid aan verschillende code-implementaties", zoals Liu en haar co-auteurs in hun paper schrijven -- waarvan sommige aanzienlijk sneller zijn dan andere. De belangrijkste grondgedachte achter ATL, legt ze uit, is deze: "Aangezien high-performance computing zo veel middelen vergt, wil je programma's in een optimale vorm kunnen aanpassen of herschrijven om dingen te versnellen. Vaak begin je met het programma dat het gemakkelijkst te schrijven is, maar dat misschien niet de snelste manier is om het uit te voeren, dus je moet nog verdere aanpassingen maken."
De nieuwe commandotaal is gebaseerd op de bestaande Coq-taal, die een proof-helper bevat. De bewijsassistent heeft op zijn beurt het vermogen om zijn beweringen wiskundig precies te bewijzen. Coq heeft nog een eigenschap die het aantrekkelijk maakte voor de MIT-groep: programma's die in die taal zijn geschreven, of een bewerking daarvan, eindigen altijd en kunnen niet oneindig in oneindige lussen draaien.
Nu is het de eerste en tot nu toe de enige tensortaal met formeel geverifieerde optimalisaties. Het MIT-team waarschuwt echter dat ATL nog steeds slechts een prototype is - zij het een veelbelovend exemplaar - dat is getest op een aantal kleine programma's.
Lees ook: