Paolo Bientinesi, Sergey Kolos and Robert van de Geijn
Department of Computer Science
The University of Texas at Austin
USA
email: {pauldj@cs,skolos@mail,rvdg@cs}.utexas.edu
It is a common situation when a computational scientist encounters a matrix operation that must be solved that does not fit the functionality of widely available ``black-box'' libraries. In this situation, the alternatives become to cast the operation into what is available (which often involves computation that is not essential), to modify the black-box library (which often requires extensive knowledge of that library), or to write a library from scratch. It is our vision that in this situation one should be able to visit a website, fill out a form with information about the operation to be performed and about the target architectures, click the SUBMIT button, and receive an optimized library routine for that operation even if the operation has not previously been implemented.
In this paper, we review recent results from the Formal Linear Algebra Methods Environment (FLAME) project regarding the theory of deriving and analysing dense linear algebra algorithms. We observe that the methodology is sufficiently systematic that it can be automated. We describe two prototype efforts, tools built upon the Mathematica environment, that demonstrate this automation. The first is a fully automatic system that, given a matrix operation, produced all possible correct algorithms for the given operation. While the applicability of the prototype was very limited, it demonstrated that full automation of all stages of the derivation is possible for the target operation. The second effort is a more interactive tool that guides the user through the derivation process. Strong evidence now exists that it can been used to semi-automatically generate all algorithms for all operations to which FLAME has been applied in the past. This includes the bulk of the operations supported by LAPACK, operations on banded matrices, Arnoldi and Lanczos methods, and operations encountered in control theory.