On the Generation of Initial Contexts for Effective Deadlock Detection

TL;DR

This paper introduces a technique to generate initial contexts for deadlock detection in distributed systems, reducing the combinatorial complexity by focusing on contexts likely to lead to deadlocks, thus enhancing the effectiveness of symbolic execution-based analysis.

Contribution

It proposes a static analysis-guided method to generate initial contexts that are more likely to cause deadlocks, integrated into an existing detection framework to eliminate the need for user-provided contexts.

Findings

Effective generation of initial contexts for deadlock detection

Reduction of combinatorial explosion in context analysis

Integration with symbolic execution framework improves deadlock analysis

Abstract

It has been recently proposed that testing based on symbolic execution can be used in conjunction with static deadlock analysis to define a deadlock detection framework that: (i) can show deadlock presence, in that case a concrete test-case and trace are obtained, and (ii) can also prove deadlock freedom. Such symbolic execution starts from an initial distributed context, i.e., a set of locations and their initial tasks. Considering all possibilities results in a combinatorial explosion on the different distributed contexts that must be considered. This paper proposes a technique to effectively generate initial contexts that can lead to deadlock, using the possible conflicting task interactions identified by static analysis, discarding other distributed contexts that cannot lead to deadlock. The proposed technique has been integrated in the above-mentioned deadlock detection framework hence enabling it to analyze systems without the need of any user supplied initial context.