Peephole partial order reduction

Chao Wang, Zijiang Yang, Vineet Kahlon, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

49 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationTools 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
Pages382-396
Number of pages15
DOIs
StatePublished - Jul 21 2008
Externally publishedYes
Event"14th International Conference onTools and Algorithms for the Construction and Analysis of Systems, TACAS2008" - Budapest, Hungary
Duration: Mar 29 2008Apr 6 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4963 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other"14th International Conference onTools and Algorithms for the Construction and Analysis of Systems, TACAS2008"
CountryHungary
CityBudapest
Period3/29/084/6/08

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Peephole partial order reduction'. Together they form a unique fingerprint.

  • Cite this

    Wang, C., Yang, Z., Kahlon, V., & Gupta, A. (2008). Peephole partial order reduction. In 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 (pp. 382-396). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4963 LNCS). https://doi.org/10.1007/978-3-540-78800-3_29