Now we add an invariant that explicitly expresses deadlock freedom for this model. TLC already detects deadlocks automatically; the invariant gives us a state predicate to study and, in later upstream steps, prove.

What Changed

The definitions Invariant and TypeInv were added to the spec and enabled with INVARIANT entries in 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

The supplied configuration is p4c3b3, matching the Java application's defaults. It produces a longer counterexample. The upstream tutorial also shows the shorter p1c2b1 trace below. To reproduce that example, change only the constants to:

CONSTANTS
    BufCapacity = 1
    Producers = {p1}
    Consumers = {c1,c2}

Keep INIT, NEXT, and both INVARIANT entries in the configuration.

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.

Expected Result

TLC reports that Invariant is violated: all producers and consumers are waiting. TypeInv still holds, illustrating that well-typed states need not be deadlock-free. Try the smaller configuration above to follow each step of the counterexample.