High-performance computing is required for an expanding variety of jobs, such as image processing and various deep learning systems based on neural networks, where massive amounts of data must be processed quickly or forever. When doing activities of this nature, compromises between speed and dependability are unavoidable. If speed is the most important factor, reliability suffers, and vice versa.
The best of both worlds
According to MIT researchers, one can have both. According to Amanda Liu of the Laboratory for Computer Science and Artificial Intelligence (CSAIL), with a new programming language built expressly for high-performance computing, speed and dependability may coexist.
At the Philadelphia Programming Principles Conference, the promise of A Tensor Language (ATL) was presented.
“Everything in our language is focused on constructing one number or tensor,” Liu explains. Tensors are vector and matrix generalizations. While vectors are one-dimensional objects (typically represented by single arrows) and matrices are two-dimensional arrays of numbers, tensors are n-dimensional arrays that can have the shape of 3x3x3 fields or somewhat bigger (or lower) dimensions.
“Because high-performance computing is so resource-intensive, you want to be able to modify or rewrite programs in an optimal way to speed things up. It often starts with the easiest program to write, but it may not be the fastest way to run it,” says Liu.
As an example, suppose an image is represented by a series of numbers of size 100×100 each corresponding to a pixel, and you want to get an average value for those numbers. This could be done in a two-phase calculation by first determining the average of each row and then obtaining the average of each column. ATL has an associated tool – what computer scientists call a “framework” – that could show how this two-step process can be turned into a faster one-step process.
“We can guarantee that this optimization is accurate by using a proof assistant,” Liu says. To this end, the team’s new language builds on the existing language, Coq, which includes a test assistant. He in turn can prove his claims in a mathematically rigorous way.
Programs written in Coqu cannot run forever in infinite loops, as can happen with programs written in Java.
“We run the program to get one answer – a number or a tensor,” Liu explains. “A program that never breaks would be useless to us, and we get a break by using Coq.”
ATL is the first tensor language with formally tested optimizations, but it is still just a promising prototype. Researchers now want to improve its scalability so that it can be used for larger real-world programs.