Petri Net Unfolding-Based Detection and Replay of Program Deadlocks

Abstract

Program deadlock detection plays an important role in ensuring the stability of software systems. In view of the high efficiency and low false alarm rate, dynamic deadlock analysis methods are widely studied. However, existing dynamic analysis methods use lock graph or its extended variants to model program behavior. Since there are information loss in existing lock graphs, deadlock false positives still exist. To solve the problem, a novel 2-stage dynamic deadlock analysis method is proposed. In the first stage, a Petri net model of the program is constructed by analyzing program running traces. Then, unfolding-based Petri net dead marking detection methods are used to identify potential program deadlocks. In the second stage, based on Petri net unfolding techniques, a deterministic program scheduling scheme that can be used for deadlock replay is derived for each potential deadlock. Each successfully replayed program deadlock is a real deadlock. It is shown that the proposed deadlock detection and replay method can eliminate more false positives compared to general dynamic methods, and the deadlock replay scheme is deterministic and easy to understand compared with existing random scheduling strategies.

Keywords

• Petri net
• deadlock detection
• net unfolding
• discrete event system
• program verification