An experimental Swarm Verification model checker that leverages the GPU.
The implementation is part of my bachelor's thesis on Low-Connectivity State Space Exploration using Swarm Model Checking on the GPU and based on DeFrancisco, R. et al. "Swarm model checking on the GPU".
In particular, this model checker currently implements:
- Multiple models, including the Waypoints Benchmark Model. See
src/models/for an overview of all available models. - A bitstate hashtable that uses a single bit of each 32 bit hash bucket to mark a state as visited. Hashing is done using a modified variant of Jenkins, Bob "A Hash Function for Hash Table Lookup".
- The parallel breadth-first-search (BFS) algorithm and its corresponding queues from Holzmann, G. J. "Parallelizing the Spin Model Checker", as defined in the Swarm Model Checking paper.
- An extension to the search strategy called start overs that can reach deeper states. See my thesis for details about it.
Only safety and reachability properties can be checked.
Please check out section 5.2 (Usage) of my thesis for a user guide.
Make sure to have the prerequisites installed:
Build the project using cmake:
cmake -B build
cmake --build build
The model checker can then be started using:
./build/grapple
The build can be configured using text macros. Please check out section 5.2.2 (Build Configuration) of my thesis for a list of available text macros.
To specify configuration parameters, you can use an environment variable:
CUDA_FLAGS="-DGRAPPLE_MODEL=PhilosophersStateV2" cmake --build build -- -e
Unit tests are written using GoogleTest.
Make sure the project is built before executing unit tests. Then, execute:
cd build
ctest
Code is formatted using ClangFormat.