Effective Partial Order Reduction in Model Checking Database Applications

Distributed applications, in particular web applications, often depend on a centralized database. The results of database operations depend on the state of database at that time and often also on the order of execution of operations performed by concurrent clients. Verification of such applications requires modeling all these possible orders so that the user can determine which are incorrect orderings and can prevent them with transactions or business logic. However, straightforward exploration leads to state space explosion. Partial order reduction prunes orderings that are equivalent to other orderings already explored. We present a novel technique of Effective Partial Order Reduction (EPOR) for model checking software of Java applications sharing database state. EPOR improves upon prior work by performing a more precise analysis and supports many more operations. The key idea behind EPOR is that monitoring the effect of database operations inside database implementation gives a more precise view of operation dependencies than what can be achieved from an external view. Like prior work, EPOR also relies on Java Pathfinder model checker for model checking Java application. However, unlike prior work, there is additional instrumentation inside the database that enables our precise analysis and allows supporting more constructs. Our results improve upon prior work by achieving significant reduction in number of states explored and thus enables more effective model checking of database applications with concurrent operations.