“Speed and accuracy don’t have to be in competition… they can work together, hand in hand.”
High-performance computing is essential for many tasks, such as image processing and deep learning applications on neural networks. These tasks require the ability to quickly and efficiently process huge amounts of data. Otherwise, it can take a ridiculous amount of time. There are often unavoidable tradeoffs when performing operations like these. According to this view, reliability will suffer if speed is the highest priority.
A team of researchers at MIT is challenging this notion and claiming that you can have it all. Amanda Liu (second-year Ph.D. student at MIT Computer Science and Artificial Intelligence Laboratory) says that speed and accuracy don’t have to compete with the new programming language. They can work together in the programs that we write.
Liu, the University of California at Berkeley postdoc Gilbert Louis Bernstein and MIT Associate Professor Adam Chlipala presented the potential of their newly developed creation, ” a Tensor Language“, last month at Philadelphia’s Principles of Programming Languages conference.
Liu states, “everything in our language is aimed at producing either one number or a Tensor.” Tensors are, in turn, generalizations vectors and matrixes. Vectors are one-dimensional objects, often represented by individual arrows, and matrices are two-dimensional arrays that contain numbers. Tensors are n-dimensional arrays. They can be 3x3x3 or even larger (or smaller) dimensions.
A computer program or algorithm is designed to perform a specific computation. There are many ways to write that program. Liu and her coauthors call it “a bewildering array of code realizations” — some much faster than others. ATL means: “Given high-performance computing’s resource-intensive nature, you want to be capable of modifying or rewriting programs to increase speed.” It is common to start with the easiest program to write. However, it may not be the fastest to run. Therefore, further adjustments are often necessary.
Let’s say an image is represented as a 100×100 array number of numbers. Each number corresponds to a pixel. You want to find the average value for these numbers. This could be accomplished in two stages. First, you would calculate the average value for each row. Then, you would calculate the average value for each column. ATL also has a toolkit, which computer scientists refer to as a “framework”, that could help you convert this two-step process into a quick one-step process.
Liu states, “we can guarantee that the optimization is correct using a proof assistant.” The team’s new language is built upon Coq, an existing language that includes a proof assistant. The proof assistant has the inherent ability to prove its assertions mathematically rigorously.
Coq also had an intrinsic feature that attracted the MIT-based group. Programs written in it or adaptations thereof always terminate and can’t run endless loops (as with Java programs, for instance). Liu says a program is run to obtain a single answer, a number or a tensor. We would consider a program that never ends useless, but Coq allows us to terminate programs for no cost.
The ATL project brings together two of Ragan-Kelley’s main research interests, Chlipala and Chlipala. Ragan-Kelley’s research has been focused on optimizing algorithms for high-performance computing. Chlipala has focused more on the formal (as in mathematically-based) verification of algorithmic optimizations. This is their first collaboration. ATL was the result of Bernstein and Liu’s collaboration last year.
It is now the first and only tensor language to have formally verified optimizations. Though it’s a promising prototype, Liu warns that ATL is still a prototype and has been tested on small programs. She says that ATL’s main goal is to be more scalable so it can be used in larger programs.
Optimizations of these programs were done manually in the past. This often involved trial and error and sometimes a lot of error. Liu says that ATL will allow people to follow a more systematic approach to rewriting programs. This will make it easier and give them greater certainty of their correctness.