Abstract

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.

Degree

College and Department

Physical and Mathematical Sciences; Computer Science

Rights

http://lib.byu.edu/about/copyright/