Dynamic Partial Order Reduction for Checking Correctness Against Transaction Isolation Levels
Explore a 16-minute conference talk from PLDI 2023 that delves into dynamic partial order reduction algorithms for verifying application correctness under various database transaction isolation levels. Learn about the challenges faced by modern applications using large-scale databases and how weaker isolation levels impact system behavior. Discover the proposed stateless model checking algorithms that work with widely-used weak isolation levels, including Read Committed, Causal Consistency, Snapshot Isolation, and Serializability. Understand how these algorithms achieve completeness, soundness, and optimality while maintaining polynomial memory consumption. Gain insights into the implementation of these algorithms using Java Pathfinder and their application to challenging distributed systems and database scenarios. Access supplementary materials, including available and reusable artifacts, to further explore this research on improving the reliability of database-driven applications.