Automation in Dense Linear Algebra

Abstract. In this article we look at the generation of libraries for dense linear algebra operations from a different perspective: instead of focus-ing on the optimization (possibly automatically) of a routine, we address the question “what would it take for a computer to mechanically (au-tomatically) generate high-performance algorithms, much like a human expert?”. We will show that for a large class of operations, the math-ematical description of the input and output variables represents the necessary and sufficient information for a symbolic system to generate loop-based algorithms as well as high-performance routines. Surprisingly, the generation process is entirely prescribed by a proof of correctness: taking Dijkstra’s advice, rather than starting from an algorithm and trying to prove its correctness, we systematically build one so that its correctness is guaranteed. This methodology is thus fundamentally differ-ent with respect to a standard auto-tuning approach: while auto-tuning often performs a parameter optimization over a large search space, our methodology and system rely on symbolic and algebraic transformations, and in principle, can be used to produce cost and error analyses hand in hand with the generated algorithms.