pith. sign in

arxiv: 2604.20410 · v1 · submitted 2026-04-22 · 💻 cs.DC · cs.PL

Extending Contract Verification for Parallel Programming Models to Fortran

Yussur Mustafa Oraji , Christian Bischof This is my paper

Pith reviewed 2026-05-09 23:01 UTC · model grok-4.3

classification 💻 cs.DC cs.PL
keywords FortranMPIcontract verificationparallel programmingprogram analysisHPC correctnessstatic analysisdynamic analysis
0
0 comments X

The pith

A contract-based verification framework for MPI programs has been extended to support Fortran while remaining more efficient than the leading alternative tool.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The authors extend their prior CoVer framework to handle Fortran in addition to C/C++ for verifying parallel programs using models like MPI. This matters because many high-performance computing codes are written in Fortran, yet most verification tools are restricted to other languages or specific error types. By modifying contract definitions and analysis methods to account for language differences, the tool maintains its ability to perform static and dynamic checks across languages. Evaluation shows the extension keeps the same accuracy, detects an existing bug in a benchmark suite, and runs substantially faster than the state-of-the-art tool MUST.

Core claim

By adapting language-specific contract definitions and modifying the analyses, CoVer now supports both C/C++ and Fortran programs for verifying parallel programming models. This preserves the framework's generality and analysis accuracy, reveals a bug in the MPI-BugBench testing framework, and makes the Fortran version substantially more efficient than MUST.

What carries the argument

CoVer, the generic contract-based verification framework for parallel programming models, with extensions to contract definitions and analysis passes for Fortran support.

If this is right

  • The tool enables verification of Fortran-based parallel applications without needing separate language-specific checkers.
  • Error detection accuracy remains consistent across C/C++ and Fortran, supporting mixed-language projects.
  • The approach demonstrates efficiency advantages over specialized tools like MUST for Fortran codes.
  • Contract verification can help identify flaws in error-testing benchmarks themselves.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If similar adaptations are feasible, the framework could support additional languages used in HPC.
  • The efficiency difference may relate to how Fortran compilers or memory models interact with the analysis, suggesting optimization paths.
  • Broader adoption could standardize contract use for parallel correctness in scientific computing.
  • Validating tools against multiple languages strengthens confidence in benchmark suites like MPI-BugBench.

Load-bearing premise

Adapting the contracts and analyses for Fortran does not reduce the coverage of error classes or introduce new inaccuracies compared to the original C/C++ implementation.

What would settle it

A collection of Fortran MPI programs containing errors that CoVer should detect based on its contracts, but where the tool either misses the errors or reports false positives.

Figures

Figures reproduced from arXiv: 2604.20410 by Christian Bischof, Yussur Mustafa Oraji.

