Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards Efficient Verification of Parallel Applications with Mc SimGrid

Matthieu Laurent, Thierry Jéron, Martin Quinson

TL;DR

The paper tackles the verification of parallel applications where nondeterministic event orders complicate bug detection. It extends MD-aware model checking by adapting Optimal Dynamic Partial Order Reduction (ODPOR) into McSimGrid with two aims: faster bug discovery via an out-of-order variant (RFS ODPOR) and human-friendly bug explanations through a critical-transition mechanism. They formalize a compact programming model, establish DPOR/ODPOR foundations, and demonstrate that RFS ODPOR preserves soundness and optimality while accelerating bug detection; a CT-based approach provides concise root-cause explanations. Experimental results show RFS ODPOR achieves competitive runtime with higher memory usage, and bug-finding experiments indicate substantial improvements in early fault discovery, suggesting practical impact for large-scale parallel software verification.

Abstract

Assessing the correctness of distributed and parallel applications is notoriously difficult due to the complexity of the concurrent behaviors and the difficulty to reproduce bugs. In this context, Dynamic Partial Order Reduction (DPOR) techniques have proved successful in exploiting concurrency to verify applications without exploring all their behaviors. However, they may lack of efficiency when tracking non-systematic bugs of real size applications. In this paper, we suggest two adaptations of the Optimal Dynamic Partial Order Reduction (ODPOR) algorithm with a particular focus on bug finding and explanation. The first adaptation is an out-of-order version called RFS ODPOR which avoids being stuck in uninteresting large parts of the state space. Once a bug is found, the second adaptation takes advantage of ODPOR principles to efficiently find the origins of the bug.

Towards Efficient Verification of Parallel Applications with Mc SimGrid

TL;DR

The paper tackles the verification of parallel applications where nondeterministic event orders complicate bug detection. It extends MD-aware model checking by adapting Optimal Dynamic Partial Order Reduction (ODPOR) into McSimGrid with two aims: faster bug discovery via an out-of-order variant (RFS ODPOR) and human-friendly bug explanations through a critical-transition mechanism. They formalize a compact programming model, establish DPOR/ODPOR foundations, and demonstrate that RFS ODPOR preserves soundness and optimality while accelerating bug detection; a CT-based approach provides concise root-cause explanations. Experimental results show RFS ODPOR achieves competitive runtime with higher memory usage, and bug-finding experiments indicate substantial improvements in early fault discovery, suggesting practical impact for large-scale parallel software verification.

Abstract

Assessing the correctness of distributed and parallel applications is notoriously difficult due to the complexity of the concurrent behaviors and the difficulty to reproduce bugs. In this context, Dynamic Partial Order Reduction (DPOR) techniques have proved successful in exploiting concurrency to verify applications without exploring all their behaviors. However, they may lack of efficiency when tracking non-systematic bugs of real size applications. In this paper, we suggest two adaptations of the Optimal Dynamic Partial Order Reduction (ODPOR) algorithm with a particular focus on bug finding and explanation. The first adaptation is an out-of-order version called RFS ODPOR which avoids being stuck in uninteresting large parts of the state space. Once a bug is found, the second adaptation takes advantage of ODPOR principles to efficiently find the origins of the bug.
Paper Structure (19 sections, 1 theorem, 3 figures, 1 table, 2 algorithms)

This paper contains 19 sections, 1 theorem, 3 figures, 1 table, 2 algorithms.

Table of Contents

  1. Introduction
  2. Adapting Model Checking Techniques to the Verification of Parallel Applications
  3. Extended Programming Model
  4. Notations and Definitions
  5. State Space Reduction using ODPOR
  6. Making Verification Efficient and Practical
  7. Directed Verification
  8. $\wut$ and $\tree$:
  9. Sleep sets:
  10. Memory management:
  11. Sketch of proof
  12. Example of use: Busy-waiting.
  13. Counter-Example Explainability
  14. Evaluation
  15. Evaluating RFS overhead
  16. ...and 4 more sections

Key Result

theorem 1

The RFS ODPOR algorithm is sound and optimal in the sense that its explores a unique execution per Mazurkiewicz's trace and explores no sleep-set-blocked execution.

Figures (3)

  • Figure 1: A communication pattern using the any wildcard.
  • Figure 2: An exploration tree at some point during CTF+ODPOR algorithm.
  • Figure 3: Number of states explored before finding the deadlock at various scales.

Theorems & Definitions (1)

  • theorem 1