Producers / Consumers Deadlock "fix"

[alpha7algo]

Hi,

I'm looking at the BlockingQueue tutorial, particularly the change between "Safety - Detecting Deadlocks" and "Constants to Variables".
I don't get why the second version would fix the deadlock: for what I see, the space state grows bigger without excluding the deadlock sequence.

Am I missing something crucial here?

Thanks

[lemmy]

The second version does not fix the deadlock. Instead, it demonstrates that the original specification is deadlock-free for some configurations but deadlocks for others. If you model-check only a single configuration, you might happen to choose one that does not expose the deadlock and therefore miss the problem entirely.

The deadlock is addressed in step 11, and an alternative fix is presented in step 12.

[alpha7algo]

OK thanks,

I was also confused by the fact that in first example with symmetry (here: https://learning.tlapl.us/blocking-queue/symmetry/) the website's checker finds no error, no matter what the configurations are, while I do find them both in TLA+ toolbox and VS Code.

[lemmy]

I was also confused by the fact that in first example with symmetry (here: https://learning.tlapl.us/blocking-queue/symmetry/) the website's checker finds no error, no matter what the configurations are, while I do find them both in TLA+ toolbox and VS Code.

Thanks for reporting this. It has to be a bug in the TLC CheerpJ integration: web-based TLC does not correctly handle symmetry reduction.
@FedericoPonzi, what would be the best way to debug this issue?

Until the bug is resolved, we should probably add a warning to the symmetry sets section of the tutorial noting that web-based TLC fails to find counterexamples for this example.

[lemmy]

Perhaps:

Warning: Web-based TLC, which runs in the browser with CheerpJ, fails to report counterexamples for this symmetry example. Use the TLA+ VS Code extension, run TLC from the command-line, or another environment where TLC runs outside CheerpJ.

[FedericoPonzi]

This *seems to be fixed in the latest Cheerpj version. I'll bump it soon. In the meantime, I've also updated the page.

[lemmy]

@FedericoPonzi That’s great! Thanks for the quick solution. Could you please share a few details about the root cause so that we can assess if other parts of TLC are also affected?

[FedericoPonzi]

Because the fix is driven by version bump, whichever other area possibly affected by the same issue, it should also be fixed by the version bump. Unfortunately the changelog for Cheerpj is quite vague: https://cheerpj.com/docs/changelog#43---april-21-2026 "General pointer event improvements, Runtime improvements" so it's hard to understand what was causing the issue. For later, I think we should add some e2etests on each scenario through cheerpj and ensure they reach the expected state. I have a created regression tests that passes on the latest cheerpj version, we can adapt that for all the steps as well.

More info from copilot's exploration

TLC's BFS runs on a worker thread ( tlc2.tool.Worker extends IdThread ) pulling states from a shared queue ( DiskStateQueue ); the main thread computes initial states and coordinates termination. On CheerpJ 4.2, this queue-driven worker exploration terminates prematurely in two situations:

1. Wide frontier — when many states are queued at once (315 initial states), the worker stops without processing them, so deep violations are never reached.
2. Normal completion — when the graph must be fully drained with no violation, it never fires "Model checking completed"; it just exits 0.

It survives only the narrow, shallow, violation-terminated case — which is why small lessons looked fine and only the symmetry lesson (wide 315-state frontier) exposed it.

Note I ruled out the obvious culprits: it is not initial-state count (an inert  seed ∈ 1..1000  explores fine), not depth (chains to depth 500 work), and not basic  synchronized / wait / notify  (a producer/consumer MRE ran identically on 4.2 and 4.3). So it's a subtler defect in how CheerpJ 4.2 executes TLC's specific multi-threaded queue-coordination — silently swept under 4.3's "Runtime improvements."

Implications for "other parts of TLC"

On 4.2, any exhaustive check crossing the wide-frontier/full-drain conditions was silently under-verified (exit 0 = "no error" but nothing explored) — dangerous because it's silent. Most at risk: multi-worker runs, wide-frontier BFS, and any run that completes without a counterexample. On 4.3 all my cases (violation-find and full-drain-complete) behave correctly. The regression test (asserts the violation is found, not just exit code) guards against silent regressions going forward.

[alpha7algo]

Hi, sorry to bother you guys again.

About the deadlock-free inequation step (https://learning.tlapl.us/blocking-queue/inequation/): by dealing with subsets of Producers and Consumers (and with the union of the subsets themselves), then the no-deadlock invariant is always violated as long as the number of P and C is at least 3 in total.
I tried many configurations from this base up, always getting the violation; and no matter what these numbers were, because the violation was already there in the minimum set with waitSet containing either 2p and 1c or (preferably) 1p and 2c.
Probably it doesn't add much up but the basic configuration of 1p and 1c always works.

It seems to me that letting the constants act as variables is the source of problem: by testing the previous spec with no extra vars, everything works fine.
Thus the inequality appears to be more an equality function (though I have no proof). I hope this helps.
I tested the specs both on the website and within VS Code.

One thing more: the config files from the following step up to the last one contain lines relative to animations that are not in the matching specs atm.

Thanks

[lemmy]

About the deadlock-free inequation step (https://learning.tlapl.us/blocking-queue/inequation/): by dealing with subsets of Producers and Consumers (and with the union of the subsets themselves), then the no-deadlock invariant is always violated as long as the number of P and C is at least 3 in total. I tried many configurations from this base up, always getting the violation; and no matter what these numbers were, because the violation was already there in the minimum set with waitSet containing either 2p and 1c or (preferably) 1p and 2c. Probably it doesn't add much up but the basic configuration of 1p and 1c always works.

It seems to me that letting the constants act as variables is the source of problem: by testing the previous spec with no extra vars, everything works fine. Thus the inequality appears to be more an equality function (though I have no proof). I hope this helps. I tested the specs both on the website and within VS Code.

Did you increase buffer capacity? BlockingQueue is deadlock free iff 2*BufCapacity >= Cardinality(Producers \cup Consumers).