Stubborn Transaction Reduction .

The exponential explosion of parallel interleavings remains a fundamentalchallenge to model checking of concurrent programs. Both partial-orderreduction (POR) and transaction reduction (TR) decrease the number ofinterleavings in a concurrent system. Unlike POR, transactions also reduce thenumber of intermediate states. Modern POR techniques, on the other hand, offermore dynamic ways of identifying commutative behavior, a crucial task forobtaining good reductions.

We show that transaction reduction can use the same dynamic commutativity asfound in stubborn set POR. We also compare reductions obtained by POR and TR,demonstrating with several examples that these techniques complement eachother.

With an implementation of the dynamic transactions in the model checkerLTSmin, we compare its effectiveness with the original static TR and two PORapproaches. Several inputs, including realistic case studies, demonstrate thatthe new dynamic TR can surpass POR in practice.