The science of deriving dense linear algebra algorithms

ABSTRACT

In this article we present a systematic approach to the derivation of families of high-performance algorithms for a large set of frequently encountered dense linear algebra operations. As part of the derivation a constructive proof of the correctness of the algorithm is generated. The article is structured so that it can be used as a tutorial for novices. However, the method has been shown to yield new high-performance algorithms for well-studied linear algebra operations and should also be of interest to those who wish to produce best-in-class high-performance codes.

REFERENCES

• 1: Philip Alpatov , Greg Baker , Carter Edwards , John Gunnels , Greg Morrow , James Overfelt , Robert van de Geijn , Yuan-Jye J. Wu, PLAPACK: parallel linear algebra package design overview, Proceedings of the 1997 ACM/IEEE conference on Supercomputing (CDROM), p.1-16, November 15-21, 1997, San Jose, CA [doi>10.1145/509593.509622]
• 2: Bientinesi, P., Gunnels, J. A., Gustavson, F. G., Henry, G. M., Myers, M. E., Quintana-Orti, E. S., and van de Geijn, R. A. 2002. The science of programming high-performance linear algebra libraries. In Proceedings of Performance Optimization for High-Level Languages and Libraries (POHLL-02). To appear.
• 3: Bientinesi, P. and van de Geijn, R. A. 2002. Developing linear algebra algorithms: Class projects Spring 2002. Tech. Rep. CS-TR-02, Department of Computer Sciences, The University of Texas at Austin. June. http://www.cs.utexas.edu/users/flame/pubs/.
• 4: Dijkstra, E. W. 1968. A constructive approach to the problem of program correctness. BIT 8, 174--186.
• 5: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 6: J. J. Dongarra , Jeremy Du Croz , Sven Hammarling , I. S. Duff, A set of level 3 basic linear algebra subprograms, ACM Transactions on Mathematical Software (TOMS), v.16 n.1, p.1-17, March 1990 [doi>10.1145/77626.79170]
• 7: Jack J. Dongarra , Jeremy Du Croz , Sven Hammarling , Richard J. Hanson, An extended set of FORTRAN basic linear algebra subprograms, ACM Transactions on Mathematical Software (TOMS), v.14 n.1, p.1-17, March 1988 [doi>10.1145/42288.42291]
• 8: Michael Dean Ernst , David Notkin, Dynamically discovering likely program invariants, 2000
• 9: Michael D. Ernst , Adam Czeisler , William G. Griswold , David Notkin, Quickly detecting relevant program invariants, Proceedings of the 22nd international conference on Software engineering, p.449-458, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337240]
• 10: Floyd, R. W. 1967. Assigning meanings to programs. In Symposium on Applied Mathematics, J. T. Schwartz, Ed. Vol. 19. American Mathematical Society, 19--32.
• 11: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 12: David Gries , Fred B. Schneider, A logical approach to discrete math, Springer-Verlag New York, Inc., New York, NY, 1993
• 13: John Andrew Gunnels , Robert A. Geijn, A systematic approach to the design and analysis of linear algebra algorithms, 2001
• 14: John A. Gunnels , Fred G. Gustavson , Greg M. Henry , Robert A. van de Geijn, FLAME: Formal Linear Algebra Methods Environment, ACM Transactions on Mathematical Software (TOMS), v.27 n.4, p.422-455, December 2001 [doi>10.1145/504210.504213]
• 15: John A. Gunnels , Greg M. Henry , Robert A. van de Geijn, A Family of High-Performance Matrix Multiplication Algorithms, Proceedings of the International Conference on Computational Sciences-Part I, p.51-60, May 28-30, 2001
• 16: John A. Gunnels , Robert A. van de Geijn, Developing Linear Algebra Algorithms: A Collection of Class Projects, University of Texas at Austin, Austin, TX, 2001
• 17: John A. Gunnels , Robert A. van de Geijn, Formal Methods for High-Performance Linear Algebra Libraries, Proceedings of the IFIP TC2/WG2.5 Working Conference on the Architecture of Scientific Software, p.193-210, October 02-04, 2000
• 18: Nicholas J. Higham, Accuracy and Stability of Numerical Algorithms, Society for Industrial and Applied Mathematics, Philadelphia, PA, 2002
• 19: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 20: Matt Kaufmann , J. S. Moore, An Industrial Strength Theorem Prover for a Logic Based on Common Lisp, IEEE Transactions on Software Engineering, v.23 n.4, p.203-213, April 1997 [doi>10.1109/32.588534]
• 21: Kaufmann, M., Manolios, P., and Moore, J. S., Eds. 2000. Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers.
• 22: C. L. Lawson , R. J. Hanson , D. R. Kincaid , F. T. Krogh, Basic Linear Algebra Subprograms for Fortran Usage, ACM Transactions on Mathematical Software (TOMS), v.5 n.3, p.308-323, Sept. 1979 [doi>10.1145/355841.355847]
• 23: Misra, J. 1976. Some aspects of the verification of loop computations. IEEE Trans. Soft. Eng. SE-4, 6 (Nov.).
• 24: Moler, C., Little, J., and Bangert, S. 1987. Pro-Matlab, User's Guide. The Mathworks, Inc.
• 25: Enrique S. Quintana , Gregorio Quintana , Xiaobai Sun , Robert vande Geijn, A Note On Parallel Matrix Inversion, SIAM Journal on Scientific Computing, v.22 n.5, p.1762-1771, 2000 [doi>10.1137/S1064827598345679]
• 26: Enrique S. Quintana-Ortí , Robert A. van de Geijn, Formal derivation of algorithms: The triangular sylvester equation, ACM Transactions on Mathematical Software (TOMS), v.29 n.2, p.218-243, June 2003 [doi>10.1145/779359.779365]
• 27: Robert A. van de Geijn , Philip Alpatou , Greg Baker , Carter Edwards , John Gunnels , Greg Morrow , James Overfelt, Using PLAPACK: parallel linear algebra package, MIT Press, Cambridge, MA, 1997
• 28: R. Clint Whaley , Jack J. Dongarra, Automatically tuned linear algebra software, Proceedings of the 1998 ACM/IEEE conference on Supercomputing (CDROM), p.1-27, November 07-13, 1998, San Jose, CA
• 29: Stephen Wolfram, The Mathematica book (3rd ed.), Cambridge University Press, New York, NY, 1996

INDEX TERMS

Primary Classification:
  G. Mathematics of Computing
  G.4 MATHEMATICAL SOFTWARE
      Subjects: Algorithm design and analysis

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.11 Software Architectures
            Subjects: Domain-specific architectures
      D.2.2 Design Tools and Techniques
          Subjects: Software libraries

  G. Mathematics of Computing
  G.4 MATHEMATICAL SOFTWARE
      Subjects: User interfaces; Efficiency

General Terms:
Algorithms, Design, Performance, Theory

Keywords:
Formal derivation, high-performance computing, libraries, linear algebra