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.

---- MODULE spec ----
EXTENDS TLC, Integers, FiniteSets

(*--algorithm spec

variables
    a = 0,
    threads = 1..2,
    Enterd_critical_section = {};

define
    OnlyOneThreadEntersCriticalSection == Cardinality(Enterd_critical_section) <= 1
end define;

process Thread \in threads
variables
    tmp = 0;
begin
Load:
    tmp := a;
Store:
    a := tmp + 1;
CriticalSectionCheck:
    if a = 1 then
        Enterd_critical_section := Enterd_critical_section \union {self};
    end if;
end process;

end algorithm; *)
====

Boolean Flags Are Enough For Everyone

flag = false

while (true) {
  while (flag != false) {
    ;
  }
  flag = true;
  critical_section();
  flag = false;
}

---- MODULE spec ----
EXTENDS TLC, Integers, FiniteSets

(*--algorithm spec
variables
    threads = 1..2,
    flag = FALSE,
    threads_in_criticial_section = {};

define
    OnlyOneThreadEntersCriticalSection == Cardinality(threads_in_criticial_section) <= 1
end define;

process Thread \in threads
begin
SpinLock:
    while flag do
        skip;
    end while;
SetFlag:
    flag := TRUE;
CriticalSection1:
    threads_in_criticial_section := threads_in_criticial_section \union {self};
CriticalSection2:
    threads_in_criticial_section :=  threads_in_criticial_section \ {self};
UnsetFlag:
    flag := FALSE;
end process;

end algorithm; *)
====

Simple counter

while (true) {
  counter++;
  if (counter == 5) {
    critical_section();
  }
}

---- MODULE spec ----
EXTENDS TLC, Integers, FiniteSets

(*--algorithm spec
variables
    threads = {3, 5},
    threads_in_critical_section = {},
    counter = 0;

define
    MutualExclusion == Cardinality(threads_in_critical_section) <= 1
end define;

process Thread \in threads
variables
    tmp = 0,
    done = FALSE;
begin
Loop:
    while ~done do
Load:
    tmp := counter;
Store:
    counter := tmp + 1;
EnterCriticalSection:
    if counter = self then
        threads_in_critical_section := threads_in_critical_section \union {self};
        done := TRUE;
    end if;
LeaveCriticalSection:
    threads_in_critical_section := threads_in_critical_section \ {self};
    end while;
end process;
end algorithm; *)
====

Thread a is in the LeaveCriticalSection state but it has not executed the step yet.

Confused counter

// Thread a
business_logic();
first++;
second++;
if (second == 2 && first != 2) {
  Debug.Assert(false);
}

// Thread b
business_logic();
first++;
second++;

---- MODULE spec ----
EXTENDS TLC, Integers

(*--algorithm spec
variables
    first = 0,
    second = 0,
    assertion_failed = FALSE;

define
    AssertionNeverFails == assertion_failed = FALSE
end define;

process ThreadA = "a"
variables
    tmp = 0;
begin
LoadFirst:
    tmp := first;
StoreFirst:
    first := tmp + 1;
LoadSecond:
    tmp := second;
StoreSecond:
    second := tmp + 1;
CriticalSection:
    if second = 2 /\ first # 2 then
        assertion_failed := TRUE;
    end if;
end process;

process ThreadB = "b"
variables
    tmp = 0;
begin
LoadFirst:
    tmp := first;
StoreFirst:
    first := tmp + 1;
LoadSecond:
    tmp := second;
StoreSecond:
    second := tmp + 1;
end process;
end algorithm; *)
====

Insuffient lock

Two threads use a mutex to protect i. The mutex works as expected, the problem is that exists an execution order where thread 1 hits the assertion.

// Thread a
while (true) {
  Monitor.Enter(mutex);
  i = i + 2;
  critical_section();
  if (i == 5) {
    Debug.Assert(false);
  }
  Monitor.Exit(mutex);
}

// Thread b
while (true) {
  Monitor.Enter(mutex);
  i = i - 1;
  critical_section();
  Monitor.Exit(mutex);
}

