Deriving dense linear algebra libraries. (English) Zbl 1298.65003

Summary: Starting in the late 1960s computer scientists including Dijkstra and Hoare advocated goal-oriented programming and the formal derivation of algorithms. The chief impediment to realizing this for loop-based programs was that a priori determination of loop-invariants, a prerequisite for developing loops, was a task too complex for any but the simplest of operations. Around 2000, these techniques were for the first time successfully applied to the domain of high-performance dense linear algebra libraries. This has led to a multitude of papers (mostly published in the ACM Transactions for Mathematical Software), a system for the mechanical derivation of algorithms, and a high-performance linear algebra library, libflame, that includes more than a thousand variants of algorithms for more than a hundred linear algebra operations. To our knowledge, this success story has unfolded with limited awareness on the part the formal methods community. This paper reports on ten years of experience and is meant to raise that awareness.


65-04 Software, source code, etc. for problems pertaining to numerical analysis
65Fxx Numerical linear algebra
15-04 Software, source code, etc. for problems pertaining to linear algebra
Full Text: DOI Link


[1] Anderson E, Bai Z, Bischof C, Blackford LS, Demmel J, Dongarra JJ, Du Croz J, Hammarling S, Greenbaum A, McKenney A, Sorensen D (1999) LAPACK users’ guide, 3rd edn. SIAM, Philadelphia · Zbl 0934.65030
[2] Bientinesi, P; Gunter, B; Vande Geijn, RA, Families of algorithms related to the inversion of a symmetric positive definite matrix, ACM Trans Math Softw, 35, 1-22, (2008)
[3] Bientinesi, P; Gunnels, JA; Myers, ME; Quintana-Ortí, ES; Geijn, RA, The science of deriving dense linear algebra algorithms, ACM Trans Math Softw, 31, 1-26, (2005) · Zbl 1073.65036
[4] Bientinesi P (2005) Mechanical derivation and systematic analysis of correct linear algebra algorithms. PhD thesis, Department of Computer Sciences, The University of Texas. Technical report TR-06-46
[5] Bientinesi, P; Quintana-Ortí, ES; Geijn, RA, Representing linear algebra algorithms in code: the FLAME application programming interfaces, ACM Trans Math Softw, 31, 27-59, (2005) · Zbl 1073.65037
[6] Bientinesi, P; Geijn, RA, Goal-oriented and modular stability analysis, SIAM J Matrix Anal Appl, 32, 286-308, (2011) · Zbl 1218.65030
[7] Dongarra, JJ; Du Croz, J; Hammarling, S; Duff, I, A set of level 3 basic linear algebra subprograms, ACM Trans Math Softw, 16, 1-17, (1990) · Zbl 0900.65115
[8] Dongarra, JJ; Du Croz, J; Hammarling, S; Hanson, RJ, An extended set of FORTRAN basic linear algebra subprograms, ACM Trans Math Softw, 14, 1-17, (1988) · Zbl 0639.65016
[9] Dijkstra, EW, A constructive approach to the problem of program correctness, BIT, 8, 174-186, (1968) · Zbl 0167.46002
[10] Dijkstra EW (1976) A discipline of programming. Prentice Hall · Zbl 0368.68005
[11] Eijkhout, V; Bientinesi, P; Geijn, R, Towards mechanical derivation of Krylov solver libraries, Procedia Comput Sci, 1, 1799-1807, (2010)
[12] Fabregat-Traver D, Bientinesi P (2011) Automatic generation of loop-invariants for matrix operations. In: Proceedings of the 11th international conference on computational science and its applications (to appear). Also TR AICES-2010/02-1, AICES, RWTH Aachen · Zbl 1344.68298
[13] Fabregat-Traver D, Bientinesi P (2011) Knowledge-based automatic generation of partitioned matrix expressions. In: Proceedings of the 13th international workshop on computer algebra in scientific computing (to appear). Also TR AICES-2010/01-3, AICES, RWTH Aachen · Zbl 1344.68298
[14] Gunnels, JA; Gustavson, FG; Henry, GM; Geijn, RA, FLAME: formal linear algebra methods environment, ACM Trans Math Softw, 27, 422-455, (2001) · Zbl 1070.65522
[15] Gries D (1981) The science of programming. Springer, New York · Zbl 0472.68003
[16] Gunnels JA (2001) A systematic approach to the design and analysis of parallel dense linear algebra algorithms. PhD thesis, Department of Computer Sciences, The University of Texas · Zbl 0639.65016
[17] Gunnels, JA; Geijn, RA; Boisvert, RF (ed.); Tang, PTP (ed.), Formal methods for high-performance linear algebra libraries, 193-210, (2001), Dordrecht
[18] Goto, K; Geijn, R, High-performance implementation of the level-3 BLAS, ACM Trans Math Softw, 35, 1-14, (2008)
[19] Goto, K; Geijn, RA, Anatomy of high-performance matrix multiplication, ACM Trans Math Softw, 34, 1-25, (2008) · Zbl 1190.65064
[20] Hoare, CAR, An axiomatic basis for computer programming, Commun ACM, 12, 576-580, (1969) · Zbl 0179.23105
[21] Khalil HK (2002) Nonlinear systems, 3rd edn. Prentice-Hall, Upper Saddle River NY
[22] Lawson, CL; Hanson, RJ; Kincaid, DR; Krogh, FT, Basic linear algebra subprograms for Fortran usage, ACM Trans Math Softw, 5, 308-323, (1979) · Zbl 0412.65022
[23] Moler C, Little J, Bangert S (1987) Pro-Matlab, user’s guide. The Mathworks, Inc.
[24] Poulson J, van de Geijn R, Bennighof J (2011) Parallel algorithms for reducing the generalized Hermitian-definite eigenvalue problem. FLAME Working Note #56. The University of Texas at Austin, Department of Computer Science. Technical Report TR-11-05 · Zbl 1190.65064
[25] Quintana-Ortí, ES; Geijn, RA, Formal derivation of algorithms: the triangular Sylvester equation, ACM Trans Math Softw, 29, 218-243, (2003) · Zbl 1072.65064
[26] van de Geijn RA, Quintana-Ortí ES (2008) The science of programming matrix computations. http://www.lulu.com/content/1911788 · Zbl 1190.65064
[27] Van Zee, FG; Chan, E; Geijn, R; Quintana-Ortí, ES; Quintana-Ortí, G, Introducing: the libflame library for dense matrix computations, IEEE Comput Sci Eng, 11, 56-62, (2009)
[28] Van Zee FG (2009) \(\texttt{libflame}\) : the complete reference. www.lulu.com
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.