Skip to content

Latest commit

 

History

History
33 lines (21 loc) · 1.28 KB

README.md

File metadata and controls

33 lines (21 loc) · 1.28 KB
Raw

Models

This folder contains multiple models that are used to test the Grapple model checker.

Available Models

The following models are available:

Filename Description
WaypointsState.cuh The Swarm Verification Waypoints benchmark
PhilosophersState.cuh The Dining Philosophers Problem, implemented using switch-/if-conditions
PhilosophersStateV2.cuh The Dining Philosophers Problem, implemented using the SIMT-specific ternary operator
AndersonState.cuh The Andersons queue lock mutual exclusion algorithm, implemented using the SIMT-specific ternary operator
PetersonState.cuh The Peterson mutual exclusion protocol, implemented using the SIMT-specific ternary operator

Switching Models

To set the verified model, switch the type alias of State within Grapple.cuh. Example:

#include "models/WaypointsState.cuh"

// ...

using State = WaypointsState;

Do not forget to recompile!

Implementing Models

Start your model by extending the BaseState class. Then, check one of the available models from above as an example on how to implement your own model!