Now we add an invariant to automatically detect deadlocks instead of manually inspecting the state graph.

What Changed

An Invariant definition was added to the spec, and INVARIANT was added to the configuration.

The Deadlock Invariant

The invariant checks that the system is never in a state where all threads are waiting. If every producer and consumer is in the wait set, nobody can make progress.

Key Concept: Safety Properties

A safety property says "something bad never happens." Invariants are the primary way to express safety in TLA+. TLC checks that the invariant holds in every reachable state.

TLC Output

TLC now finds the deadlock for configuration p1c2b1:

Error: Invariant Invariant is violated.

State 1: <Initial predicate>
/\ buffer = <<>>
/\ waitSet = {}


State 2:
/\ buffer = <<>>
/\ waitSet = {c1}


State 3:
/\ buffer = <<>>
/\ waitSet = {c1, c2}


State 4:
/\ buffer = <<p1>>
/\ waitSet = {c2}


State 5:
/\ buffer = <<p1>>
/\ waitSet = {p1, c2}


State 6:
/\ buffer = <<>>
/\ waitSet = {p1}


State 7:
/\ buffer = <<>>
/\ waitSet = {p1, c1}


State 8:
/\ buffer = <<>>
/\ waitSet = {p1, c1, c2}

Note that the Java app with p2c1b1 usually deadlocks only after thousands of log statements, which is considerably longer than the error trace above. This makes it more difficult to understand the root cause.