Loading...
Please wait, while we are loading the content...
Similar Documents
Peephole partial order reduction.
| Content Provider | CiteSeerX |
|---|---|
| Author | Gupta, Aarti Yang, Zijiang Wang, Chao Kahlon, Vineet |
| Abstract | 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. 1 |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Concurrent Software Persistent Set New Peephole Reduction Method Redundant Interleavings Automatic Pruning Explicit-state Algorithm Symbolic Method Peephole Partial Order Reduction Symbolic Dynamic Partial Order Reduction Execution Path Smt Sat Solver Symbolic Formulation Concise Constraint Guarded Independent Transition New Method Peephole Reduction |
| Content Type | Text |
