Dynamic Contract Analysis for Parallel Programming Models

TL;DR

This paper introduces CoVer-Dynamic, a dynamic analysis extension for contract-based correctness checking in parallel programming, improving accuracy and performance over static tools and handling runtime-dependent errors.

Contribution

It presents a unified static-dynamic verification framework that enhances correctness checking for parallel programming models using a contract-based approach.

Findings

CoVer-Dynamic improves classification accuracy and reduces false positives.

It achieves a 2x speedup over the state-of-the-art checker MUST.

The approach detects errors beyond static analysis capabilities.

Abstract

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.