Why we want to do partial order reductionDefinitionsConditions on ample setsHeuristics for ample setsfsu-logoWhy we want to do partial order reductionDefinitionsConditions on ample setsHeuristics for ample setsPartial Order Reduction (Recitation)David HenriquesCarnegie Mellon UniversityMany slides by Deepak D’Souza (thanks!)December 2nd 2011David Henriques Order Theory 1/ 20fsu-logoWhy we want to do partial order reductionDefinitionsConditions on ample setsHeuristics for ample setsWhat and WhyFor specifications that don’t worry about the order of“independent” tran sitions, it should be enough to explore just oneof the interleaved sequences of independent transitions.rsu u′α ββαDavid Henriques Order Theory 2/ 20fsu-logoWhy we want to do partial order reductionDefinitionsConditions on ample setsHeuristics for ample setsDefinitions◮Transitions α a n d β are said to be independent if◮(Enabledness) Neither α nor β can disable the other. That is ifα and β are both enabl e d in a state s, and sα→ s′, then β isstill enabled at s′(and vice versa).◮(Commutativity) The sequ ence of transi t ions αβ and βα leadto the same stat e .◮A tran sition α is said to be invisible wrt a property tha t uses aset of propositions P if: whenever sα→ s′we have∀p ∈ P : s |= p iff s′|= p.David Henriques Order Theory 3/ 20fsu-logoWhy we want to do partial order reductionDefinitionsConditions on ample setsHeuristics for ample sets(In)DependenceIn different models of computation, different situations generatedependent transi tions:◮Pairs of transitions that share a variable, which is changed byat least one of them.◮Pairs of transitions belonging to the same process.◮Send and recieve transitions that use the same message queue.David Henriques Order Theory 4/ 20fsu-logoWhy we want to do partial order reductionDefinitionsConditions on ample setsHeuristics for ample setsStutter-free LTL◮Two sta te sequences π a n d π′are said to bestutter-equivalent, written π ∼stπ′, iff t h e sequence ofdistinct states is identical in π and π′.◮An LTL formula ϕ is said to be stuffer-free iff for each pa ir ofstutter-equivalent state sequences π and π′, we haveπ |= ϕ iff π′|= ϕ.◮The X -free fragment of LTL given by t h e syntaxϕ ::= p | ¬ϕ | ϕ ∨ ϕ | ϕUϕ. (no X ϕ)is stutter-free.◮Conversely, every LTL property that is stutter-free can beexpressed in the X -free fragment of LTL.David Henriques Order Theory 5/ 20fsu-logoWhy we want to do partial order reductionDefinitionsConditions on ample setsHeuristics for ample setsObjectiveWe want to generate a reduced state transition graph such thateach path in the full state transition graph ha s a stutter-equivalentpath in the reduced graph.We bui ld this graph by DFSing the ful l state graph except that wedisallow some transitions. T h is is called st atic reduction.David Henriques Order Theory 6/ 20fsu-logoWhy we want to do partial order reductionDefinitionsConditions on ample setsHeuristics for ample setsAmple setsEach state s in the model has several trans itions. We call tha t setenabled(s).We want to identify a subset of transitions enabled at s, calledample(s).sample(s)In the DFS search we will only consider neighbours of s that ariseout of transition in ample(s).David Henriques Order Theory 7/ 20fsu-logoWhy we want to do partial order reductionDefinitionsConditions on ample setsHeuristics for ample setsProblems with reductionSuppose ample(s) is chosen to be {β}.rsu u′α ββαProblems:◮The state sequence s, u, r is ignored.◮What if we had a trans ition γ enabled only at u? It (and th epaths starting from it) would also not be explored.David Henriques Order Theory 8/ 20fsu-logoWhy we want to do partial order r eductionDefinitionsConditions on ample setsHeuristics for ample setsConditions on ample sets hel psu u′α βαγγβvr′βrConditions :◮(C0) Ensure enabled(s) 6= ∅implies ample(s) 6= ∅.◮(C1) Ensure that notransition dependent on a βin ample set at s can fi rewithout some transition inample(s) happening first.◮(C2) Ensure ample(s)contains only transitionsinvisible wrt the propertyb eing checked.David Henriques Order Theory 9/ 20fsu-logoWhy we want to do partial order r eductionDefinitionsConditions on ample setsHeuristics for ample setsConditions still not sufficientp¬pα3α1α3α1α2¬p ¬pββββα2α3α2α1Add Condition:◮(C3) Ensure that no cycle in reduced graph, and a transition β,which is always enabled in the cycle but never included in t he amplesets al ong the cycle.David Henriques Order Theory 10/ 20fsu-logoWhy we want to do partial order r eductionDefinitionsConditions on ample setsHeuristics for ample setsCorrectness cl aimTheorem (Correctness of reduction)If ample sets are chosen satisfying conditions (C0) to (C3), thenthe reduced graph contains a stutter-equivalent path for every pathin the original graph.Hence model checking wrt stutter-free LTL properties can be donesoundly on the reduced graph.David Henriques Order Theory 11/ 20fsu-logoWhy we want to do partial order r eductionDefinitionsConditions on ample setsHeuristics for ample setsWarningWe are actually checking for stronger conditions than the onesneeded. However, these procedures are easy to check. There is atradeoff between how precise we wanto to be and how muchcomputational power we are willing to payDavid Henriques Order Theory 12/ 20fsu-logoWhy we want to do partial order r eductionDefinitionsConditions on ample setsHeuristics for ample setsThe fallback planIf everything else fails, we can alwaystake ample(s) = enabled(s)!David Henriques Order Theory 13/ 20fsu-logoWhy we want to do partial order r eductionDefinitionsConditions on ample setsHeuristics for ample setsNotationAssume the existence of several processes Pi◮pci(s) denotes the program counter of process Pi;◮pre(α) is the set of transitions that may enable α;◮dep(α) is th e set of transitions dependent on α;◮Tiis the set of transitions of process Pi◮Ti(s) is the set of transitions of Pienabled in s;◮currenti(s) is the set of transit ions of Pienabled in some states′s.t. pci(s′) = pci(s).(Note: transi tions in Ti(s) are interdependent since they are fromthe same process)David Henriques Order Theory 14/ 20fsu-logoWhy we want to do partial order r eductionDefinitionsConditions on ample setsHeuristics for ample setsNotationαβread = γδwrite = ωs1s2s4s3ωα ωβωγδδωα◮pc1(s3) = 2◮pc2(s3) =