Allocation Tracking and Parameter Checking for Parallel Programming Models using Contracts
TL;DR
An extension to the CoVer contract language designed to capture and check a broader range of error classes and introduce generic parameter checking and allocation tracking, while keeping generality across both programming model and language is presented.
Abstract
Correctness checking tools for High-Performance Computing programs are typically limited to specific parallel programming models such as MPI or OpenSHMEM. The CoVer framework previously addressed this by introducing a generic, contract-based approach that decoupled API requirements from the core tool. However, CoVer's effectiveness remains bounded by the expressiveness of its underlying contract language, restricting the types of errors it can verify. This paper presents an extension to the CoVer contract language designed to capture and check a broader range of error classes. Our extensions introduce generic parameter checking and allocation tracking, while keeping generality across both programming model and language. We evaluate these extensions and demonstrate that analysis accuracy remains consistent across multiple languages, reinforcing the framework's general applicability. While the additional runtime analyses naturally incur a performance overhead, these improvements greatly enhance CoVer's utility with a significant accuracy improvement.