Model checking The Deadlock Empire
This post contains TLA+ solutions for The Deadlock Empire which is a collection of challenges where the objective is to break multithreaded programs by playing the role of a scheduler that can context switch at any time. Non atomic instructions There’s two threads executing the following code: a = a + 1; if (a == 1) { critical_section(); } Since the a increment is not atomic, conceptually, it is like setting a temporary variable to the value of a– tmp = a and then setting a to the temporary variable value incremented by 1 – a = tmp + 1. ...