A Partial Order Reduction Technique for Event-driven Multi-threaded Programs

TL;DR

This paper introduces a novel partial order reduction technique for event-driven multi-threaded programs that efficiently reduces the number of explored states by not treating event queues as shared objects, improving verification performance.

Contribution

The authors propose a new POR method based on dependence-covering sets that reorders events only when necessary, avoiding unnecessary reordering of events within the same thread.

Findings

Explores significantly fewer transitions than existing methods, often orders of magnitude fewer.

Proves that dependence-covering sets suffice to detect deadlocks and assertion violations.

Implemented a dynamic algorithm demonstrating effectiveness on Android application traces.

Abstract

Event-driven multi-threaded programming is fast becoming a preferred style of developing efficient and responsive applications. In this concurrency model, multiple threads execute concurrently, communicating through shared objects as well as by posting asynchronous events that are executed in their order of arrival. In this work, we consider partial order reduction (POR) for event-driven multi-threaded programs. The existing POR techniques treat event queues associated with threads as shared objects and thereby, reorder every pair of events handled on the same thread even if reordering them does not lead to different states. We do not treat event queues as shared objects and propose a new POR technique based on a novel backtracking set called the dependence-covering set. Events handled by the same thread are reordered by our POR technique only if necessary. We prove that exploring dependence-covering sets suffices to detect all deadlock cycles and assertion violations defined over local variables. To evaluate effectiveness of our POR scheme, we have implemented a dynamic algorithm to compute dependence-covering sets. On execution traces obtained from a few Android applications, we demonstrate that our technique explores many fewer transitions ---often orders of magnitude fewer--- compared to exploration based on persistent sets, wherein, event queues are considered as shared objects.