The new language, say the researchers, addresses the trade-offs between speed and correctness seen with high-performance computing tasks involving immense piles of data, where it’s believed that if speed is the top priority, then reliability will likely suffer, and vice versa. However, say the researchers, with their new language – called A Tensor Language (ATL) – it’s possible to achieve both.

“Speed and correctness do not have to compete,” says Amanda Liu, a second-year PhD student at the MIT Computer Science and Artificial Intelligence Laboratory (CSAIL). “Instead, they can go together, hand-in-hand, in the programs we write.”

Everything in their language, say the researchers, is aimed at producing either a single number or a tensor – a generalization of a vector or matrix. Where vectors are one-dimensional objects (often represented by individual arrows) and matrices are familiar two-dimensional arrays of numbers, tensors are n-dimensional arrays, which could take the form of a 3x3x3 array, for instance, or something of even higher (or lower) dimensions.

The whole point of a computer algorithm or program is to initiate a particular computation. But there can be many different ways of writing that program – in fact, “a bewildering variety of different code realizations,” say the researchers, some of which are considerably speedier than others. This is where ATL comes in.

“Given that high-performance computing is so resource-intensive, you want to be able to modify, or rewrite, programs into an optimal form in order to speed things up,” says Liu. “One often starts with a program that is easiest to write, but that may not be the fastest way to run it, so that further adjustments are still needed.”

作为一个例子,中se an image is represented by a 100×100 array of numbers, each corresponding to a pixel. To get an average value for these numbers, a two-stage computation could be used by first determining the average of each row and then getting the average of each column. ATL, however, has an associated toolkit – a “framework” – that might show how this two-step process could be converted into a faster one-step process.

“We can guarantee that this optimization is correct by using something called a proof assistant,” Liu says.

Toward this end, the researchers’ new language builds upon an existing language, Coq, which contains a proof assistant. The proof assistant, in turn, has the inherent capacity to prove its assertions in a mathematically rigorous fashion.

Coq had another intrinsic feature that made it attractive, say the researchers: programs written in it, or adaptations of it, always terminate and cannot run forever on endless loops (as can happen with programs written in Java, for example).

“We run a program to get a single answer – a number or a tensor,” says Liu. “A program that never terminates would be useless to us, but termination is something we get for free by making use of Coq.”

ATL, say the researchers, now stands as the first – and so far the only – tensor language with formally verified optimizations. Currently ATL is still just a prototype – albeit a promising one – that’s been tested on a number of small programs.

“One of our main goals, looking ahead,” says Liu, “is to improve the scalability of ATL, so that it can be used for the larger programs we see in the real world.”

In the past, optimizations of these programs have typically been done by hand, on a much more ad hoc basis, which often involves trial and error, and sometimes a good deal of error, say the researchers.

ATL,刘说,“人们将能够效仿a much more principled approach to rewriting these programs — and do so with greater ease and greater assurance of correctness.”

For more, see “Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites.”