Sound Transaction-based Reduction without Cycle Detection

Опубликовано 6 сентября 2016, 5:59

Model checking has been used to find numerous bugs in software systems. This success comes from the toolΓÇÖs ability to enumerate all possible system states. When the system being examined is multithreaded the number of system states tends to be exponentially larger than single threaded systems due to the many possible permutations of transition interleaving orders. Reduction techniques based on Ample sets exist (called Partial-order Reduction or Model Checking with Representatives) that eliminate many of the redundant interleaving orders. Natural Ample sets can be computed for systems that communicate predominately through message channels. Reduction techniques based on LiptonΓÇÖs theory of left and right movers provides the same benefit of eliminating many redundant interleaving orders by forming Transactions. Transactions can be computed quite naturally for systems that communicate using a locking discipline and shared memory. Both reduction techniques operate by controlling the thread scheduler thereby delaying the execution of some threads. However, delaying the execution of threads indefinitely can result in a loss of soundness. This is commonly referred to as The Ignoring Problem in Partial-order Reduction. Classical reduction algorithms detect cycles in the thread execution to insure no thread is ignored. In my talk I will present an overview of The Ignoring Problem for Partial-order Reduction and how it is ΓÇ£fixedΓÇ¥ using cycle detection. I will present a new Transaction based reduction algorithm for model checking multithreaded systems that does not use cycle detection to insure soundness. This algorithm generally performs better than cycle detection in Transaction based reduction. When the model checker is part of an abstraction refinement framework this algorithm really shines.