Towards Efficient Verification of Parallel Applications with Mc SimGrid

TL;DR

This paper enhances the efficiency of verifying parallel applications by adapting the ODOR algorithm to better detect and explain bugs, addressing limitations of existing DPOR techniques in complex, real-world scenarios.

Contribution

It introduces two novel adaptations of the ODOR algorithm, RFS ODPOR for improved bug detection efficiency and a bug origin analysis method, advancing verification techniques for parallel applications.

Findings

RFS ODPOR reduces exploration of uninteresting state space regions.

The bug origin analysis efficiently locates the root causes of bugs.

Adaptations improve verification speed and bug explanation accuracy.

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.