Load Balancing Parallel Explicit State Model Checking

<p>This research first identifies some of the key concerns about the techniques and algorithms developed for distributed and parallel model checking; specifically, the inherent problem with load balancing and large queue sizes resultant in a static partition algorithm. This research then presents a load balancing algorithm to improve the run time performance in distributed model checking, reduce maximum queue size, and reduce the number of states expanded before error discovery. The load balancing algorithm is based on Generalized Dimension Exchange (GDE). This research presents an empirical analysis of the GDE based load balancing algorithm on three different supercomputing architectures---distributed memory clusters, Networks of Workstations (NOW) and shared memory machines. The analysis shows increased speedup, lower maximum queue sizes and fewer total states explored before error discovery on each of the architectures. Finally, this research presents a study of the communication overhead incurred by using the load balancing algorithm, which although significant, does not offset performance gains.</p>

Name thesis:degree_name

MS

Grantor dc:publisher

Brigham Young University - Provo

Author dc:creator

• Kumar, Rahul

• load
• balancing
• computer
• model
• checking
• verification
• gde
• speedup
• error
• states
• queue
• sizes
• Computer Sciences

Language dc:language

English

Repository record dc:identifier

https://scholarsarchive.byu.edu/etd/44

OAI identifier oai:identifier

oai:scholarsarchive.byu.edu:etd-1043