home › event - parallel model checking using abstraction

EVENT:

Parallel model checking using abstraction
Conferences & Talks

 

description

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

 

upcoming events   view all 

The Cutting Edge of Artificial Intelligence
Tolga Kurtoglu, Margareta Ackerman, Andra Keay, Piero Scaruffi, Allen Saakyan
22 February 2018 | George E. Pake Auditorium, PARC
PARC Forum  

Printed Electronics: From Vision to Disruption
Markus Larsson
13 March 2018 | Munich, Germany
Conferences & Talks  

The Ghost in the Smart Machine (Panel)
Tolga Kurtoglu, Panelist
22 March 2018 | Chicago, IL
Conferences & Talks  

Bringing Reliable (and Transparent) AI to Business (Keynote)
Tolga Kurtoglu, Keynote Speaker
26 April 2018 | Seattle, WA
Conferences & Talks