Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Dynamic Contract Analysis for Parallel Programming Models

Yussur Mustafa Oraji, Alexander Hück, Christian Bischof

TL;DR

CoVer-Dynamic is presented, a dynamic analysis extension that reuses CoVer's contract language to provide a unified static-dynamic verification framework that improves classification accuracy and eliminates false positives on standardized MPI and OpenSHMEM benchmarks, while detecting errors beyond static analysis only.

Abstract

Parallel programming in high-performance computing depends on low-level APIs such as MPI, requiring users to manage synchronization and resources manually. Several correctness checking tools exist to help bug-free code development, though most target a single programming model, limiting their applicability. Our previous work, the static analysis tool CoVer, leverages a contract-based approach enabling users to specify custom error-checking rules and support emerging or unconventional programming models without requiring extensive new tooling. However, static analysis cannot fully reason about runtime-dependent behavior such as pointer aliasing or indirect control flow. To address this, we present CoVer-Dynamic, a dynamic analysis extension that reuses CoVer's contract language to provide a unified static-dynamic verification framework. By enforcing the same contracts at runtime, CoVer-Dynamic improves classification accuracy and eliminates false positives on standardized MPI and OpenSHMEM benchmarks, while detecting errors beyond static analysis only. Our evaluation shows that CoVer-Dynamic consistently outperforms the state-of-the-art correctness checker MUST, averaging a 2x speedup. Finally, our results show limitations in the expressiveness of the contract language, motivating future work to support more error classes.

Dynamic Contract Analysis for Parallel Programming Models

TL;DR

CoVer-Dynamic is presented, a dynamic analysis extension that reuses CoVer's contract language to provide a unified static-dynamic verification framework that improves classification accuracy and eliminates false positives on standardized MPI and OpenSHMEM benchmarks, while detecting errors beyond static analysis only.

Abstract

Parallel programming in high-performance computing depends on low-level APIs such as MPI, requiring users to manage synchronization and resources manually. Several correctness checking tools exist to help bug-free code development, though most target a single programming model, limiting their applicability. Our previous work, the static analysis tool CoVer, leverages a contract-based approach enabling users to specify custom error-checking rules and support emerging or unconventional programming models without requiring extensive new tooling. However, static analysis cannot fully reason about runtime-dependent behavior such as pointer aliasing or indirect control flow. To address this, we present CoVer-Dynamic, a dynamic analysis extension that reuses CoVer's contract language to provide a unified static-dynamic verification framework. By enforcing the same contracts at runtime, CoVer-Dynamic improves classification accuracy and eliminates false positives on standardized MPI and OpenSHMEM benchmarks, while detecting errors beyond static analysis only. Our evaluation shows that CoVer-Dynamic consistently outperforms the state-of-the-art correctness checker MUST, averaging a 2x speedup. Finally, our results show limitations in the expressiveness of the contract language, motivating future work to support more error classes.
Paper Structure (30 sections, 13 figures, 1 table)

This paper contains 30 sections, 13 figures, 1 table.

Table of Contents

  1. Introduction
  2. Background
  3. Error Classes
  4. Missing Initialization or Finalization
  5. Local Data Races
  6. Handle Lifecycle
  7. Common Remote Memory Access Errors
  8. Verification using CoVer
  9. Contract Language
  10. Tool Architecture
  11. Implementing dynamic contract analysis
  12. Challenges of Dynamic Contract Analysis
  13. Contract Availability
  14. Call Interception
  15. Live Error Reporting
  16. ...and 15 more sections

Figures (13)

  • Figure 1: Examples of data races difficult for automatic detection
  • Figure 2: Example of a local data race, as the source data is written to before the communication completes.
  • Figure 3: Example of a request leak. The first handle is lost due to the repeated call.
  • Figure 4: Example of a mixed synchronization error in MPI RMA (fence+lock); only one synchronization method may be used at one time per window.
  • Figure 5: Examples of contract definitions.
  • ...and 8 more figures