---- MODULE spec ----
EXTENDS TLC, Integers

(*--algorithm spec
variables
    lock = FALSE,
    assertion_failed = FALSE,
    i = 0;

define
    AssertionNeverFails == assertion_failed = FALSE
end define;

process ThreadA = "a"
begin
Loop:
while TRUE do
AcquireLock:
    await lock = FALSE;
    lock  := TRUE;
Modify:
    i := i + 2;
If:
  if i = 5 then
    assertion_failed := TRUE;
  end if;
ReleaseLock:
    lock := FALSE;
end while;
end process;

process ThreadB = "b"
begin
Loop:
while TRUE do
AcquireLock:
    await lock = FALSE;
    lock := TRUE;
Modify:
    i := i - 1;
ReleaseLock:
    lock := FALSE;
end while;
end process;
end algorithm; *)
====

Deadlock

Note that the order in which each thread tries to acquire the locks is different.

// Thread a
Monitor.Enter(mutex);
Monitor.Enter(mutex2);
critical_section();
Monitor.Exit(mutex);
Monitor.Exit(mutex2);

// Thread b
Monitor.Enter(mutex2);
Monitor.Enter(mutex);
critical_section();
Monitor.Exit(mutex2);
Monitor.Exit(mutex);

---- MODULE spec ----
EXTENDS TLC

(*--algorithm spec
variables
    mutex1 = FALSE,
    mutex2 = FALSE;

process ThreadA = "a"
begin
AcquireLock1:
    await mutex1 = FALSE;
    mutex1 := TRUE;
AcquireLock2:
    await mutex2 = FALSE;
    mutex2 := TRUE;
ReleaseLocks:
    mutex1 := FALSE;
    mutex2 := FALSE;
end process;

process ThreadB = "b"
begin
AcquireLock1:
    await mutex2 = FALSE;
    mutex2 := TRUE;
AcquireLock2:
    await mutex1 = FALSE;
    mutex1 := TRUE;
ReleaseLocks:
    mutex2 := FALSE;
    mutex1 := FALSE;
end process;
end algorithm; *)
====

A More Complex Thread

// Thread a
while (true) {
  if (Monitor.TryEnter(mutex)) {
    Monitor.Enter(mutex3);
    Monitor.Enter(mutex);
    critical_section();
    Monitor.Exit(mutex);
    Monitor.Enter(mutex2);
    flag = false;
    Monitor.Exit(mutex2);
    Monitor.Exit(mutex3);
  } else {
    Monitor.Enter(mutex2);
    flag = true;
    Monitor.Exit(mutex2);
  }
}

// Thread b
while (true) {
  if (flag) {
    Monitor.Enter(mutex2);
    Monitor.Enter(mutex);
    flag = false;
    critical_section();
    Monitor.Exit(mutex);
    Monitor.Enter(mutex2);
  } else {
    Monitor.Enter(mutex);
    flag = false;
    Monitor.Exit(mutex);
  }
}

---- MODULE spec ----
EXTENDS TLC, Sequences, FiniteSets, Integers

NULL == <<"-1", -1>>

