Partial order reduction using guarded independence relations
View Patent ↗A system and method for conducting symbolic partial order reduction for concurrent systems includes determining a guarded independence relation which includes transitions from different threads that are independent for a set of states, when a condition or predicate holds. Partial order reduction is performed using the guarded independence relation to permit automatic pruning of redundant thread interleavings when the guarded independence condition holds.
1. A method for conducting symbolic partial order reduction for concurrent systems of multithreaded executions, comprising:
determining a guarded independence relation which includes transitions from different threads that are independent for a set of states, when a condition or predicate holds;
performing symbolic partial order reduction in bounded model checking using the guarded independence relation to permit automatic pruning of redundant thread interleavings when the guarded independence condition holds; and
representing all possible length-k interleavings by adding at every time frame copies of program state variables with
Φ
:=
I
(
V
0
)
⋀
⋀
i
=
0
k
(
SCH
(
V
i
)
⋀
⋀
j
=
1
N
TR
j
(
V
i
,
V
i
+
1
)
)
,
where v i εV i denotes a copy of vεV at the i-th time frame and I(v 0 ) represents a set of initial states, SCH represents a transition relation of a scheduler, and TR j ; represents the transition of thread T j .
2. The method as recited in claim 1 , wherein determining a guarded independence relation includes statically computing a potential conflict set between all pairs of thread transitions.
3. The method as recited in claim 1 , further comprising reducing a size of representation of the guarded independence relation, by merging independent thread transition pairs with common independence conditions.
4. The method as recited in claim 1 , further comprising reducing a size of representation of the guarded independence relation, by encoding dependent thread transition pairs.
5. A computer readable medium comprising a computer readable program stored in a computer-readable medium, wherein the computer readable program when executed on a computer causes the computer to perform the steps of claim 1 .
6. A method for conducting symbolic partial order reduction for concurrent systems of multithreaded executions, comprising:
determining an independence relation between transitions of different threads; and
performing symbolic partial order reduction in bounded model checking using a peephole encoding that imposes constraints on a finite window of transitions at a state based on the independence relation to permit automatic pruning of redundant thread interleavings; and
representing possible length-k interleavings by adding at every time frame copies of program state variables with
Φ
:=
I
(
V
0
)
⋀
⋀
i
=
0
k
(
SCH
(
V
i
)
⋀
⋀
j
=
1
N
TR
j
(
V
i
,
V
i
+
1
)
)
,
where v i εV i denotes a copy of vεV at the i-th time frame and I(V 0 ) represents a set of initial states, SCH represents a transition relation of a scheduler, and TR j represents the transition of thread T j .
7. The method as recited in claim 6 , wherein the independence relation is a guarded independence relation.
8. The method as recited in claim 7 , wherein determining the independence relation includes statically computing a potential conflict set between all pairs of thread transitions.
9. The method as recited in claim 7 , further comprising reducing a size of representation of the guarded independence relation, by merging independent thread transition pairs with common independence conditions.
10. The method as recited in claim 7 , further comprising reducing a size of representation of the guarded independence relation, by encoding dependent thread transition pairs.
11. The method as recited in claim 6 , wherein the peephole encoding adds constraints to permit automatic pruning of redundant thread interleavings during a search performed by a Satisfiability Modulo Theory/Boolean Satisfiability (SMT/SAT) solver.
12. The method as recited in claim 11 , further comprising determining transaction boundaries of a concurrent system, wherein the peephole encoding is applied only on transitions that denote context switches between threads at the transaction boundaries.
13. The method as recited in claim 11 , further comprising performing symbolic partial order reduction during SMT/SAT based bounded model checking of the concurrent system to find design errors.
14. The method as recited in claim 6 , wherein the peephole encoding provides constraints that guarantee optimal reduction of thread interleavings for programs with two threads.
15. The method as recited in claim 6 , further comprising determining transaction boundaries of a concurrent system, wherein the peephole encoding is applied only on transitions that denote context switches between threads at the transaction boundaries.
16. A computer readable medium comprising a computer readable program stored in a computer-readable medium, wherein the computer readable program when executed on a computer causes the computer to perform the steps of claim 6 .