Using processor virtualization to load balancing distributed state space construction

Most distributed model-checking algorithms use global hash functions to partition state space. This creates load imbalance between computation processors. In this paper, we focus on the use of processor virtualization for parallelizing the state space construction algorithm. Our aim is to optimize the distributed model checking process by using load balancing techniques. We study the effectiveness of Charm++ runtime system and Adaptive Message Passing Interface that support processor virtualization for load balancing the distributed state space construction. The objective is to allow the verification of large and complex systems by maintaining equally loaded processors and achieving higher speed-up. Preliminary experiments are reported to show the benefits of constructing state space using processor virtualization.