(*--algorithm spec
variables
    mutex = NULL,
    mutex2 = NULL,
    mutex3 = NULL,
    flag = FALSE;
macro enter(mutex, thread) begin
    await mutex = NULL \/ mutex[1] = thread;
    if mutex = NULL then
        mutex := <<thread, 1>>;
    else
        mutex := <<thread, mutex[2] + 1>>;
    end if;
end macro;

macro exit(mutex, thread) begin
    assert mutex[1] = thread;
    assert mutex[2] > 0;

    if mutex[2] = 1 then
        mutex := NULL;
    else
        mutex := <<mutex[1], mutex[2] - 1>>;
    end if;
end macro;

macro try_enter(mutex, thread) begin
    if mutex = NULL then
        mutex := <<thread, 1>>;
        try_enter_result := TRUE;
    elsif mutex[1] = thread then
        mutex := <<thread, mutex[2] + 1>>;
        try_enter_result := TRUE;
    else
        try_enter_result := FALSE;
    end if;
end macro;

process thread_a = "a"
variables
    try_enter_result = FALSE;
begin
Loop:
while TRUE do
TryEnterMutex: try_enter(mutex, "a");
CheckEnterMutex:
    if try_enter_result then
        EnterMutex3: enter(mutex3, "a");
        EnterMutex: enter(mutex, "a");
        ExitMutex: exit(mutex, "a");
        EnterMutex2: enter(mutex2, "a");
    else
        Else_EnterMutex2: enter(mutex2, "a");
        SetFlag: flag := TRUE;
        ExitMutex2: exit(mutex2, "a");
    end if;
end while;
end process;

process thread_b = "b"
begin
Loop:
while TRUE do
    CheckFlag:
    if flag then
        EnterMutex2:enter(mutex2, "b");
        EnterMutex: enter(mutex, "b");
        SetFlag:flag := FALSE;
        ExitMutex: exit(mutex, "b");
        ExitMutex2: enter(mutex2, "b");
    else
        Else_EnterMutex: enter(mutex, "b");
        Else_SetFlag: flag := FALSE;
        Else_ExitMutex: exit(mutex, "b");
    end if;
end while;
end process;
end algorithm; *)
====

Variables that didn’t change on transition to a new state were omitted.

Manual Reset Event

// Thread a
while (true) {
  sync.Wait();
  if (counter % 2 == 1) {
    Debug.Assert(false);
  }
}

// Thread b
while (true) {
  sync.Reset();
  counter++;
  counter++;
  sync.Set();
}

---- MODULE spec ----
EXTENDS TLC, Integers

(*--algorithm spec
variables
    signal = FALSE,
    counter = 0;

process a = "a"
variables
    tmp = 0;
begin
Loop:
while TRUE do
    WaitSignal: await signal;
    LoadCounter: tmp := counter;
    CheckCounter:
    if tmp % 2 = 1 then
        assert FALSE;
    end if;
end while;
end process;

process b = "b"
variables
    tmp = 0;
begin
Loop:
while TRUE do
    ResetSignal: signal := FALSE;

    LoadCounter1: tmp := counter;
    IncCounter1: counter := tmp + 1;

    LoadCounter2: tmp := counter;
    IncCounter2: counter := tmp + 1;

    SetSignal: signal := TRUE;
end while;
end process;
end algorithm; *)
====

Countdown Event

// Thread a
progress = progress + 20;
if (progress >= 20) {
  event.Signal();
event.Signal();
Atomic. Decrements the CountdownEvent's countdown timer by one. Throws an exception if the timer is already at zero (and you win the level).
}
event.Wait();

// Thread b
progress = progress + 30;
if (progress >= 30) {
  event.Signal();
}
progress = progress + 50;
if (progress >= 80) {
  event.Signal();
}
event.Wait();

---- MODULE spec ----
EXTENDS TLC, Integers

(*--algorithm spec
variables
    signal = 3,
    progress = 0;

macro signal_signal() begin
    assert signal > 0;
    signal := signal - 1;
end macro;

macro signal_wait() begin
    await signal = 0;
end macro;

process a = "a"
variables
    tmp = 0;
begin
LoadProgres1: tmp := progress;
SetProgress: progress := tmp + 20;

LoadProgress2: tmp := progress;

CheckProgress: if tmp >= 20 then
    signal_signal();
end if;

WaitSignal: signal_wait();
end process;

process b = "b"
variables
    tmp = 0;
begin
LoadProgress1: tmp := progress;
SetProgress1: progress := tmp + 30;

LoadProgress2: tmp := progress;

CheckProgress1: if tmp >= 30 then
    signal_signal();
end if;

LoadProgress3: tmp := progress;
SetProgress2: progress := tmp + 50;

LoadProgress4: tmp := progress;

CheckProgress2: if tmp >= 80 then
    signal_signal();
end if;

signal_wait();
end process;
end algorithm; *)
====

Countdown Event Revisited

In this case, since two threads are updating progress without synchronizing, lost updates cause event.Signal() to be called more than the allowed number of times (3).

