Extending Contract Verification for Parallel Programming Models to Fortran
This work addresses programming errors in high-performance computing for developers using Fortran, but it is incremental as it builds on prior work to extend language support.
The paper tackled the problem of verifying correctness in parallel programming models like MPI by extending the CoVer framework to support Fortran, enabling static and dynamic analysis across languages. The result showed that the enhanced version preserved analysis accuracy, revealed a bug in MPI-BugBench, and was substantially more efficient than the state-of-the-art tool MUST while maintaining generality.
High-performance computing often relies on parallel programming models such as MPI for distributed-memory systems. While powerful, these models are prone to subtle programming errors, leading to development of multiple correctness checking tools. However, these are often limited to C/C++ codes, tied to specific library implementations, or restricted to certain error classes. Building on our prior work with CoVer, a generic, contract-based verification framework for parallel programming models, we extend CoVer's applicability to Fortran, enabling static and dynamic analysis across multiple programming languages. We adapted language-specific contract definitions and modified the analyses to support both C/C++ and Fortran programs. Our evaluation demonstrates that the enhanced version preserves CoVer's analysis accuracy and even revealed a bug in the MPI-BugBench testing framework, underscoring the effectiveness of the approach. The Fortran port of CoVer turns out to be substantially more efficient than the state-of-the-art tool MUST, while maintaining generality across languages.