Computer Science Colloquium

Toward a Final Generation of Linear Algebra Libraries

Paolo Bientinesi
The University of Texas at Austin

Friday, January 28, 2005 11:30 A.M.
Room 1302 Warren Weaver Hall
251 Mercer Street
New York, NY 10012-1185

Colloquium Information:


Michael Overton, (212) 998-3121


Over the decades there have always been projects that target "Next Generation Libraries" in various problem domains. High-performance libraries that target linear algebra operations are among the most prominent of these. A question becomes "At what point we will be able to generate a Final Generation Library?". The Formal Linear Algebra Methods Environment (FLAME) project at UT-Austin has demonstrated that classical theoretical results from computer science lead the way in answering that question. What we have discovered is that the algorithms, which are inherently loop-based in this area, can be systematically derived from the mathematical specification of the linear algebra operation. Key is the discovery of how to systematically identify loop-invariants, from which then the loop can be derived to be correct. This advance enables us to derive families of algorithms so that the best (e.g., fastest or most stable) algorithm for a situation can be chosen. By defining APIs so that the code closely resembles the format of the algorithm, the correctness of the code can be asserted. It appears that the methodology can be extended to also systematically derive stability analyses for algorithms within the family, as well as performance analyses. Interestingly, the methodology is sufficiently systematic that it can be automated. Our vision is that someday a user will be able to go to a webpage, specify a linear algebra operation mathematically, describe details of a target architecture/language, and receive a library that is automatically generated -- even if no known algorithm for that operation yet exists in code. In this talk we will overview our preliminary results that show that this vision is within reach.

top | contact