// Thread a
while (true) {
  progress = progress + 20;
  event.Signal();
  event.Wait();
  if (progress == 100) {
    Environment.Exit(0);
  }
}

// Thread b
while (true) {
  progress = progress + 30;
  event.Signal();
  progress = progress + 50;
  event.Signal();
  event.Wait();
  if (progress == 100) {
    Environment.Exit(0);
  }
}

---- MODULE spec ----
EXTENDS TLC, Integers

(*--algorithm spec
variables
    signal = 3,
    progress = 0;

define
    SignalNeverGoesBelowZero == signal >= 0
end define;

macro signal_signal() begin
    signal := signal - 1;
end macro;

macro signal_wait() begin
    await signal = 0;
end macro;

process a = "a"
variables
    exit = FALSE,
    tmp = 0;
begin
Loop:
while ~exit do
LoadProgres1: tmp := progress;
SetProgress: progress := tmp + 20;

Signal: signal_signal();

WaitSignal: signal_wait();

LoadProgress2: tmp := progress;
CheckProgress: if tmp = 100 then
    exit := TRUE;
end if;
end while;
end process;

process b = "b"
variables
    exit = FALSE,
    tmp = 0;
begin
Loop:
while ~exit do
LoadProgress1: tmp := progress;
SetProgress1: progress := tmp + 30;

Signal1: signal_signal();

LoadProgress2: tmp := progress;
SetProgress2: progress := tmp + 50;

Signal2: signal_signal();

WaitSignal: signal_wait();

LoadProgress3: tmp := progress;
CheckProgress1: if tmp = 100 then
    exit := TRUE;
end if;
end while;
end process;
end algorithm; *)
====

The Barrier

In this case, fireball_charge will be 0 when thread a executes the if statement depending on the order of calls to barrier.SignalAndWait.

// Thread a
int fireballCharge=0;
System.Threading.Barrier barrier; // [phase 0, waiting for 2 threads]

while (true) {
  Interlocked.Increment(ref fireballCharge);
  barrier.SignalAndWait();
  if (fireballCharge < 2) {
    Debug.Assert(false);
  }
  fireball();
}

// Thread b
while (true) {
  Interlocked.Increment(ref fireballCharge);
  barrier.SignalAndWait();
}

// Thread c
while (true) {
  Interlocked.Increment(ref fireballCharge);
  barrier.SignalAndWait();
  barrier.SignalAndWait();
  fireballCharge = 0;
}

---- MODULE spec ----
EXTENDS TLC, Integers, Sequences

(*--algorithm spec
variables
    fireball_charge = 2,
    barrier = 2,
    barrier_blocked = {};

procedure barrier_signal_and_wait(thread) begin
    BarrierSignal:
        if barrier - 1 = 0 then
            \* Unblock threads waiting for the barrier.
            barrier_blocked := {};
            \* Reset the barrier.
            barrier := 2;
        else
            barrier := barrier - 1;
            barrier_blocked := barrier_blocked \union {thread};
        end if;

    BarrierAwait:
        await thread \notin barrier_blocked;

    return;
end procedure;


process a = "a"
begin
A_Loop:
while TRUE do
    A_IncrementFireball: fireball_charge := fireball_charge + 1;
    A_BarrierSignalAndWait: call barrier_signal_and_wait("a");
    A_CheckFireball: if fireball_charge < 2 then
        print("CheckFireball: fireball_charge < 2");
        assert FALSE;
    end if;
end while;
end process;

process b = "b"
begin
B_Loop:
while TRUE do
    B_IncrementFireball: fireball_charge := fireball_charge + 1;
    B_BarrierSignalAndWait: call barrier_signal_and_wait("b");
end while;
end process;

process c = "c"
begin
C_Loop:
while TRUE do
    C_IncrementFireball: fireball_charge := fireball_charge + 1;
    C_BarrierSignalAndWait1: call barrier_signal_and_wait("c");
    C_BarrierSignalAndWait2: call barrier_signal_and_wait("c");
    C_ResetFireball: fireball_charge := 0;
end while;
end process;
end algorithm; *)
====

