At the Principles of Programming Languages Conference in Philadelphia last month, Amanda Liu, a second-year PhD student at the MIT Computer Science and Artificial Intelligence Laboratory (CSAIL), said that using their new programming language designed specifically for high-performance computing can be a good balance between speed and correctness. Previously, it was widely believed that there was an inevitable trade-off between speed and reliability.
The ATL language aims to produce a number or tensor, and the so-called tensor is the generalization of vectors and matrices.
Vectors are one-dimensional objects (usually represented by separate arrows), and matrices are arrays of two-dimensional numbers that are relatively familiar to faces.
Tensors, on the other hand, are n-dimensional arrays, such as arrays that can be used in 3×3×3, or higher/lower dimensions.
a verified framework for optimizing tensor programs（via）
The whole point of a computer algorithm or program is to start a particular calculation. However, to achieve the goal, it can be written in many different ways. As the research team writes in an upcoming conference paper:
The variety of different code implementations is dizzying, and some scenarios are much faster.
But given the exaggerating resource overhead of high-performance computing, ATL wanted to modify or rewrite programs in a more efficient way.
The average developer is accustomed to starting programming where it is easiest to start, but this obviously does not take into account the best operational efficiency, so further tuning optimization is required.
Suppose the image is represented by an array of numbers 100×100, each of which corresponds to a pixel, and you want to get the mean of these numbers.
This work can be done with two-order calculations, first determining the average of each row and then getting the average of each column.
ATL provides a related toolkit — what computer scientists call a "framework" — that shows how to translate these two steps into a faster one-step process.
Liu adds: We can use the so-called "proof assistant" to ensure that this optimization is correct.
With this in mind, the team built the new language on top of the existing Coq language. And the proof assistant contained therein has the inherent ability to prove its assertions in a mathematically rigorous way.
However, in the eyes of the MIT team, Coq has another commendable intrinsic feature - the programs written or adapted to it cannot run endlessly in an infinite loop.
For example, this can happen with a program written in Java. We run a program to get a single answer — a number, or a tensor.
A program that never terminates is useless to us, but terminate is a feature we can get for free using Coq.
It can only be mentioned that the ATL project combines the results of two studies, Ragan-Kelley and Chlipala, the former of which has long been concerned with algorithm optimization in the context of high-performance computing.
Chlipala, meanwhile, is more focused on the formalization of algorithmic optimizations (e.g., mathematical-based validation), but ATL is the first time both have collaborated – Bernstein and Liu joined forces last year and produced ATL.
ATL is the first and so far only tensor language with formal validation optimizations. ATL is still in the prototype stage, but the research team has tested many small programs, and it can be seen that it has a fairly bright future.
Going forward, one of their main goals is to improve the scalability of ATL so that it can be used for larger programs that we see in the real world.
Previously, the optimization of these programs usually required manual work. In addition to the problems that need to be solved temporarily, there are always repeated experiments involved, so it is inevitable that a large number of errors will occur.
The good news is that with ATL, we can expect to follow a more principled approach to rewriting these programs — easier and more robustly.