TY - GEN
T1 - Peephole partial order reduction
AU - Wang, Chao
AU - Yang, Zijiang
AU - Kahlon, Vineet
AU - Gupta, Aarti
PY - 2008
Y1 - 2008
N2 - We present a symbolic dynamic partial order reduction (POR) method for model checking concurrent software. We introduce the notion of guarded independent transitions, i.e., transitions that can be considered as independent in certain (but not necessarily all) execution paths. These can be exploited by using a new peephole reduction method. A symbolic formulation of the proposed peephole reduction adds concise constraints to allow automatic pruning of redundant interleavings in an SMT/SAT solver based search. Our new method does not directly correspond to any explicit-state algorithm in the literature, e.g., those based on persistent sets. For two threads, our symbolic method guarantees the removal of all redundant interleavings (better than the smallest persistent-set based methods). To our knowledge, this type of reduction has not been achieved by other symbolic methods.
AB - We present a symbolic dynamic partial order reduction (POR) method for model checking concurrent software. We introduce the notion of guarded independent transitions, i.e., transitions that can be considered as independent in certain (but not necessarily all) execution paths. These can be exploited by using a new peephole reduction method. A symbolic formulation of the proposed peephole reduction adds concise constraints to allow automatic pruning of redundant interleavings in an SMT/SAT solver based search. Our new method does not directly correspond to any explicit-state algorithm in the literature, e.g., those based on persistent sets. For two threads, our symbolic method guarantees the removal of all redundant interleavings (better than the smallest persistent-set based methods). To our knowledge, this type of reduction has not been achieved by other symbolic methods.
UR - http://www.scopus.com/inward/record.url?scp=47249124522&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=47249124522&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-78800-3_29
DO - 10.1007/978-3-540-78800-3_29
M3 - Conference contribution
AN - SCOPUS:47249124522
SN - 3540787992
SN - 9783540787990
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 382
EP - 396
BT - Tools and Algorithms for the Construction and Analysis of Systems - 14th Int. Conf., TACAS 2008 - Held as Part of the Joint European Conf. Theory and Practice of Software, ETAPS 2008 Proceedings
T2 - "14th International Conference onTools and Algorithms for the Construction and Analysis of Systems, TACAS2008"
Y2 - 29 March 2008 through 6 April 2008
ER -