Verifying MPI API Usage Requirements with Contracts

doi:10.1007/978-3-032-07194-1_4

Verifying MPI API Usage Requirements with Contracts

2026-01-01

1

PRE

AI

Y

Yussur Mustafa Oraji *

DOI：10.1007/978-3-032-07194-1_4

原文链接

原文求助

摘要

En 中文

并行编程模型，如MPI和OpenSHMEM，使大规模分布式内存计算机在HPC中的应用成为可能。然而，程序员常常忽略其API的细微规则，例如正确同步本地内存访问与通信以及释放获取的资源。现有的正确性工具旨在自动检测这些问题，但通常是模型特定的。我们提出使用模型无关的函数注解来避免这种依赖：契约允许在函数声明中指定通用的前置和后置条件。我们规定了必须在每个调用点满足的要求，以避免常见的MPI错误，如资源泄漏和本地数据竞争。与传统检查器相比，契约的透明性还允许最终用户维护和扩展检查，以及将其特定分析适应其用例。本文介绍了一种契约语言和CoVer，一个可扩展的静态验证器，用于检查基于库的并行编程模型的使用。它使用LLVM框架进行数据流分析，以验证这些契约注解。我们将检测准确性与静态工具PARCOACH和MPI-Checker在RMARaceBench和MPI-BugBench上的表现进行比较，并基于LULESH、miniVite和PRK Stencil Kernel等小型应用评估编译时开销。CoVer通过覆盖各种问题提高了检测准确率，同时保持了相当的开销。

Keyword:

MPI

Correctness

HPC

Parallel

Tools

Verifying MPI API Usage Requirements with Contracts

摘要

期刊

机构

引用论文