Search papers, labs, and topics across Lattice.
The authors extend CoVer, a contract-based verification framework for parallel programming models, to support Fortran in addition to C/C++. This enables static and dynamic analysis of parallel codes written in multiple languages using a single tool. The evaluation demonstrates that the extended CoVer maintains accuracy, reveals a bug in MPI-BugBench, and achieves better performance than the state-of-the-art tool MUST.
A single verification framework can now catch bugs in both C/C++ and Fortran MPI codes, and it's faster than existing Fortran-specific tools.
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.
