Collaborative Research: A Systematic Approach to the Derivation, Representation, Analysis, and Correctness of Dense and Banded Linear Algebra Algorithms for HPC Architectures

尽管人们普遍认为稠密线性代数库的研究已经枯竭，但历史表明，随着用于科学应用的高性能计算机出现新的体系结构特征，重新研究广泛使用的稠密线性代数软件包的必要性重新浮出水面。当向量超级计算机在20世纪70年代首次出现，基于微处理器的工作站在80年代出现，分布式存储器并行体系结构在90年代出现时，情况就是如此。现在，随着多级存储器在顺序和并行体系结构中的出现，再次需要重新设计，因为当前一代密集线性代数程序包所获得的性能与针对个别操作的最佳算法优化的性能不匹配。一个密切相关的问题是，现有的库并不总是具有科学计算社区所需的功能和性能。从以前的库开发新的稠密线性代数库的传统方法的基本问题是，它本质上是进化的。人们非常重视最大限度的代码重用，因为人们相信，新的库继承了先前库的“正确性”(主要是通过详尽的测试建立的)，从而减少了生产新库所需的努力。不幸的是，进化方法过去失败了，未来注定也会失败，这是有可识别的原因的。这个提议的项目背后的基本前提是，如果要避免重复的努力投资，必须开发一种革命性的方法。最近的研究发现了一种系统的方法，通过应用计算机科学的经典推导技术来推导出被证明是正确的稠密线性代数算法。现在可能触手可及的实用解决方案包括(部分)自动开发(派生、实现以及成本和稳定性分析)高性能密集和带状线性代数库。这与实现这类库的传统方法不同，因为它们的复杂性，开发、调试和维护是乏味且容易出错的过程。拟议的工作承诺通过系统地和直接地将系统派生的、可证明正确的算法翻译成命令式编程语言来交付几乎不需要维护的库。拟议的工作将通过集中开发上述系统方法而不冒险进入自动化，从而为这种自动化系统奠定基础。此外，还将开发使用最新软件工程技术编写的原型库，以展示这些方法的潜力。特别是，通过使用模板元编程和表达式模板等C++技术来克服驱动系统方法的抽象的明显成本的能力将是研究的中心。成功将由系统化方法实现自动化的程度来衡量，由将使用该方法发现的新算法来衡量，并由所产生的原型库(在顺序和并行体系结构上)所展示的性能来衡量。其他项目目前使用的自动化方法在性能和灵活性方面与拟议的库相比并不具有竞争力。

Despite the general belief that research in dense linear algebra libraries has been exhausted, history shows that as new architectural features appear in high-performance computers used for scientific applications, the need for the renewed investigation of widely used dense linear algebra packages resurfaces. This has been the case when vector supercomputers first appeared in the 1970s, when microprocessor based workstations appeared in the 1980s, and when distributed memory parallel architectures appeared in the 1990s. Now, with the emergence of multi-level memories in both sequential and parallel architectures, a redesign is once again warranted, as the performance attained by the current generation of dense linear algebra packages does not match that of the best optimizations of algorithms for individual operations. A closely related concern is that the existing libraries do not always have the functionality nor the performance required by the scientific computing community.The fundamental problem with the traditional approach to developing a new dense linear algebra library from a previous library is that it has been inherently evolutionary. There has been a heavy emphasis on maximal code-reuse in the belief that the ``correctness'' (established largely through exhaustive testing) of the previous library is then inherited by the new library, thus reducing the effort required to produce that new library. Unfortunately, there are identifiable reasons why the evolutionary approach has failed in the past and is doomed to failure in the future. The fundamental premise behind this proposed project is that a revolutionary approach must be developed if the repeated investment of effort is to be avoided.Recent research has uncovered a systematic approach to the derivation of provably correct dense linear algebra algorithms via the application of classic derivation techniques from computer science. The practical solutions that may now be within reach include the (partially) automatic development (derivation, implementation, and cost and stability analysis) of high-performance dense and banded linear algebra libraries. This is in contrast to the traditionalapproaches for implementation of such libraries for which the development, debugging, and maintenance are tedious and error-prone processes because of their complexity. The proposed work promises to deliver libraries that require little or no maintenance through the systematic and direct translation of systematically derived, provably correct algorithms to an imperative programming language.The proposed work will lay the foundation for such automated systems by concentrating on developing the systematic approaches mentioned above, without yet venturing into automation. In addition, prototype libraries, coded using the latest software engineering techniques, will be developed to demonstrate the potential of the approaches. In particular, the ability to overcome the apparent cost of the abstractions that drive the systematic approaches by using C++ techniques like template meta-programming and expression templates will be central to the study. Success will be measured by the degree to which the systematic approaches will enable automation, by the new algorithms that will be uncovered using the methodology, and by theperformance that can be demonstrated (on sequential and parallel architectures) by the resulting prototype libraries. Automated methods currently used by other projects are not deemed to be competitive, in terms of performance and flexibility, with the proposed libraries.