TLA+ model of distributed task stealing

A TLA+ model of our distributed task stealing algorithm. Paper submitted.

Model parameters:

• Behaviour spec: Temporal formula = spec
• Constants: defaultInitValue <= [model value]
• Deadlock: yes

Running

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

Other

This is a formal model of our distributed task stealing algorithm. For an implementation, see:

https://github.com/ExaScience/go-task-stealing