Parallelizing model checking algorithms using multi-core and many-core architectures

• Main Author: Wu, Zhimin
• Other Authors: Liu Yang
• Format: Theses and Dissertations
• Language: English
• Published: 2017
• Subjects: DRNTU::Engineering::Computer science and engineering::Software::Software engineering
• Online Access: http://hdl.handle.net/10356/72377
• Institution: Nanyang Technological University

The reliance on the functioning of software systems is growing with the development of IT industry. The complexity and scalability to design these systems are increasing, especially for concurrent systems with concurrent executions, communications and resource distributions, e.g., classical cryptography protocols and quantum communication systems. Thus, the reliability of these systems becomes crucial. Model checking is an automated verification approach to validate these complicated systems, which has been proved to be effective in discovering errors. Model checking works through the exploration of all possible system states in a brute force manner. This technique checks whether a system model meets a given specification, and it consists of system modeling, requirement specification, and verification. Compared to other traditional approaches, e.g., simulation, testing, and deductive verification, model checking has many advantages for its automatic and exhaustive searching. However, model checking is not feasible for systems with infinite state space, since the data size would be unbounded or the number of processes would be infinite. For finite state space systems, there are also two major problems or obstacles that limit the usage of model checking techniques in practical industrial systems. Firstly, model checking suffers from the infamous state space explosion problem. Secondly, the efficiency of algorithms on model checking is always subject to the size of state space. It is challenging to handle the examination of largest possible state space efficiently with limited processors and memories. By now, many techniques are proposed to handle the state space explosion problem. Symbolic model checking approaches reduce the cost of storage to store the system model by representing the state space implicitly with the structure called binary decision diagram (BDD). Partial order reduction is designed to deal with the state space explosion in concurrent systems with asynchronous components. It builds a reduced state space which eliminates the additional interleaving sequences for executions. On-the-fly model checking avoids generating the complete state space by conducting the verification during the process of state space generation. Symmetry Reduction, which is based on group theory, reduces the size of the state space by identifying the isomorphic states in the state space. Besides these typical smart techniques, parallel computing has recently been garnering much attention in the model checking community. Parallel computing is primarily implemented to extend the available computation resources to handle larger systems. The performance improvement gained from the parallelized generating and analyzing of large state spaces is promising. Thus, we conducted our research on the parallelization of model checking problems. The existing research on the parallelization of model checking problems reflects the idea that model checking problems can be transferred to some graph exploration problem. So far, various parallel computing platforms have been utilized, e.g., the multi-core CPU, many-core GPU and even the cloud environment. Based on the survey on previous research, the targets of our research are: 1) parallelizing subproblems in model checking algorithms, 2) improving the parallelization in existing approaches by utilizing the latest techniques in different parallel computing platforms, and 3) combining parallel computing with the existing techniques like on-the-fly model checking for the state space explosion problem. To this end, we analyze the feasibility of algorithms in model checking and start with the algorithms related to LTL model checking. We handle the state space generation, counterexample generation and the onthe-fly strongly connected components (SCC) detection process, to build approaches which optimize the original algorithm via parallelization in different platforms. Then we work on the problem related to probabilistic model checking – the computation of the reachability probabilities, which is also an important subroutine for determining approximately optimal policies of the typical probabilistic model – Markov decision processes (MDPs). We propose a GPU-accelerated value iteration to compute the reachability probabilities of MDPs. Our parallelization of the algorithms achieves expected performance improvement. Besides the algorithm-level parallelization, many existing research present the integration of the parallelized algorithms into many famous model checking tools, so as to prove their applicability. These applications have significantly improved the performance of their original sequential version of algorithms. Therefore, it is promising to extend our research from algorithm level to the application level. Our work has contained the extension of the existing PAT model checker with the concurrent LTL model checking algorithm. We aim at developing a new application which can both cover the model checking techniques, and contribute to the latest realistic problems which have not been covered by the applications mentioned above. To this end, quantum communication attracts our attention and is suitable to be the application domain. To the best of our knowledge, there is no tool support for the formal verification of quantum communication systems, including both the general model checking and the automatic quantum bisimilarity checking. Thus, we design and implement a tool-Qubet1.0, a model checking, bisimulation checking and emulation tool for quantum communication systems. Based on this essential tool, our algorithms-level parallelization is integrated with promising results. To sum up, our research consists of both algorithm-level parallelization and application-level work. Five works are involved in the thesis: we investigate the existing solutions to state space explosion problem and the existing optimizations for model checking algorithms, as well as the latest techniques in different parallel computing platforms, in order to get a better understanding of our targets and the potential solutions. Firstly, we focus on three LTL model checking related problems; we make use of the many-core GPU to construct the parallel on-the-fly state space generation for reachability checking. We gain significant performance speedup (average 50x and up to 100x) compared with the traditional sequential algorithms; we make use of the multi-core CPU to build the concurrent on-the-fly SCC detection for automata-based model checking with fairness assumption. We achieve around 2x speedup for the complete SCC detection in large-scale system models compared to the sequential on-the-fly model checking in PAT. Besides, our parallel on-the-fly fairness checking approach speedups fairness checking around 2x-45x; Also, we exploit the latest architecture of many-core GPU and build the GPU-accelerated Counterexample Generation algorithm, which is proved to be effective and scalable; Secondly, we propose the GPU-based computation of the reachability probabilities. We gain around 10x speedup compared to the sequential version of VI, and around 1.5x-17x speedup compared to the topological value iteration. Finally, we design and implement an applicable tool QUBET1.0, and present that our algorithm-level research works well when being applied to the application. Our application work is significant to the designers of quantum communication systems.