GPU Accelerated counterexample generation in LTL model checking

• المؤلفون الرئيسيون: WU, Zhimin, LIU, Yang, LIANG, Yun, SUN, Jun
• التنسيق: text
• اللغة: English
• منشور في: Institutional Knowledge at Singapore Management University 2014
• الموضوعات: Model Check; Share Memory; Task Schedule; Strongly Connect; Component; Model Check Problem; Software Engineering
• الوصول للمادة أونلاين: https://ink.library.smu.edu.sg/sis_research/4988; https://ink.library.smu.edu.sg/context/sis_research/article/5991/viewcontent/gpu.pdf
• المؤسسة: Singapore Management University

Strongly Connected Component (SCC) based searching is one of the most popular LTL model checking algorithms. When the SCCs are huge, the counterexample generation process can be time-consuming, especially when dealing with fairness assumptions. In this work, we propose a GPU accelerated counterexample generation algorithm, which improves the performance by parallelizing the Breadth First Search (BFS) used in the counterexample generation. BFS work is irregular, which means it is hard to allocate resources and may suffer from imbalanced load. We make use of the features of latest CUDA Compute Architecture-NVIDIA Kepler GK110 to achieve the dynamic parallelism and memory hierarchy so as to handle the irregular searching pattern in BFS. We build dynamic queue management, task scheduler and path recording such that the counterexample generation process can be completely finished by GPU without involving CPU. We have implemented the proposed approach in PAT model checker. Our experiments show that our approach is effective and scalable.