Dynamic Partial Order Reduction for Transactional Programs on Serializable Platforms
摘要
In this paper, we present a stateless model checking algorithm for establishing the correctness of database backed applications modeled as transactional programs under the strongest isolation level, namely serializability. We show that our algorithm is sound, complete, optimal and runs with polynomial memory consumption. In contrast, existing DPOR algorithms for transactional programs work only with weak isolation levels exploring exponentially many more equivalence classes of executions than what serializability permits. We report an implementation of our algorithm by applying it to several thousands of litmus tests as well as challenging database backed applications from the literature.