Parallelizing A Symbolic Compositional Model Checking Algorithm Ariel Cohen with Kedar Namjoshi (Bell Labs), Yaniv Sa’ar (Weizmann), Lenore Zuck (UIC/NSF) and Katya Kisyova (UIC) HVC – October 2010 Ariel Cohen Parallelizing A Symbolic Compositional Model Checking Algorithm HVC – 2010 1 Essentials Symbolic BDD-based model checking revolutionized the field. Parallelizing these algorithms, however, has proven difficult. Ariel Cohen Parallelizing A Symbolic Compositional Model Checking Algorithm HVC – 2010 2 Essentials Symbolic BDD-based model checking revolutionized the field. Parallelizing these algorithms, however, has proven difficult. We show how a local reasoning method gives a rise to simple and effective algorithms for parallel, symbolic model checking. Intuition: Many concurrent programs are formed of loosely coupled processes (this is a good design principal); Local (compositional) analysis works well for loosely-coupled processes. Proofs can be carried out with limited mutual knowledge of internal process state; Ariel Cohen Parallelizing A Symbolic Compositional Model Checking Algorithm HVC – 2010 2 Old News Let P := P1 k P2 k ... k PN represents an asynchronous composition of N threads/processes communicating by shared memory. The reachable state space often grows as 2N ; Checking safety properties is PSPACE-complete in N; Modular reasoning is essential for scalability. Ariel Cohen Parallelizing A Symbolic Compositional Model Checking Algorithm HVC – 2010 3 Global Proofs of Always(ϕ) Let P := P1 k P2 k ... k PN ; Proof-Theoretic Method I I I guess a state assertion θ; check that θ is inductive; check θ → ϕ; How to find an appropriate θ? I Model Checking method F F F Ariel Cohen compute reachable states, Reach, as a least fixpoint; take θ to be Reach; check subset relation Reach → ϕ; Parallelizing A Symbolic Compositional Model Checking Algorithm HVC – 2010 4 Local Proofs of Always(ϕ) Guess a vector of assertions, (θ1 , θ2 , ..., θN ) such that Locality: θi is defined on variables visible to process Pi (i.e., the shared variables X and local variables Li ); Step: θi is an inductive invariant for process Pi ; Non-interference: actions of Pj preserve θi , assuming θj ; This is an “assume-guarantee” system – a reformation of Owicki & Gries [1976] Theorem: The last two constraints are equivalent to the statement that θ1 ∧ θ2 ∧ ... ∧ θN is an inductive invariant of the full program. This motivates the name “split invariant” for (θ1 , θ2 , ..., θN ). Ariel Cohen Parallelizing A Symbolic Compositional Model Checking Algorithm HVC – 2010 5 Computing the Split Invariant FOREACH i : initialize θi to the initial states of Pi ; REPEAT FOREACH i : increase θi by computing successors in Pi ; FOREACH i : FOREACH j 6= i : increase θi through interference from θj ; UNTIL (convergence of all θi ) Interference: (Intuitively) θj gives θi a summary of the states it found, in terms of the shared variables Ariel Cohen Parallelizing A Symbolic Compositional Model Checking Algorithm HVC – 2010 6 Computing the Split Invariant FOREACH i : initialize θi to the initial states of Pi ; REPEAT FOREACH i : increase θi by computing successors in Pi ; FOREACH i : FOREACH j 6= i : increase θi through interference from θj ; UNTIL (convergence of all θi ) IF (∧i : θi → ϕ) THEN “ϕ is an invariant”; ELSE “unable to prove ϕ”; END Ariel Cohen Parallelizing A Symbolic Compositional Model Checking Algorithm HVC – 2010 6 Computing the Split Invariant FOREACH i : initialize θi to the initial states of Pi ; REPEAT FOREACH i : increase θi by computing successors in Pi ; FOREACH i : FOREACH j 6= i : increase θi through interference from θj ; UNTIL (convergence of all θi ) Does local reasoning always work? We have an efficient method for exposing local state by adding auxiliary variables (CAV 07). Ariel Cohen Parallelizing A Symbolic Compositional Model Checking Algorithm HVC – 2010 6 Local Reasoning Works Well Example N Reachability Nodes Time (s) Local Reasoning Nodes Time (s) Semaphore (Safety) Peterson’s (Safety) Bakery (Safety) Szymanski (Safety) 10 12 5 6 7 8 3 4 10 20 3 4 9 10 1.2M 10.4 1.8M 440 6.9M 16 91M 509 2.9M 65 11M 844 68k 0.1 395k 0.6 21M 24 over 20 minutes 300k 0.3 11.6M 93 9.1M 63 25M 421 160k 252k 3.7M 43.8M 7.8M 27M 788k 3.8M 371k 2.1M 1.2M 14.6M 4.1M 8.6M Semaphore (Liveness) Bakery (Liveness) Dining-Phil (Liveness) Ariel Cohen Parallelizing A Symbolic Compositional Model Checking Algorithm 0.3 0.5 8.1 172 20 97 2.4 10 1.1 9 2.5 52 8.6 18 HVC – 2010 7 Introducing Parallelism The split invariance calculation is a simultaneous fixpoint over the vector (θ1 , θ2 , ..., θN ); By the chaotic iteration theorem (Cousot & Cousot 1977), any evaluation schedule generates the final answer, so long as it is fair in the limit; This gives rise to a highly non-deterministic parallel algorithm: I I I Ariel Cohen each component θi is computed by a separate thread (i); the effect of each process is broadcast to other processes; repeated until global convergence; Parallelizing A Symbolic Compositional Model Checking Algorithm HVC – 2010 8 Image of Parallel Algorithm Ariel Cohen Parallelizing A Symbolic Compositional Model Checking Algorithm HVC – 2010 9 Problem: Synchronizing BDD Computations We use BDDs; Concurrent BDD access does not scale any better than the distributed scheme described next; Ariel Cohen Parallelizing A Symbolic Compositional Model Checking Algorithm HVC – 2010 10 Problem: Synchronizing BDD Computations We use BDDs; Concurrent BDD access does not scale any better than the distributed scheme described next; In our implementation each machine (thread) i has its own BDD stores for computing θi ; The only BDDs which must be exchanged between machines are ”summary” transitions (only over shared variables) used for interference calculations; This results in replication of BDDs, and BDD copying when summaries are exchanged; Ariel Cohen Parallelizing A Symbolic Compositional Model Checking Algorithm HVC – 2010 10 Copying BDDs BDD stores have to agree on the ordering of the shared variables; This might results in replication of common terms; Cost of copying summary transitions – depends on the amount of shared state; Ariel Cohen Parallelizing A Symbolic Compositional Model Checking Algorithm HVC – 2010 11 Copying BDDs BDD stores have to agree on the ordering of the shared variables; This might results in replication of common terms; Cost of copying summary transitions – depends on the amount of shared state; Experiments on a number of protocols show a speedup of roughly 5.5 − 7.5x on a machine with 8 cores. Ariel Cohen Parallelizing A Symbolic Compositional Model Checking Algorithm HVC – 2010 11 Experiments – Muxsem N Seq. Time Time 4 cores Speedup Eff. Time 8 cores Speedup Eff. 512 1024 1536 2048 27 117 360 561 8.3 34.8 112 165 3.25 3.3 3.2 3.4 0.81 0.82 0.80 0.85 4.8 19.2 65 92 5.6 6.1 5.5 6.1 0.70 0.76 0.69 0.76 N 512 1024 1536 2048 Ariel Cohen Sequential number of BDD nodes 19.5M 81.0M 219.0M 335.0M Parallel number of BDDs nodes 19.8M 82.0M 221.0M 342.0M Parallelizing A Symbolic Compositional Model Checking Algorithm BDD inc. 1% 1% 1% 2% HVC – 2010 12 Experiments – Szymanski N sequential Time Time 4 cores Speedup Eff. Time 8 cores Speedup Eff. 6 7 8 9 20.5 130 564 2896 6.5 41 163 739 3.15 3.17 3.46 3.91 0.78 0.79 0.86 0.97 4.4 23.7 93 492 4.65 5.48 6.06 5.88 0.78 0.78 0.76 0.73 N 6 7 8 9 Ariel Cohen Sequential number of BDD nodes 4.8M 16.1M 49M 141M Parallel number of BDDs nodes 6.9M 23M 73M 216M Parallelizing A Symbolic Compositional Model Checking Algorithm BDD inc. 43% 42% 48% 53% HVC – 2010 13 Experiments – German’s N sequential Time Time 4 cores Speedup Eff. Time 8 cores Speedup Eff. 8 9 10 11 12 185 489 1076 2867 over BDD limit 44 126 268 691 1819 4.20 3.88 4.00 4.14 - 1.05 0.97 1.00 1.03 - 31 76 164 385 1013 5.96 6.40 6.56 7.44 - 0.74 0.80 0.82 0.93 - The number of BDD nodes is the same for sequential and parallel. Ariel Cohen Parallelizing A Symbolic Compositional Model Checking Algorithm HVC – 2010 14 Finishing Up Local-reasoning is effective for loosely-coupled protocols. Sequentially, sometimes faster by a few orders of magnitude than reachability; Parallelism can be exploited for a further speed-up (5.5 − 7.5x on an 8 cores machine); Both single-machine (multi-core) and distributed implementations possible; The parallel implementation can be extended easily to check general temporal properties; Ariel Cohen Parallelizing A Symbolic Compositional Model Checking Algorithm HVC – 2010 15 Open Questions We have not yet considered parallelizing refinement steps; A particularly challenging problem is the implementation of an efficient, thread-safe BDD package; Combine with other techniques; An open task: add parallelism to SPLIT; Ariel Cohen Parallelizing A Symbolic Compositional Model Checking Algorithm HVC – 2010 16 Closely Related Work • Owicki-Gries 1976, Lamport 1977 [local proof rules]; • Moon-Kukula-Shiple-Somenzi 1999 [local reasoning for • • • • synchronous models]; Grumberg-Heyman-Ifergan-Schuster 2005, 2006 [distributed model checking for synchronous models]; Sahoo-Jain-Iyer-Dill-Emerson 2005 [multi-core model checking for synchronous models]; Ezekiel-Luettgen-Cardo 2008 [multi-core, symbolic model checking for asynchronous models]; Stern-Dill 2001, Holzmann-Bosnacki 2007 [parallel, explicit-state model checking for asynchronous models]; (The parallel algorithms all compute exact reachability) Ariel Cohen Parallelizing A Symbolic Compositional Model Checking Algorithm HVC – 2010 17