Extending Contract Verification for Parallel Programming Models to Fortran

TL;DR

This paper extends the CoVer verification framework to Fortran, enabling cross-language static and dynamic analysis for parallel programming models, and demonstrates improved efficiency and bug detection capabilities.

Contribution

The authors adapt CoVer to support Fortran, broadening its applicability and efficiency in verifying parallel programming models across multiple languages.

Findings

CoVer's analysis accuracy is preserved with Fortran support.

The extended CoVer detected a bug in MPI-BugBench.

Fortran port of CoVer is more efficient than MUST.

Abstract

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.