|
|
 |
|
NIA Seminar by Jonathan Ezekiel |
|
Date: March 24, 2006
Time: 10:30am
Location: NIA, Rm 137
Parallelizing a Model Checker on Shared-Memory Machines
Jonathan Ezekiel, University of York, UK
Model checking is a decision procedure for the automatic verification of finite state systems. It usually requires the preliminary step of constructing the state-space of the system. During this step the number of states can grow exponentially with the number of processes. This is known as the state explosion problem which often causes the execution of the decision procedure to be resource-consuming in terms of memory and CPU time.
One approach to addressing the state explosion problem is to utilize the extra time and memory resources offered by multiprocessor machines. Due to it's irregular nature and dependencies between tasks the state space generation process is difficult to parallelize without incurring significant run time penalties. This talk presents strategies to deal with the penalties and facilitate parallelism on a shared-memory architecture.
These strategies have been applied to the state space generation algorithm Saturation using the pthreads library and evaluated using thread profiling tools.
|
|
|
Home