Sparse matrix vector multiplication (SpMV) is a fundamental kernel in scientific codes that rely on iterative solvers. In this first part of our work, we present both a sequential and a basic MPI parallel implementations of SpMV, aiming to provide a challenge problem for the scientific software verification community. The implementations are described in the context of the PETSc library.
論文ID : 2510.13427タイトル : Verification Challenges in Sparse Matrix Vector Multiplication in High Performance Computing: Part I著者 : Junchao Zhang (アルゴンヌ国立研究所)分類 : cs.LO cs.DC cs.MS発表会議 : International Workshop on Verification of Scientific Software (VSS 2025)出版情報 : EPTCS 432, 2025, pp. 98–105論文リンク : https://arxiv.org/abs/2510.13427 疎行列ベクトル乗算(SpMV)は、反復求解器に依存する科学計算コードの基本的なカーネルである。本論文の第1部では、SpMVの順序実装と基本的なMPI並列実装の両方を提示し、科学ソフトウェア検証コミュニティに対する課題問題の提供を目指している。これらの実装はPETScライブラリの文脈で説明されている。
本研究は、高性能計算(HPC)における疎行列ベクトル乗算(SpMV)のソフトウェア検証課題に対処している。SpMVは疎線形方程式系Ax=bを解くための中核演算であり、特に大規模Krylov部分空間法に基づく反復求解器を用いた科学計算コードで広く応用されている。
基礎性 : SpMVは科学計算の基本的なコア・アルゴリズムであり、その正確性は上位層のアプリケーションの信頼性に直接影響する複雑性 : 数学的定義は単純(yi = Σ(aij·xj))であるが、ストレージ形式、データ分布、並列化、最適化により実装が複雑になる検証課題 : 既存の複雑に最適化された実装は、ソフトウェア検証に重大な課題をもたらすPETScライブラリに存在する高度に最適化されたMPI並列SpMV実装は、その複雑性により検証が困難である 科学ソフトウェア検証コミュニティ向けに特別に設計された標準化された課題問題が不足している 科学ソフトウェア検証コミュニティに対して、単純から複雑へと段階的なSpMV実装を提供することで、検証ツールと手法の開発と評価を支援する構造化された課題問題を提供すること。
標準化された検証課題問題の提供 : 科学ソフトウェア検証コミュニティ向けにSpMVの標準的なテストケースを設計異なる複雑度の2つのSpMVアルゴリズムの実装 :
順序実装(seq.c) 基本的なMPI並列実装(mpibasic.c) 完全な検証フレームワークの確立 : 入力データ生成、正確性チェック、エラー検出メカニズムを含む検証目標の明確な定義 : 各実装に対する具体的な検証要件と課題を提供入力 :
疎行列A (M×N、NNZ個の非ゼロ要素)、CSR形式で保存 ベクトルx (N次元) 期待される結果z = Ax (M次元) 出力 :
計算結果y = Ax 正確性検証: ||y-z||²は0であるべき(浮動小数点丸め誤差を除く) 制約条件 :
圧縮疎行形式(CSR)を使用 MPI並列分散計算をサポート 疎行列Aは3つの配列で表現される:
a[nnz]: 非ゼロ要素値を保存j[nnz]: 非ゼロ要素の列インデックスを保存i[m+1]: 行ポインタ、ik は第k行のa とj における開始位置を指す// 順序版
typedef struct {
int m, n; // 行列次元
int *i, *j; // CSR形式インデックス
double *a; // 非ゼロ要素値
} Mat;
// MPI並列版
typedef struct {
int m, n, M, N; // ローカルおよびグローバル次元
int rstart, cstart; // 開始行列インデックス
int *i, *j;
double *a;
} Mat;
for (i = 0; i < A.m; i++) {
y.a[i] = 0.0;
for (j = A.i[i]; j < A.i[i + 1]; j++)
y.a[i] += A.a[j] * x.a[A.j[j]];
}
データ分布戦略 :行ブロック分布による行列: m = M/size + (M%size > rank ? 1 : 0) 列レイアウト分布によるベクトルx: n = N/size + (N%size > rank ? 1 : 0) 通信パターン :MPI_AllgatherまたはMPI_Allgathervを使用して完全なベクトルxを収集MPI_Allreduceを使用してグローバル範数を計算計算フロー :ローカル行列レイアウト(rstart, cstart)を計算 グローバル配列からローカルデータを抽出 分散ベクトルxをローカル完全コピーXに収集 ローカルSpMV計算を実行 ローカル誤差範数を計算しグローバル削減 段階的複雑度設計 : 単純な順序実装から基本的な並列実装へと進み、検証ツールの段階的テストを可能にする標準化された検証インターフェース : 統一された入力出力形式と正確性チェックメカニズムを提供実際のアプリケーション背景 : PETScライブラリの実装パターンに基づき、実用的な意義を持つ拡張可能なフレームワーク : より複雑な最適化版(Part II)の基礎を構築行列規模 : 32×36行列、50個の非ゼロ要素を含むデータ生成 : 付属のPythonスクリプトcsr.pyを使用してテストデータを生成ハードコード入力 : 使用を簡略化するため、テストデータはソースコードに直接埋め込まれているカスタマイズ可能性 : ユーザーはPythonスクリプトパラメータを修正して異なるテストケースを生成可能正確性検証 : ||y-z||²の二乗範数を計算成功基準 : 範数 ≤ 1e-6 (浮動小数点丸め誤差を考慮)リターンコード : 正確な場合は0、エラーの場合は非ゼロ値を返すプログラミング言語 : C言語並列フレームワーク : MPIコンパイル要件 : CコンパイラまたはMPIコンパイラのみが必要コード可用性 : GitHubリポジトリで公開発布計算結果yが以下を満たすことを検証: yi = Σ(aij·xj)、ここでCSR表現に保存されていないaijは0と見なされる
レイアウト正確性 : Σm = M, Σn = Nを検証ローカル計算正確性 : 各プロセス上のyが対応するローカル部分行列と完全ベクトルxの正確な乗算結果であることを検証論文は具体的なテストデータを提供している:
入力行列: 32×36疎行列(50個の非ゼロ要素) 入力ベクトル: 36次元ベクトル 期待される出力: 32次元結果ベクトル すべてのデータは整数および浮動小数点配列形式で提供される Krylov部分空間法 : SpMVは反復求解器の中核成分PETScライブラリ : 豊富なKrylov法とSpMV実装スイートを提供科学ソフトウェア検証 : 高性能科学計算ソフトウェアの正確性検証に対処科学ソフトウェア検証コミュニティにおけるSpMV検証課題の標準化の欠落を埋める 複雑に最適化された実装の検証に対する基本的な参照を提供 理論的検証手法と実際のHPCアプリケーション要件を結びつける SpMVソフトウェア検証の標準化された課題問題の確立に成功 段階的な検証ツールテストに適した異なる複雑度の2つの実装を提供 実際のPETScライブラリパターンに基づき、実用的な応用価値を持つ 規模制限 : 現在のテストケースは規模が小さい(32×36行列)最適化の欠落 : 基本的なMPI実装は実際の本番環境における複雑な最適化を含まない検証範囲 : 基本的な正確性のみをカバーし、性能と数値安定性検証には対応していないPart II開発 : 後続の研究でより複雑に最適化されたMPI実装を提供する予定テストケースの拡張 : より大規模で異なる疎パターンを持つテスト行列を追加検証ツール統合 : 既存の検証ツールとの統合テスト実用価値が高い : 科学ソフトウェア検証コミュニティの実際のニーズに対応設計が合理的 : 段階的複雑度設計により検証ツール開発とテストが容易標準化程度が高い : 完全な入出力仕様と正確性チェックメカニズムを提供再現性が強い : コードは公開で入手可能、テストデータは内蔵され、再現が容易実際の背景 : 広く使用されているPETScライブラリに基づき、実用的な応用意義を持つ理論分析の欠落 : アルゴリズム複雑度分析または理論的性質の議論がないテストカバレッジの限定 : 単一のテストケースのみを提供し、多様性が不足検証の深さ : 主に機能的正確性に焦点を当て、数値精度と境界条件分析が不足性能考慮 : 性能検証関連の課題には対応していない分野への貢献 : 科学ソフトウェア検証に重要な標準化テストプラットフォームを提供実用価値 : 検証ツール開発と評価に直接使用可能拡張性 : より複雑な実装の基礎フレームワークを構築コミュニティ価値 : HPCとソフトウェア検証コミュニティ間の交流と協力を促進検証ツール開発 : ツール有効性を検証するための標準テストケース教育応用 : 並列計算とソフトウェア検証の教育事例として適切ベンチマークテスト : SpMV実装正確性の参照基準として機能研究プラットフォーム : 関連アルゴリズムと最適化研究の標準化プラットフォームを提供S Balay et al. (2025): PETSc/TAO Users Manual. Technical Report ANL-21/39 - Revision 3.23, アルゴンヌ国立研究所 Yousef Saad (2003): Iterative Methods for Sparse Linear Systems, second edition. Society for Industrial and Applied Mathematics 総合評価 : これは実用性が非常に高い実務的論文であり、理論的革新の貢献は限定的であるが、科学ソフトウェア検証コミュニティが必要とする標準化された課題問題を提供している。論文構成は明確で実装は完全であり、優れた再現性と拡張性を備えており、HPC ソフトウェア検証分野の発展を推進する上で重要な価値を持つ。