Theoretical Comparison of Partial Order Reduction: Java Pathfinder vs. Moonwalker
Abstract: A problem in modern model checkers is the state explosion problem. Many methods exists to reduce the problem whereas partial order reduction is one of the most common methods. The partial order reduction is designed to reduce states that are not relevant for concurrency bugs by making transitions through non-relevant states. There are many different ways to do the partial order reduction and many model checkers uses their own implementation. With different implementations the outcome may differ. This report examines the differences between two similar model checkers with different implementations of the partial order reductions, Java Pathfinder and Moonwalker, by focusing on its state reduction feature and the time it takes to do the reduction. By doing a theoretical comparison this paper tries to answer the questions stated and the testing of Java Pathfinder will deduce how Moonwalker would behave compared to Java Pathfinder for a relevant code. The result was that both Moonwalker and Java Pathfinder reduces most of the states, where Java Pathfinder outperforms Moonwalker slightly. The more interesting result was the time it would take for Moonwalker and Java Pathfinder to do their partial order reduction where Moonwalker could use double or even triple the time compared to Java Pathfinder.
AT THIS PAGE YOU CAN DOWNLOAD THE WHOLE ESSAY. (follow the link to the next page)