Sound Transaction-based Reduction without Cycle Detection

September 28, 2005
Robert Palmer | University of Utah

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.

Speaker Details

Robert is a graduate student at the University of Utah where he is involved with the Utah Gauss project aimed at verifying MPI based concurrent programs. Robert has been an Instructor at Utah, an Intern at MSR, and currently is interning at Intel doing program verification. Robert’s primary interest is in program correctness with a slant towards automated reasoning. In his spare time he designs circuits and writes programs with his six year old son, reads books about trucks to his two year old son, and goes for walks with his wife.