Figure 1
Figure 1. Figure 1: Example of contract definitions (C/C++). hold prior to any callsite of MPI_Get, as indicated by the PRE scope. Finally, in that scope is an operation, more specifically a call operation with MPI_Init as the target. Further, there are additional requirements in the postcondition scope (POST), which in this case forbid data races. MPI_Get is a non-blocking call, which means that the function may return prior… view at source ↗
Figure 2
Figure 2. Figure 2: Architecture of CoVer-Static, from [19]. [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Example of contract definitions (Fortran). [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Overview of some additional Fortran metadata in the LLVM IR. [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Results of the overhead analysis. IR often carries additional metadata for variables. CoVer-Dynamic inserts ad￾ditional instrumentation when it is accessed, causing significant slowdown com￾pared to C. We have implemented multiple methods to reduce the number of instrumented metadata accesses, though currently the number of instrumented calls due to memory accesses is still around 2x to that of C code. 5 R… view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper extends the CoVer contract-based verification framework to Fortran by adapting language-specific contract definitions and modifying the static and dynamic analyses to handle both C/C++ and Fortran programs using parallel models such as MPI. The evaluation asserts that the enhanced tool preserves the original analysis accuracy, discovers a bug in the MPI-BugBench framework, and achieves substantially higher efficiency than the state-of-the-art MUST tool while retaining cross-language generality.

Significance. If the accuracy-preservation claim holds under rigorous cross-language testing, the work would meaningfully broaden the reach of generic contract-based verification to Fortran-heavy HPC codes, where existing tools are often C/C++-only. The reported efficiency edge over MUST and the incidental bug discovery would strengthen the case for language-agnostic contract approaches in distributed-memory correctness checking.

major comments (2)
  1. Evaluation section: the central claim that language-specific adaptations 'preserve CoVer's analysis accuracy' lacks supporting evidence such as an enumeration of modified contract rules for Fortran array semantics and argument passing, or side-by-side detection results on matched MPI error patterns across languages; without this, it is impossible to confirm that error-class coverage and false-positive/negative rates remain unchanged.
  2. Evaluation section: quantitative performance claims (substantially more efficient than MUST) are presented without full methodology details, error bars, or raw timing data, undermining assessment of the efficiency result that is highlighted in the abstract.
minor comments (2)
  1. The manuscript would benefit from explicit discussion of Fortran-specific edge cases (e.g., assumed-shape arrays, I/O statements) that could affect dynamic contract insertion or static analysis soundness.
  2. Abstract and evaluation: the bug discovery in MPI-BugBench is noted but not described in sufficient detail to allow readers to reproduce or understand its relation to the Fortran port.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback on our manuscript. We address each major comment below and describe the changes we will make in the revised version.

read point-by-point responses

  1. Referee: Evaluation section: the central claim that language-specific adaptations 'preserve CoVer's analysis accuracy' lacks supporting evidence such as an enumeration of modified contract rules for Fortran array semantics and argument passing, or side-by-side detection results on matched MPI error patterns across languages; without this, it is impossible to confirm that error-class coverage and false-positive/negative rates remain unchanged.

    Authors: We agree that additional explicit evidence is needed to substantiate the accuracy-preservation claim. In the revised manuscript we will add a dedicated subsection enumerating the principal modifications to the contract rules required for Fortran array semantics and argument-passing conventions. We will also include a side-by-side comparison table showing detection outcomes for a representative set of MPI error patterns executed in both C/C++ and Fortran, thereby documenting that error-class coverage and false-positive/negative rates are unchanged. The incidental discovery of a bug in MPI-BugBench when exercising the Fortran port supplies further empirical support for cross-language consistency. revision: yes

  2. Referee: Evaluation section: quantitative performance claims (substantially more efficient than MUST) are presented without full methodology details, error bars, or raw timing data, undermining assessment of the efficiency result that is highlighted in the abstract.

    Authors: We accept that the performance results would be more convincing with fuller methodological transparency. In the revision we will expand the experimental-setup description to include hardware specifications, the number of repetitions performed, and the precise measurement procedure. Where multiple runs were executed we will report error bars; otherwise we will state the single-run nature of the measurements. Raw timing data for all benchmarks will be provided in an appendix or as supplementary material so that readers can independently assess the reported efficiency advantage over MUST. revision: yes

Circularity Check

0 steps flagged

No circularity: claims rest on implementation adaptations and independent evaluation

full rationale

The paper describes concrete language-specific adaptations to contract definitions and analyses to support Fortran alongside C/C++, then reports empirical results from running the extended CoVer on test suites, direct efficiency comparison to MUST, and discovery of a bug in MPI-BugBench. No derivation chain, fitted parameters, or self-referential equations are present; the accuracy-preservation claim is tied to the evaluation rather than to any prior CoVer result by construction. The single self-citation to the authors' earlier CoVer work supplies only the base framework and is not load-bearing for the Fortran-extension claims, which remain externally falsifiable via the reported experiments.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work assumes contract specifications can be ported across languages with only local changes and that the underlying analysis remains sound after modification.

axioms (1)
  • domain assumption Contract definitions can be adapted per language without loss of verification power for parallel error classes
    Invoked when the paper states it adapted language-specific contract definitions for Fortran.

pith-pipeline@v0.9.0 · 5454 in / 1078 out tokens · 17112 ms · 2026-05-09T23:01:06.063250+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

23 extracted references · 23 canonical work pages

  1. [1]

    llvm.org/docs/Directives.html

    Compiler directives supported by Flang — The Flang Compiler,https://flang. llvm.org/docs/Directives.html

    work page

  2. [2]

    The LLVM Project,https://llvm.org/

    work page

  3. [3]

    In: Recent Advances in the Message Passing Interface

    Burak, S., Ivanov, I.R., Domke, J., Müller, M.: SPMD IR: Unifying SPMD and Multi-value IR Showcased for Static Verification of Collectives. In: Recent Advances in the Message Passing Interface. pp. 3–20. Springer (2025).https: //doi.org/10.1007/978-3-031-73370-3_1

    work page doi:10.1007/978-3-031-73370-3_1 2025

  4. [4]

    Droste, M

    Droste, A., Kuhn, M., Ludwig, T.: MPI-checker: Static analysis for MPI. In: Proceedings of the Second Workshop on the LLVM Compiler Infrastructure in HPC. pp. 1–10. LLVM ’15, Association for Computing Machinery (Nov 2015). https://doi.org/10.1145/2833157.2833159

    work page doi:10.1145/2833157.2833159 2015

  5. [5]

    In: Tools for High Per- formance Computing 2009

    Hilbrich, T., Schulz, M., de Supinski, B.R., Müller, M.S.: MUST: A Scalable Ap- proach to Runtime Error Detection in MPI Programs. In: Tools for High Per- formance Computing 2009. pp. 53–66. Springer (2010).https://doi.org/10.1007/ 978-3-642-11261-4_5

    work page 2009

  6. [6]

    Jammer, T., Saillard, E., Schwitanski, S., Jenke, J., Vinayagame, R., Hück, A., Bischof,C.:MPI-BugBench:AFrameworkforAssessingMPICorrectnessTools.In: Recent Advances in the Message Passing Interface. pp. 121–137. Springer (2025). https://doi.org/10.1007/978-3-031-73370-3_8 12 Y. Oraji et al

    work page doi:10.1007/978-3-031-73370-3_8 2025

  7. [7]

    Legate numpy: Accelerated and distributed array computing,

    Laguna, I., Marshall, R., Mohror, K., Ruefenacht, M., Skjellum, A., Sultana, N.: A large-scale study of MPI usage in open-source HPC applications. In: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis. pp. 1–14. SC ’19, Association for Computing Machinery, New York, NY, USA (Nov 2019).https://doi....

    work page doi:10.1145/3295500.3356176 2019

  8. [8]

    Lattner, C., Adve, V.: Data Structure Analysis: A Fast and Scalable Context- Sensitive Heap Analysis

    work page

  9. [9]

    Concurrency and Computation: Practice and Experience15(2), 93–100 (2003).https://doi.org/10.1002/cpe.705

    Luecke, G., Chen, H., Coyle, J., Hoekstra, J., Kraeva, M., Zou, Y.: MPI-CHECK: A tool for checking Fortran 90 MPI programs. Concurrency and Computation: Practice and Experience15(2), 93–100 (2003).https://doi.org/10.1002/cpe.705

    work page doi:10.1002/cpe.705 2003

  10. [10]

    Message Passing Interface Forum: MPI: A Message-Passing Interface Standard Version 5.0 (2025),https://www.mpi-forum.org/docs/mpi-5.0/mpi50-report.pdf

    work page 2025

  11. [11]

    Norman,M.R.:miniWeather.OakRidgeNationalLaboratory(ORNL),OakRidge, TN (United States) (Mar 2020).https://doi.org/10.11578/dc.20201001.88

    work page doi:10.11578/dc.20201001.88 2020

  12. [12]

    NVIDIA: NVIDIA Collective Communication Library (NCCL) Documentation (2025),https://docs.nvidia.com/deeplearning/nccl/

    work page 2025

  13. [13]

    OpenSHMEM Committee: OpenSHMEM: Application Programming Inter- face Version 1.5 (2020),http://openshmem.org/site/sites/default/site_files/ OpenSHMEM-1.5.pdf

    work page 2020

  14. [14]

    Oraji, Y.M.: Artifact for ’Extending Contract Verification for Parallel Program- ming Models to Fortran’.https://doi.org/10.5281/zenodo.18679755

    work page doi:10.5281/zenodo.18679755

  15. [15]

    Oraji, Y.M.: Fix unmatched wait for correct request-based rma (!28)·Merge requests·High Performance Computing - Public / MPI-BugBench·GitLab (Jan 2026),https://git-ce.rwth-aachen.de/hpc-public/mpi-bugbench/-/merge_ requests/28

    work page 2026

  16. [16]

    Oraji, Y.M., Hück, A., Bischof, C.: Extending MPI Correctness Benchmarking to theFortranLanguage.In:ProceedingsoftheSC’25WorkshopsoftheInternational Conference for High Performance Computing, Networking, Storage and Analysis. pp. 244–248. SC Workshops ’25, Association for Computing Machinery (Nov 2025). https://doi.org/10.1145/3731599.3767366

    work page doi:10.1145/3731599.3767366 2025

  17. [17]

    Oraji, Y.M., Hück, A., Bischof, C.: Dynamic Contract Analysis for Parallel Pro- gramming Models (preprint, peer-reviewed article to appear in IPDPS HIPS 2026 workshop proceedings) (Mar 2026).https://doi.org/10.48550/arXiv.2603.03023

    work page doi:10.48550/arxiv.2603.03023 2026

  18. [18]

    In: Pro- ceedings of the SC ’25 Workshops of the International Conference for High Perfor- mance Computing, Networking, Storage and Analysis

    Oraji, Y.M., Schwitanski, S., Burak, S., Bischof, C., Müller, M.: Coupling Static and Dynamic MPI Correctness Tools to Optimize Accuracy and Overhead. In: Pro- ceedings of the SC ’25 Workshops of the International Conference for High Perfor- mance Computing, Networking, Storage and Analysis. pp. 188–197. SC Workshops ’25, Association for Computing Machine...

    work page arXiv 2025

  19. [19]

    In: Recent Advances in the Message Passing Interface

    Oraji, Y.M., Schwitanski, S., Hück, A., Jenke, J., Kreutzer, S., Bischof, C.: Veri- fying MPI API Usage Requirements with Contracts. In: Recent Advances in the Message Passing Interface. pp. 54–72. Springer (2026).https://doi.org/10.1007/ 978-3-032-07194-1_4

    work page 2026

  20. [20]

    The International Jour- nal of High Performance Computing Applications28(4), 425–434 (Nov 2014)

    Saillard, E., Carribault, P., Barthou, D.: PARCOACH: Combining static and dynamic validation of MPI collective communications. The International Jour- nal of High Performance Computing Applications28(4), 425–434 (Nov 2014). https://doi.org/10.1177/1094342014552204

    work page doi:10.1177/1094342014552204 2014

  21. [21]

    Jigsaw: Accelerating spmm with vector sparsity on sparse tensor core,

    Schwitanski, S., Oraji, Y.M., Pätzold, C., Jenke, J., Tomski, F., Müller, M.S.: RMASanitizer: Generalized Runtime Detection of Data Races in Remote Mem- ory Access Applications. In: Proceedings of the 53rd International Conference on Extending Contract Verification for Parallel Programming Models to Fortran 13 Parallel Processing. pp. 833–844. ICPP ’24, A...

    work page doi:10.1145/3673038.3673109 2024

  22. [22]

    Available: http://doi.acm.org/10.1145/2892208.2892235

    Sui, Y., Xue, J.: SVF: Interprocedural static value-flow analysis in LLVM. In: Proceedings of the 25th International Conference on Compiler Construction. pp. 265–266. CC ’16, Association for Computing Machinery (Mar 2016).https://doi. org/10.1145/2892208.2892235

    work page doi:10.1145/2892208.2892235 2016

  23. [23]

    In: 2014 IEEE High Performance Extreme Computing Conference (HPEC)

    Van der Wijngaart, R.F., Mattson, T.G.: The Parallel Research Kernels. In: 2014 IEEE High Performance Extreme Computing Conference (HPEC). pp. 1–6 (Sep 2014).https://doi.org/10.1109/HPEC.2014.7040972

    work page doi:10.1109/hpec.2014.7040972 2014