Search papers, labs, and topics across Lattice.
CoVer-Dynamic extends the CoVer static analysis tool with dynamic analysis capabilities, enabling a unified contract-based framework for verifying parallel programs. By enforcing user-defined contracts at runtime, the tool improves bug detection accuracy and reduces false positives compared to static analysis alone. Experiments on MPI and OpenSHMEM benchmarks demonstrate that CoVer-Dynamic outperforms the state-of-the-art MUST checker by 2x in speed, while also identifying errors undetectable by static analysis.
Achieve 2x speedup over state-of-the-art MPI correctness checker MUST by unifying static and dynamic contract analysis, while also catching bugs missed by static methods alone.
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.
