2025-11-10T02:34:56.080990

Verification Challenges in Sparse Matrix Vector Multiplication in High Performance Computing: Part I

Zhang
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.
academic

Verification Challenges in Sparse Matrix Vector Multiplication in High Performance Computing: Part I

基本信息

  • 论文ID: 2510.13427
  • 标题: Verification Challenges in Sparse Matrix Vector Multiplication in High Performance Computing: Part I
  • 作者: Junchao Zhang (Argonne National Laboratory)
  • 分类: 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

摘要

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.

研究背景与动机

问题定义

该研究针对高性能计算中稀疏矩阵向量乘法(SpMV)的软件验证挑战。SpMV是求解稀疏线性方程组Ax=b的核心运算，广泛应用于基于迭代求解器的科学计算代码中，特别是在大规模Krylov子空间方法中。

重要性

  1. 基础性: SpMV是科学计算的基础核心算法，其正确性直接影响上层应用的可靠性
  2. 复杂性: 虽然数学定义简单(yi = Σ(aij·xj))，但存储格式、数据分布、并行化和优化使实现变得复杂
  3. 验证挑战: 现有的复杂优化实现给软件验证带来了重大挑战

现有方法局限性

  • PETSc库中存在高度优化的MPI并行SpMV实现，但其复杂性使得验证困难
  • 缺乏专门为软件验证社区设计的标准化挑战问题

研究动机

为科学软件验证社区提供一个结构化的挑战问题，通过提供从简单到复杂的SpMV实现，帮助验证工具和方法的开发与评估。

核心贡献

  1. 提供了标准化的验证挑战问题: 为科学软件验证社区设计了SpMV的标准测试用例
  2. 实现了两种不同复杂度的SpMV算法:
    • 顺序实现(seq.c)
    • 基础MPI并行实现(mpibasic.c)
  3. 建立了完整的验证框架: 包括输入数据生成、正确性检查和错误检测机制
  4. 明确定义了验证目标: 为每种实现提供了具体的验证要求和挑战

方法详解

任务定义

输入:

  • 稀疏矩阵A (M×N，NNZ个非零元素)，采用CSR格式存储
  • 向量x (N维)
  • 期望结果z = Ax (M维)

输出:

  • 计算结果y = Ax
  • 正确性验证: ||y-z||²应为0(忽略浮点舍入误差)

约束条件:

  • 使用压缩稀疏行(CSR)格式
  • 支持MPI并行分布式计算

数据结构设计

CSR格式表示

稀疏矩阵A采用三个数组表示:

  • 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]];
}

MPI并行实现

  1. 数据分布策略:
    • 矩阵按行块分布: m = M/size + (M%size > rank ? 1 : 0)
    • 向量x按列布局分布: n = N/size + (N%size > rank ? 1 : 0)
  2. 通信模式:
    • 使用MPI_Allgather或MPI_Allgatherv收集完整的向量x
    • 使用MPI_Allreduce计算全局范数
  3. 计算流程:
    • 计算局部矩阵布局(rstart, cstart)
    • 从全局数组提取局部数据
    • 收集分布式向量x到局部完整副本X
    • 执行局部SpMV计算
    • 计算局部误差范数并全局归约

技术创新点

  1. 渐进式复杂度设计: 从简单顺序实现到基础并行实现，便于验证工具的渐进式测试
  2. 标准化验证接口: 提供统一的输入输出格式和正确性检查机制
  3. 实际应用背景: 基于PETSc库的真实实现模式，具有实际意义
  4. 可扩展框架: 为未来更复杂的优化版本(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

MPI并行实现验证要求

  1. 布局正确性: 验证Σm = M, Σn = N
  2. 局部计算正确性: 验证每个进程上的y是对应局部子矩阵与完整向量x的正确乘积结果

测试用例

论文提供了具体的测试数据:

  • 输入矩阵: 32×36稀疏矩阵(50个非零元素)
  • 输入向量: 36维向量
  • 期望输出: 32维结果向量
  • 所有数据以整数和浮点数组形式提供

相关工作

相关研究领域

  1. Krylov子空间方法: SpMV是迭代求解器的核心组件
  2. PETSc库: 提供了丰富的Krylov方法和SpMV实现套件
  3. 科学软件验证: 针对高性能科学计算软件的正确性验证

本文定位

  • 填补了科学软件验证社区缺乏标准化SpMV验证挑战的空白
  • 为复杂优化实现的验证提供了基础参考
  • 连接了理论验证方法与实际HPC应用需求

结论与讨论

主要结论

  1. 成功建立了SpMV软件验证的标准化挑战问题
  2. 提供了两种不同复杂度的实现，适合渐进式验证工具测试
  3. 基于真实PETSc库模式，具有实际应用价值

局限性

  1. 规模限制: 当前测试用例规模较小(32×36矩阵)
  2. 优化缺失: 基础MPI实现未包含实际生产环境中的复杂优化
  3. 验证范围: 仅覆盖基础正确性，未涉及性能和数值稳定性验证

未来方向

  1. Part II开发: 计划在后续工作中提供更复杂的优化MPI实现
  2. 扩展测试用例: 增加更大规模和不同稀疏模式的测试矩阵
  3. 验证工具集成: 与现有验证工具进行集成测试

深度评价

优点

  1. 实用价值高: 解决了科学软件验证社区的实际需求
  2. 设计合理: 渐进式复杂度设计便于验证工具开发和测试
  3. 标准化程度高: 提供了完整的输入输出规范和正确性检查机制
  4. 可复现性强: 代码公开可获取，测试数据内嵌，易于复现
  5. 实际背景: 基于广泛使用的PETSc库，具有真实应用意义

不足

  1. 理论分析缺乏: 未提供算法复杂度分析或理论性质讨论
  2. 测试覆盖有限: 仅提供单一测试用例，多样性不足
  3. 验证深度: 主要关注功能正确性，缺乏数值精度和边界条件分析
  4. 性能考虑: 未涉及性能验证相关的挑战

影响力

  1. 领域贡献: 为科学软件验证提供了重要的标准化测试平台
  2. 实用价值: 可直接用于验证工具的开发和评估
  3. 可扩展性: 为后续更复杂实现奠定了基础框架
  4. 社区价值: 促进了HPC和软件验证社区的交流合作

适用场景

  1. 验证工具开发: 作为标准测试用例验证工具有效性
  2. 教学应用: 适合作为并行计算和软件验证的教学案例
  3. 基准测试: 可作为SpMV实现正确性的参考基准
  4. 研究平台: 为相关算法和优化研究提供标准化平台

参考文献

  1. S Balay et al. (2025): PETSc/TAO Users Manual. Technical Report ANL-21/39 - Revision 3.23, Argonne National Laboratory
  2. Yousef Saad (2003): Iterative Methods for Sparse Linear Systems, second edition. Society for Industrial and Applied Mathematics

总体评价: 这是一篇实用性很强的工作论文，虽然在理论创新方面贡献有限，但为科学软件验证社区提供了急需的标准化挑战问题。论文结构清晰，实现完整，具有良好的可复现性和扩展性，对推动HPC软件验证领域的发展具有重要价值。