Parallel model checking using abstraction

摘要: Many model checking techniques are based on enumerative graph search, a procedure that is known to be prohibitively time and memory consuming. Modern multi-core processors rely parallelism instead of raw clock speed provide increased performance, so it necessary leverage this achieve better performance in checking. In work, we compare hash-distributed well-known parallel search technique for checking, with an algorithm from the automated planning heuristic community called Parallel Structured Duplicate Detection (PSDD). We show PSDD has two major advantages over First, able perform full partial-order reduction where must conservative subsequently miss opportunities many cases, causing much larger space. Second, performs duplicate detection states immediately, avoiding need store inter-thread communication. have implemented compared both Spin checker; our results uses significantly less than can faster give speedup Spin's built-in depth-first search. Finally, how use external memory, such as disk storage, greatly reduce its internal requirements.