Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applications that Do Not Terminate
This addresses concurrency bugs in event-driven systems like smart homes, offering a novel solution for non-terminating applications, though it is incremental in combining existing techniques.
The paper tackled the challenge of model checking non-terminating event-driven applications by combining dynamic partial order reduction with stateful model checking, resulting in a 7X average speedup and enabling completion for 69 app pairs that previously did not finish.
Event-driven architectures are broadly used for systems that must respond to events in the real world. Event-driven applications are prone to concurrency bugs that involve subtle errors in reasoning about the ordering of events. Unfortunately, there are several challenges in using existing model-checking techniques on these systems. Event-driven applications often loop indefinitely and thus pose a challenge for stateless model checking techniques. On the other hand, deploying purely stateful model checking can explore large sets of equivalent executions. In this work, we explore a new technique that combines dynamic partial order reduction with stateful model checking to support non-terminating applications. Our work is (1) the first dynamic partial order reduction algorithm for stateful model checking that is sound for non-terminating applications and (2) the first dynamic partial reduction algorithm for stateful model checking of event-driven applications. We experimented with the IoTCheck dataset: a study of interactions in smart home app pairs. This dataset consists of app pairs originated from 198 real-world smart home apps. Overall, our DPOR algorithm successfully reduced the search space for the app pairs, enabling 69 pairs of apps that did not finish without DPOR to finish and providing a 7X average speedup.