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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Dynamic Partial Order Reduction for Transactional Programs on Serializable Platforms

  • Parosh Aziz Abdulla,
  • Ashutosh Gupta,
  • Shankara Narayanan Krishna,
  • Omkar Tuppe

摘要

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.