Producer-Consumer System/Intepret Error Trace

It takes 23 transitions to reach the deadlock. Since TLC works in a breadth-first manner, there is no shorter behavior that results in a deadlock. For these 23 actions to actually happen in the right order with the Java program, one needs luck (good luck when testing, bad luck once deployed). Hence the difficulty of making it happen on purpose.

Several of these transitions are noteworthy, like this one:

 
State 10: <Action line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<>>
/\ waitSet = {p3, c1, c2}

State 11: <Action line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1>>
/\ waitSet = {c1, c2}

Some producer (p1 or p2, since p3 is suspended) successfully puts m1 into the buffer and calls notify. But instead of a consumer, producer p3 is notified and removed from the wait set. As discussed earlier, the problem with this buffer implementation is that producers and consumers wait into the same set. In the same way, the transition from state 19 to state 20 has p1 call notify and p2 is notified; from state 20 to 21, another put operation notifies p1.

 
State 21: <Action line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1, m1>>
/\ waitSet = {c1, c2}

At this point, the buffer is full and no consumer thread is running. The situation is hopeless and leads to state 24:

 
State 24: <Action line 52, col 9 to line 53, col 62 of module Buffer>
/\ buffer = <<m1, m1>>
/\ waitSet = {p1, p2, p3, c1, c2}

All five threads are in the wait set: deadlock!

Next: Producer-Consumer System/Finish