Scholarlink

<p>Parallel architectures-from GPUs to heterogeneous clusters-promise significant performance gains, but every attempt to use their resources runs into two traditionally disjointed problems: how to achieve a&#xa0;noticeable speedup and at the same time guarantee the correctness of code transformations. Empirical tuning strategies can no longer cope with the growing complexity of computational graphs, and manual proof of equivalence of program versions becomes almost impossible. We propose a&#xa0;holistic algebraic approach that transforms these multidirectional problems into a&#xa0;single formal model. As a&#xa0;basis, we use a&#xa0;polynomial representation of dependencies and data flows extended by tensor constructions, which allows us to describe both classical linear algebra cycles and irregular patterns of graph computing in the same way. At this level, program invariants are calculated through the construction of Grobnerbases, and the complexity of calculations is obtained by differentiating by resource variables, which forms closed analytical estimates of time and energy consumption. The algebraic nature of the model makes further transformations deterministic: any permutations of iterations, convolutions of loops, and distribution of computations over devices are translated into equivalent operations on ideals; the correctness of transformations is automatically deduced as a&#xa0;consequence of equality of ideals up to isomorphism. For a&#xa0;number of typical HPC tasks, including multiplication of large sparse matrices and graph streaming, it is possible to achieve up to 50% speedup compared to manually optimized code, and the proof of functional equivalence of both versions is generated by the machine without the developer’s participation. Experience shows that the algebraic model is easily integrated into existing compilation chains and reduces the barrier between theoretical research and industrial practice. The proposed approach demonstrates that computer algebra can become not an auxiliary, but a&#xa0;central tool for developing parallel software, it combines automatic generation of performance models, rigorous proof-of-correctness, and high-performance code synthesis into a&#xa0;continuous pipeline that is accessible to the researcher without deep immersion in hardware details.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Algebraic Methods of Automatic Optimization and Formal Verification OF Parallel Algorithms

  • 期刊论文

  • 发表日期：

    2025年4月1日

查看全文
  • A. M. Tramova,
  • A. A. Popov,
  • V. S. Artemyev,
  • N. V. Mokrova

摘要

Parallel architectures-from GPUs to heterogeneous clusters-promise significant performance gains, but every attempt to use their resources runs into two traditionally disjointed problems: how to achieve a noticeable speedup and at the same time guarantee the correctness of code transformations. Empirical tuning strategies can no longer cope with the growing complexity of computational graphs, and manual proof of equivalence of program versions becomes almost impossible. We propose a holistic algebraic approach that transforms these multidirectional problems into a single formal model. As a basis, we use a polynomial representation of dependencies and data flows extended by tensor constructions, which allows us to describe both classical linear algebra cycles and irregular patterns of graph computing in the same way. At this level, program invariants are calculated through the construction of Grobnerbases, and the complexity of calculations is obtained by differentiating by resource variables, which forms closed analytical estimates of time and energy consumption. The algebraic nature of the model makes further transformations deterministic: any permutations of iterations, convolutions of loops, and distribution of computations over devices are translated into equivalent operations on ideals; the correctness of transformations is automatically deduced as a consequence of equality of ideals up to isomorphism. For a number of typical HPC tasks, including multiplication of large sparse matrices and graph streaming, it is possible to achieve up to 50% speedup compared to manually optimized code, and the proof of functional equivalence of both versions is generated by the machine without the developer’s participation. Experience shows that the algebraic model is easily integrated into existing compilation chains and reduces the barrier between theoretical research and industrial practice. The proposed approach demonstrates that computer algebra can become not an auxiliary, but a central tool for developing parallel software, it combines automatic generation of performance models, rigorous proof-of-correctness, and high-performance code synthesis into a continuous pipeline that is accessible to the researcher without deep immersion in hardware details.