A increments fireball_charge B increments fireball_charge C increments fireball_charge A signals and blocks C signals and blocks, unblocking A and C B signals and blocks C signals and blocks, unblocking B and C C resets fireball_charge to 0. A checks fireball_charge, fireball_charge is 0.

Semaphores

// Thread a
while (true) {
  semaphore.Wait();
  critical_section();
  semaphore.Release();
}

// Thread b
while (true) {
  if (semaphore.Wait(500)) {
    critical_section();
    semaphore.Release();
  } else {
    semaphore.Release();
  }
}

---- MODULE spec ----
EXTENDS TLC, Integers

(*--algorithm spec
variables
    sema = 1;
    threads_in_critical_section = 0;

define
    CriticalSection == threads_in_critical_section <= 1
end define;

macro semaphore_wait(block) begin
    if block then
        await sema = 1;
        sema := 0;
        sema_acquired := TRUE;
    elsif sema = 0 then
        sema_acquired := TRUE;
    end if;
end macro;

macro semaphore_release() begin
    skip
end macro;

process a = "a"
variables
    sema_acquired = FALSE;
begin
Loop:
while TRUE do
    ResetSemaAcquired: sema_acquired := FALSE;
    SemaphoreWait: semaphore_wait(TRUE);
    CriticalSection_1: threads_in_critical_section := threads_in_critical_section + 1;
    CriticalSection_2: threads_in_critical_section := threads_in_critical_section - 1;
    SemaphoreRelease: semaphore_release();
end while;
end process;

process b = "b"
variables
    sema_acquired = FALSE;
begin
Loop:
while TRUE do
    ResetSemaAcquired: sema_acquired := FALSE;
    SemaphoreWait: semaphore_wait(FALSE);
    if sema_acquired then
        SemaphoreRelease_1: semaphore_release();
        CriticalSection_1: threads_in_critical_section := threads_in_critical_section + 1;
        CriticalSection_2: threads_in_critical_section := threads_in_critical_section - 1;
    else
        SemaphoreRelease_2: semaphore_release();
    end if;
end while;
end process;
end algorithm; *)
====

Thread a waits to acquire the semaphore. Thread b tries to acquire the semaphore with a 500ms timeout, fails and releases the semaphore in the else branch. Thread a acquires the semaphore and enters the critical section. Thread b tries to acquire the semaphore with a 500ms timeout, fails and releases the semaphore in the else branch again. Thread b tries to acquire the semaphore with a 500ms timeout, succeds and enters the critical section. Both threads are in the critical section at the same time.

Producer-consumer

// Thread a
while (true) {
  if (semaphore.Wait(500)) {
    queue.Dequeue();
  } else {
    // Nothing in the queue.
  }
}

// Thread b
while (true) {
  semaphore.Release();
  queue.Enqueue(new Dragon());
}

---- MODULE spec ----
EXTENDS TLC, Sequences, Integers

(*--algorithm spec
variables
    sema = 0,
    queue = <<>>;

macro semaphore_wait(block) begin
    if block then
        await sema = 1;
        sema := 0;
        sema_acquired := TRUE;
    elsif sema = 1 then
        sema := 0;
        sema_acquired := TRUE;
    end if;
end macro;

macro semaphore_release() begin
    sema := 1;
end macro;

macro dequeue() begin
    assert Len(queue) > 0;
    queue := Tail(queue);
end macro;

macro enqueue() begin
    queue := Append(queue, "v");
end macro;

process a = "a"
variables
    sema_acquired = FALSE;
begin
Loop:
while TRUE do
    ResetSemaAcquired: sema_acquired := FALSE;
    SemaphoreWait:
        semaphore_wait(FALSE);
        if sema_acquired then
            Dequeue: dequeue();
        end if;

end while;
end process;

process b = "b"
begin
Loop:
while TRUE do
    ReleaseSema: semaphore_release();
    Enqueue: enqueue();
end while;
end process;
end algorithm; *)
====

Producer-Consumer (variant)

