Introduction to Partial Order Reductions ======================================== :: November 6, 2014 Séminaire Spécification - Vérification Université Paris 13 In model checking, a well known source of state-space explosion (SSE) is the explicit representation of concurrent actions by their interleavings. Partial-order reductions (PORs) are a family of techniques attempting to cope with this by constructing an equivalent state space where irrelevant executions of the original are discarded. This talk will be a gentle introduction to the topic. We will focus on Godefroid's persistent sets, prove that a selective exploration based on them visits all deadlocks, discuss the two main classes of algorithms for computing them, and finish, time permitting, with an overview of the conceptual similarities and differences between PORs and the unfolding technique. Problem and Main Idea --------------------- x Example PN with concurrency x State explosion, diamonds x Model of computation; assumptions x Commutativity x Equivalence relation on runs x Sufficient to explore one per class x Partitioning of the interleaving space x Commutativity is expensive -> unconditional independence x Def: unconditional independence - Execution + independence relation = dependency graph Persistent Sets --------------- x Def: persitent sets x Def: reduced state space x Thm 4.3: preservation of deadlocks x Local reachability, firability x Global reachability; reduction to deadlock x Caveat: conjecture, exponentially larger SE - Ample sets: same principle, specific extensions for LTL\X Sleep Sets ---------- - Example and main idea - Stateless algorithm: persistent and sleep sets, [God97] Algorithms ---------- - Deciding if a set is persistent is hard -> overapproximations - Static overapproximation - Static stubborn sets - Dynamic POR, [FG05] - Two words about ODPOR, [POPL'14] Evaluation ---------- x [FG05] Relation with unfoldings ------------------------ - Slide Summary ------- - Persistent (ample, stubborn) sets exploit `independence of transitions` - Sleep sets expoit information about the past - They Explore `at least one` interleaving per class - Dynamic vs static computation of persistent sets Miscellanea ----------- - horaire - exposés suivants - mail à qui? - calendrier christine, mahdi Conditional independence revisited ---------------------------------- - why it's interesting: FIFO channels (send, receive, length) - link to Mazurkiewick traces is lost Ouf of scope ------------ - ODPOR - Ample sets