Parallel programming in high-performance computing depends on low-level APIs such as MPI, requiring users to manage synchronization and resources manually. Several correctness checking tools exist to help bug-free code development, though most target a single programming model, limiting their applicability. Our previous work, the static analysis tool CoVer, leverages a contract-based approach enabling users to specify custom error-checking rules and support emerging or unconventional programming models without requiring extensive new tooling. However, static analysis cannot fully reason about runtime-dependent behavior such as pointer aliasing or indirect control flow. To address this, we present CoVer-Dynamic, a dynamic analysis extension that reuses CoVer's contract language to provide a unified static-dynamic verification framework. By enforcing the same contracts at runtime, CoVer-Dynamic improves classification accuracy and eliminates false positives on standardized MPI and OpenSHMEM benchmarks, while detecting errors beyond static analysis only. Our evaluation shows that CoVer-Dynamic consistently outperforms the state-of-the-art correctness checker MUST, averaging a 2x speedup. Finally, our results show limitations in the expressiveness of the contract language, motivating future work to support more error classes.

翻译：高性能计算中的并行编程依赖于诸如MPI等底层API，这要求用户手动管理同步与资源。尽管已有多种正确性检查工具可辅助开发无缺陷代码，但多数工具仅针对单一编程模型，限制了其适用性。我们先前开发的静态分析工具CoVer采用基于契约的方法，使用户能够指定自定义错误检查规则，并支持新兴或非常规编程模型，而无需大量新工具开发。然而，静态分析无法完全推理依赖于运行时的行为，如指针别名或间接控制流。为此，我们提出CoVer-Dynamic，这是一种动态分析扩展，它复用CoVer的契约语言以提供统一的静态-动态验证框架。通过在运行时强制执行相同契约，CoVer-Dynamic在标准化MPI和OpenSHMEM基准测试中提高了分类精度并消除了误报，同时检测到仅靠静态分析无法发现的错误。我们的评估表明，CoVer-Dynamic在性能上持续优于当前最先进的正确性检查器MUST，平均实现2倍加速。最后，我们的结果揭示了契约语言在表达能力方面的局限性，这为未来支持更多错误类别的研究提供了方向。