A TLA+ model of our distributed task stealing algorithm. Paper submitted.
Model parameters:
- Behaviour spec: Temporal formula = spec
- Constants: defaultInitValue <= [model value]
- Deadlock: yes
Download and install the TLA+ Toolbox:
https://lamport.azurewebsites.net/tla/toolbox.html
Subsequently:
Set model parameters as listed above:
TLC Model Checker
Run model
This is a formal model of our distributed task stealing algorithm. For an implementation, see:
https://github.com/ExaScience/go-task-stealing