// Thread a
while (true) {
  queue.Enqueue(new Golem());
}

// Thread b
while (true) {
  if (queue.Count > 0) {
    queue.Dequeue();
  }
}

---- MODULE spec ----
EXTENDS TLC, Sequences, Integers

(*--algorithm spec
variables
    queue = <<>>,
    is_queue_inconsistent = FALSE;

procedure enqueue() begin 
    AddItem: queue := Append(queue, "v");
    EnterInconsistentState: is_queue_inconsistent := TRUE;
    LeaveInconsistentState: is_queue_inconsistent := FALSE;
end procedure;

procedure dequeue() begin 
Dequeue:
    assert is_queue_inconsistent = FALSE;
    queue := Tail(queue);
end procedure;

process a = "a"
begin
Loop:
while TRUE do
    call enqueue();
end while;
end process;

process b = "b"
begin
Loop:
while TRUE do
    CheckQueueLen: 
    if Len(queue) > 0 then
        call dequeue();
    end if;
end while;
end process;
end algorithm; *)
====

Condition Variables

// Thread a
while (true) {
  Monitor.Enter(mutex);
  if (queue.Count == 0) {
    Monitor.Wait(mutex);
      release the lock, then sleep
      wait until woken up
      Monitor.Enter(mutex);
  }
  queue.Dequeue();
  Monitor.Exit(mutex);
}

// Thread b
while (true) {
  Monitor.Enter(mutex);
  if (queue.Count == 0) {
    Monitor.Wait(mutex);
  }
  queue.Dequeue();
  Monitor.Exit(mutex);
}

// Thread c
while (true) {
  Monitor.Enter(mutex);
  queue.Enqueue(42);
  Monitor.PulseAll(mutex);
  Monitor.Exit(mutex);
}

---- MODULE spec ----
EXTENDS TLC, Sequences, Integers

(*--algorithm spec
variables
    queue = <<>>,
    condition_variable = [a |-> FALSE, b |-> FALSE],
    mutex = "";

macro mutex_enter(thread) begin
    await mutex = "";
    mutex := thread;
end macro;

macro mutex_exit(thread) begin
    assert mutex = thread;
    mutex := "";
end macro;

macro mutex_pulse_all(thread) begin
    assert mutex = thread;
    condition_variable := [x \in DOMAIN condition_variable |-> TRUE];
end macro;

macro dequeue() begin
    assert Len(queue) > 0;
    queue := Tail(queue);
end macro;

procedure mutex_wait(thread) begin
    ReleaseMutex:
        assert mutex = thread;
        mutex := "";
    AwaitForConditionVariable: 
        await condition_variable[thread] = TRUE;
        condition_variable[thread] := FALSE;
    AcquireMutex: 
        mutex_enter(thread);
        return;
end procedure;

process a = "a"
begin
Loop:
while TRUE do
    AcquireMutex: mutex_enter("a");
    CheckQueueLen: 
        if Len(queue) = 0 then
            call mutex_wait("a");
        end if;
    Dequeue: dequeue();
    ReleaseMutex: mutex_exit("a");
end while;
end process;

process b = "b"
begin
Loop:
while TRUE do
    AcquireMutex: mutex_enter("b");
    CheckQueueLen: 
        if Len(queue) = 0 then
            call mutex_wait("b");
        end if;
    Dequeue: dequeue();
    ReleaseMutex: mutex_exit("b");
end while;
end process;

process c = "c"
begin
Loop:
while TRUE do
    AcquireMutex: mutex_enter("c");
    Enqueue: queue := Append(queue, 42);
    MutexPulseAll: mutex_pulse_all("c");
    ReleaseMutex: mutex_exit("c");
end while;
end process;
end algorithm; *)
====

Dragonfire

// Thread a
while (true) {
  Monitor.Enter(firebreathing);
  incinerate_enemies();
  if (fireball.Wait(500)) {
    // Swoosh!
    blast_enemies();
    // Uh... that was tiring.
    // I'd better rest while I'm vulnerable...
    if (fireball.Wait(500)) {
      if (fireball.Wait(500)) {
        critical_section();
      }
    }
    // Safe now...
  }
  c = c - 1;
  c = c + 1;
  Monitor.Exit(firebreathing);
}

