Formal methods for high-performance linear algebra libraries

Abstract

A colleague of ours, Dr. Timothy Mattson of Intel, once made the following observation: "Literature professors read literature. Computer Science professors should at least occasionally read code." The point he was making was that in order to write superior prose one needs to read good (and bad) literature. Analogously, it is our thesis that exposure to elegant (and ugly) programs tends to yield the insights which are necessary if one wishes to produce consistently well-written code. Since the advent of high-performance distributed-memory parallel computing, the need for intelligible code has become ever greater. Development and maintenance of libraries for these kinds of architectures is simply too complex to be amenable to conventional approaches to coding. Attempting to do so has led to the production of an abundance of inefficient, anfractuous code that is difficult to maintain and nigh-impossible to upgrade. Having struggled with these issues for more than a decade, we have arrived at a conclusion which is somewhat surprising to us: the answer is to apply formal methods from Computer Science to the development of high-performance linear algebra libraries. The resulting approach has consistently resulted in aesthetically-pleasing, coherent code that greatly facilitates performance analysis, intelligent modularity, and the enforcement of program correctness via assertions. Since the technique is completely language-independent, it lends itself equally well to a wide spectrum of programming languages (and paradigms) ranging from C and Fortran to C++ and Java. In this paper, we illustrate our observations by looking at our Formal Linear Algebra Methods Environment (FLAME). © 2001 by Springer Science+Business Media New York.