Efficient parallel CTL model-checking for pushdown systems

A Pushdown system (PDS) is a finite transition system equipped with stacks that are allowed to accurately model procedure calls and mimic the program's stack. Therefore, a PDS is extensively used for the analysis and verification of sequential programs. The computational tree logic (CTL) model checking for PDS is reduced to an emptiness problem, which consists of computing the set of accepting configurations of an alternating Buchi PushDown System(ABPDS). When the PDSs are very large, the emptiness analysis can be time-consuming. In this study, we use the features of a Compute Unified Device Architecture (CUDA) to achieve the parallelism. First, we propose a parallel algorithm to conduct the emptiness analysis of the ABPDS in multi-threads. Thus we propose a partitioned alternating multi automaton, which is a parallel extension of the alternating multi automaton (AMA) to represent the infinite set of configurations for the alternating Pushdown System and demonstrate how the emptiness analysis can be conducted in parallel based on a partitioned alternating multi automaton. Second, the process of the emptiness analysis is irregular, which means it is difficult to allocate resources dynamically. In order to effectively utilize the graphics processing unit (GPU), we design a new data structure and use thread scheduling to fit the computing model. The algorithm is implemented in a tool and is compared to the PDS model checker PuMoC as a benchmark. The results demonstrate a significant performance speedup (average 50X and up to 180X).