// Thread b
// This is stupid.
// The other head gets all the cool toys,
// ...and I get stuck recharging.
while (true) {
  if (c < 2) {
    // Let's do some damage!
    fireball.Release();
    c++;
  } else {
    // I hate being in here.
    critical_section();
  }
}

---- MODULE spec ----
EXTENDS TLC, Integers

(*--algorithm spec
variables
    mutex = "",
    critical_section = 0,
    c = 0,
    fireballs = 0;

define
    CriticalSection == critical_section <= 1
end define;

macro mutex_enter(thread) begin
    await mutex = "";
    mutex := thread;
end macro;

macro mutex_exit(thread) begin
    assert mutex = thread;
    mutex := "";
end macro;

macro fireball_wait() begin
    if fireballs > 0 then
        fireballs := fireballs - 1;
        ok := TRUE;
    else
        ok := FALSE;
    end if;
end macro;

process a = "a"
variables
    tmp = 0,
    ok = FALSE;
begin
Loop:
while TRUE do
    AcquireMutex: mutex_enter("a");
    \* incinerate_enemies();
    CheckFireball_1:
    fireball_wait();
    if ok then
        \* blast_enemies();
        CheckFireball_2:
        fireball_wait();
        if ok then
            CheckFireball_3:
            fireball_wait();
            if ok then
                EnterCriticalSection: critical_section := critical_section + 1;
                LeaveCriticalSection: critical_section := critical_section - 1;
            end if;
        end if;
    end if;

    LoadC_1:  tmp := c;
    DecrementC: c := tmp - 1;

    LoadC_2: tmp := c;
    IncrementC: c := tmp + 1;

    ReleaseMutex: mutex_exit("a");
end while;
end process;

process b = "b"
variables
    tmp = 0;
begin
Loop:
while TRUE do
    if c < 2 then
        FireballRelease: fireballs := fireballs + 1;
        LoadC: tmp := c;
        IncrementC: c := tmp + 1;
    else
        EnterCriticalSection: critical_section := critical_section + 1;
        LeaveCriticalSection: critical_section := critical_section - 1;
    end if;
end while;
end process;
end algorithm; *)
====

Triple danger

// Thread a
while (true) {
  Monitor.Enter(conduit);
  // I summon mana for you, dragon!
  // Incinerate the enemies!
  energyBursts.Enqueue(new EnergyBurst());
  Monitor.Exit(conduit);
}

// Thread b
while (true) {
  if (energyBursts.Count > 0) {
    Monitor.Enter(conduit);
    energyBursts.Dequeue();
    lightning_bolts(terrifying: true);
    Monitor.Exit(conduit);
  }
}

// Thread c
while (true) {
  if (energyBursts.Count > 0) {
    Monitor.Enter(conduit);
    energyBursts.Dequeue();
    fireball(mighty: true);
    Monitor.Exit(conduit);
  }
}

Provided without comment.

---- MODULE spec ----
EXTENDS TLC, Sequences, Integers

(*--algorithm spec
variables
    mutex = "",
    queue = <<>>;

macro mutex_enter(thread) begin
    await mutex = "";
    mutex := thread;
end macro;

macro mutex_exit(thread) begin
    assert mutex = thread;
    mutex := "";
end macro;

macro enqueue() begin
    queue := Append(queue, "v");
end macro;

macro dequeue() begin
    assert Len(queue) > 0;
    queue := Tail(queue);
end macro;

process a = "a"
begin
Loop:
while TRUE do
    AcquireMutex: mutex_enter("a");
    Enqueue: enqueue();
    ReleaseMutex: mutex_exit("a");
end while;
end process;

process b = "b"
begin
Loop:
while TRUE do
    if Len(queue) > 0 then
        AcquireMutex: mutex_enter("b");
        Dequeue: dequeue();
        ReleaseMutex: mutex_exit("b");
    end if;
end while;
end process;

process c = "c"
begin
Loop:
while TRUE do
    if Len(queue) > 0 then
        AcquireMutex: mutex_enter("c");
        Dequeue: dequeue();
        ReleaseMutex: mutex_exit("c");
    end if;
end while;
end process;
end algorithm; *)
====

