Automatic Discovery of Transition Symmetry in Multithreaded Programs Using Dynamic Analysis

While symmetry reduction has been established to be an important technique for reducing the search space in model checking, its application in concurrent software verification is still limited, due to the difficulty of specifying symmetry in realistic software. We propose an algorithm for automatically discovering and applying transition symmetry in multithreaded programs during dynamic model checking. Our main idea is using dynamic program analysis to identify a permutation of variables and labels of the program that entails syntactic equivalence among the residual code of threads and to check whether the local states of threads are equivalent under the permutation. The new transition symmetry discovery algorithm can bring substantial state space savings during dynamic verification of concurrent programs. We have implemented the new algorithm in the dynamic model checker Inspect. Our preliminary experiments show that this algorithm can successfully discover transition symmetries th...

• Type: Conference
• Year: 2009
• Where: SPIN
• Authors: Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, Chao Wang
• Keywords: Dynamic Model, Model Checking, SPIN 2009, Theoretical Computer Science, Transition Symmetry