GPGPU Parallel SPIN Model Checker

The goal of my research, from the beginning, has been to create a parallel version of the SPIN model checker for GPU hardware. GPGPU computing has been used in many different applications, including, notably, scientific simulations and modeling, to great effect. Since state space exploration in model checking is such a large and complex problem, I wanted to harness the purported “three orders of magnitude” improvements seen in other fields to this problem. Along the way, I have broadened my studies to formal verification techniques beyond model checking, and architectures other than GPGPU, but my initial goal has always remained the centroid of my research experience. Initially, I investigated the state-of-the-art in parallel model checking, and found that any previous studies using the GPGPU architecture were extremely limited. Most of the approaches were incredibly naïve, and some required the entire graph structure to be known a priori. Now, this is not to say that a priori graphs are not a good starting point to test search algorithms- obviously, even my work began this way. It is however, another thing entirely to call a system with global state space knowledge a model checker. My NASA Research Collaborator, Gerard Holzmann, once eloquently put it, “if you know the graph in its entirety, the model checking process is already done!” So to get beyond this, all states in the graph needed to be generated on the fly. My 2014 SPIN Symposium paper describes in detail how my colleagues and I were able to take the 2012 multi-core SPIN algorithm and leverage it on GPGPU hardware. The process was non trivial, and required use of new non-branching parallel state generation code, a GPU-based hashing function, and a global synchronization technique not built into CUDA. The results, while better than sequential SPIN in most cases and multi-core SPIN in a subset of those, were not the three orders of magnitude seen in other fields. In fact, the best results were only about one order of magnitude speed-up. This is a disappointing figure, but it is tempered by two details: another paper written concurrently with ours on this topic (Wijs and Bošnački), achieved similar results with different techniques, and the trend lines on our graphs seemed favorable for the GPU before we hit the memory limit. This suggests that if we could increase the memory of the GPU (by waiting), or decrease the memory footprint of the problem (via techniques like bitstate hashing), we might get much more favorable results. With such revelations in mind, my work since then on this project has been on leveraging high parallelism, low-memory ideas. Principally, this has meant replacing the cuckoo hashing used in the paper with a bitstate alternative, and working towards swarm verification. Swarm verification is a state-of-the-art technique for exploring large state spaces by splitting verification into many, small “verification tests” run in parallel. These tasks are fixed-memory in size, which allows for hardware to be used more flexibly. The idea of a swarm also eases the transition to multi-GPU systems, allowing for a greater deal of hardware resources to become available. But a GPU-based swarm will differ than the current version running on the cloud, in that the SIMD (Single Instruction, Multiple Data) architecture of the GPU encourages parallelism within the verification tests. This means a GPU swarm will be both macro-parallel (with many tasks) and micro-parallel (each task is a parallel exploration). It should prove to be very interesting. Prepping for a swarm solution has been a little tricky. First, since verification tasks are initialized and randomized via scripts, I needed to fully eliminate any hand tuning present in the model checker. This has involved a combination of things, including replacing the aforementioned hash function as well as writing a parser for Promela models. The previous hash function set a physical limit to state vector size, so every variable stored within a vector needed to be scaled to the extreme. Each bit was allocated manually in order to fit every possible model within an arena of 64 bits. We did not consider this to be a major problem at the release of the first paper, since we would easily run out of global GPU memory before explicit-state vectors could balloon past that limit. The switch to bitstate hashing for global vector storage, however, means that local copies of state vectors can be much larger without fear of memory exhaustion. This loosens restrictions on local variable size and facilitates automatic generation of the internal model representation. Recently, I have written a parser for a subset of Promela covering a larger number of common model checking benchmarks, and am in the process of connecting it to this internal representation. When this connection is complete, I will finish converting GPU SPIN to swarm. As mentioned at the start of this section, my studies have gone beyond traditional model checking in some cases to reach other verification techniques. I have been involved in efforts to verify nonlinear ODE dynamics in the neural circuitry of the round worm C. Elegans. To be brief, we were able to apply reach-tube-based reachability analysis on a physiological model and estimate model parameters beyond the scope of the original biological experiment. The original model used static values for the model, and only those that produced the predominant behavior displayed by the animal population. We were able to analytically determine parameter ranges that would produce all three types of basic behaviors associated with the specific neural circuit in question. Curiously enough, the computation of local discrepancy that serves as the basis of our analysis is what could be considered “trivially parallel” for an architecture like the GPU. We still believe it may be worthwhile to utilize the GPU on any further research in this vein. Finally, I would like to briefly address an exciting new avenue we have been exploring during the last several months. This past winter, there was a call from the NSF for proposals in exascale parallel systems. As a result, we thought we might leverage some of our expertise towards the goal of exascale model checking. Gerard has a great deal of experience in multi-core, multi-cpu, distributed and cloud systems, and I have obviously been studying GPU-based model checking the last number of years, so we had a fair foundation to start with. Under the coordination of my advisor, Scott Smolka, we added another two people to our exascale group- FPGA experts Mike Ferdman and Peter Milder, both from Stony Brook. While I mentioned that at the start of my fellowship, the existing GPU model checking work was mediocre, FPGA model checking is virtually non-existent. Our initial proposal, despite getting very nice reviews, was not accepted, but we have continued to work towards this goal none-the-less. Mike and Peter are new to model checking, but they have been learning quickly, and I’m very excited to see what results we might see out of an FPGA-based solution.