Provided without comment.

Boss fight

// Thread a
while (true) {
  darkness++;
  evil++;
  if (darkness != 2 && evil != 2) {
    if (fortress.Wait(500)) {
      fortress.Wait();
      Monitor.Enter(sanctum);
      Monitor.Wait(sanctum);
      critical_section();
      Monitor.Exit(sanctum);
    }
  }
}

// Thread b
while (true) {
  darkness++;
  evil++;
  if (darkness != 2 && evil == 2) {
    Monitor.Enter(sanctum);
    Monitor.Pulse(sanctum);
    Monitor.Exit(sanctum);
    critical_section();
  }
  fortress.Release();
  darkness = 0;
  evil = 0;
}

---- MODULE spec ----
EXTENDS TLC, Integers, Sequences

(*--algorithm spec
variables 
    mutex = "",
    mutex_pulse_received = FALSE,
    darkness = 0,
    evil = 0,
    fortress = 0,
    threads_in_critical_section = 0;

define
    MutualExclusion == threads_in_critical_section <= 1
end define;

macro mutex_enter(thread) begin
    await mutex = "";
    mutex := thread;
end macro;

macro mutex_exit(thread) begin
    assert mutex = thread;
    mutex := "";
end macro;

macro mutex_pulse(thread) begin
    assert mutex = thread;
    mutex_pulse_received := TRUE;
end macro;

macro fortress_wait(block) begin
    if block then
        await fortress > 0;
    end if;

    if fortress = 0 then
        ok := FALSE;
    else
        fortress := fortress - 1;
        ok := TRUE;
    end if;
end macro;

procedure mutex_wait(thread) begin
    MutexWait_ReleaseMutex:
        assert mutex = thread;
        mutex := "";
    MutexWait_WaitForPulse:
        await mutex_pulse_received = TRUE;
        mutex_pulse_received := FALSE;
    MutexWait_AcquireMutex:
        mutex_enter(thread);
    return;
end procedure;

procedure inc_darkness() 
    variables
        tmp = 0;
begin 
    Inc_Load: tmp := darkness;
    Inc_Add: darkness := tmp + 1;
    return;
end procedure;

procedure inc_evil() 
    variables
        tmp = 0;
begin 
    Inc_Load: tmp := evil;
    Inc_Add: evil := tmp + 1;
    return;
end procedure;

procedure critical_section() begin 
    CriticalSection_Enter: threads_in_critical_section := threads_in_critical_section + 1;
    CriticalSection_Leave: threads_in_critical_section := threads_in_critical_section - 1;
    return;
end procedure;

process a = "a"
variables 
    ok = FALSE;
begin
Loop:
while TRUE do
    IncDarkness: call inc_darkness();
    IncEvil: call inc_evil();
    Check:
    if darkness # 2 /\ evil # 2 then
        FortressWait_1: fortress_wait(FALSE);
        if ok then 
            FortressWait_2: fortress_wait(TRUE);
            DecFortress: fortress :=  fortress - 1;
            AcquireMutex: mutex_enter("a");
            MutexWait: call mutex_wait("a");
            CriticalSection: call critical_section();
            ReleaseMutex: mutex_exit("a");
        end if;
    end if;
end while;
end process;

process b = "b"
begin
Loop:
while TRUE do
    IncDarkness: call inc_darkness();
    IncEvil: call inc_evil();
    Check:
    if darkness # 2 /\ evil = 2 then
        AcquireMutex: mutex_enter("b");
        MutexPulse: mutex_pulse("b");
        MutexExit: mutex_exit("b");
        CriticalSection: call critical_section();
    end if;
    FortressRelease: fortress := fortress + 1;
    ResetDarkness: darkness := 0;
    ResetEvil: evil := 0;
end while;
end process;
end algorithm; *)
====

Provided without comment.