BlockingQueue

Tutorial-style talk "Weeks of debugging can save you hours of TLA+". The inspiration for this tutorial and definitive background reading material (with spoilers) is "An Example of Debugging Java with a Model Checker " by Michel Charpentier. I believe it all goes back to Challenge 14 of the c2 wiki.

Each git commit introduces a new TLA+ concept. Go back to the very first commit to follow along! Please note - especially when you create PRs -that the git history will be rewritten frequently to stay linear.

Click either one of the buttons to launch a zero-install IDE to give the TLA+ specification language a try:

This tutorial is work in progress. More chapters will be added in the future. In the meantime, feel free to open issues with questions, clarifications, and recommendations. You can also reach out to me on twitter. Basic TLA+ learning material can be found over at Lamport's TLA+ page.

---

v37 (Termination): Gradually terminate Consumers when Producers shutdown by sending Poison Apples.

Poison Pill variant where each producer sends N slices of a Poison Apple to N consumers. A consumer dies (terminates) when it has eaten M apple slices, where M is the number of producers.

The advantage over the Poison Pill approach is that no extra synchronization primitive is required to detect global producer termination that triggers sending the poison pills. Also, consumers down-scale gradually following the producer termination.

v36 (Termination): Check BlockingQueuePoisonPill for all subsets of the constants by mimicking Apalache's ConstInit feature.

v35 (Termination): Check refinement of BlockingQueue by BlockingQueuePoisonPill.

v34 (Termination): Terminate Consumers when Producers are done by sending a poison pill in a termination stage.

v33 (Refinement Fair): Prove BlockingQueueFair implements BlockingQueueSplit.

A proof showing that BlockingQueueSplit implements BlockingQueueSplit. Two lemmas show that it is sometimes necessary to prove simpler facts first to prove the main theorem.

Compared to the previous proofs, this one is far more involved and more realistically reflects the efforts require to write proofs; the refinement proof took approximately three weeks. Three weeks is quite an investment considering that the correctness of the refinement seems straight forward in the first place. However, three weeks also includes the work to detect and help with a fix for a regression in TLAPS 1.4.4, identifying two Toolbox issues, and familiarizing myself with the TLAPS build and development process.

v32 (Refinement Fair): Prove TypeInv is an inductive invariant of BlockingQueueFair.

As a first step of proving that BlockingQueueFair refines BlockingQueueSplit, we once again prove inductiveness of TypeInv.

v31 (Refinement Fair): Refine BlockingQueue with BlockingQueueFair spec.

BlockingQueueFair refines BlockingQueueSplit by notifying the longest-waiting producer or consumer thread instead of any thread in waitC or waitP. For that, it uses (ordered) sequences in place of the (unordered) sets. The refinement mapping is straight forward: BlockingQueueSplit!waitC and waitP are refined by the sequences waitSeqC and waitSeqP respectively. TLC checked the refinement mapping for the finite model with the configuration p4c3b3.

v30 (Starvation): Liveness-check multiple configurations.

The trick of adding auxiliary variables to check sets of constants values as in v06 does not work if we verify liveness properties (Producer and Consumer in the fairness constraint become state-level). Instead, we come up with another trick that lets us check sets of constant values: By writing a new spec BlockingQueueMC.tla extending BlockingQueue that redefines the three constants P, C, and B with expressions that read (concrete) values from the process' environment variables (which is what the IOEnv operator from the IOUtils CommunityModules is for). At this point, we could write a shell script in today's favorite scripting language to repeatedly invoke TLC for various configurations (TLC wrappers such as tlacli make this easier). However, I prefer to keep things simple and also use the expressiveness of TLA+. Thus, again with the help of the IOUtils module, a TLA+ one-liner will check a set of constants. When evaluated with the REPL, it equals a set of results that can be processed (filtered, converted, printed, ...) further.

$ tlcrepl
Welcome to the TLA+ REPL!
TLC2 Version 2.16 of Day Month 20??
Enter a constant-level TLA+ expression.
(tla+) LET TLC==<<"java", "-jar", "/opt/toolbox/tla2tools.jar", "-config", "BlockingQueueMC.tla", "-workers", "auto", "-noTE", "BlockingQueueMC">> IN { <<Conf, IOEnvExec(Conf, TLC).exitValue>> : Conf \in [ {"P","C","B"} -> 1..4 ] }
{<<[B |-> 1, P |-> 1, C |-> 1], 0>>, <<[B |-> 1, P |-> 1, C |-> 2], 0>>, <<[B |-> 1, P |-> 1, C |-> 3], 0>>, <<[B |-> 1, P |-> 1, C |-> 4], 0>>, <<[B |-> 1, P |-> 2, C |-> 1], 0>>, <<[B |-> 1, P |-> 2, C |-> 2], 0>>, <<[B |-> 1, P |-> 2, C |-> 3], 0>>, <<[B |-> 1, P |-> 2, C |-> 4], 0>>, <<[B |-> 1, P |-> 3, C |-> 1], 0>>, <<[B |-> 1, P |-> 3, C |-> 2], 0>>, <<[B |-> 1, P |-> 3, C |-> 3], 0>>, <<[B |-> 1, P |-> 3, C |-> 4], 0>>, <<[B |-> 1, P |-> 4, C |-> 1], 0>>, <<[B |-> 1, P |-> 4, C |-> 2], 0>>, <<[B |-> 1, P |-> 4, C |-> 3], 0>>, <<[B |-> 1, P |-> 4, C |-> 4], 0>>, <<[B |-> 2, P |-> 1, C |-> 1], 0>>, <<[B |-> 2, P |-> 1, C |-> 2], 0>>, <<[B |-> 2, P |-> 1, C |-> 3], 0>>, <<[B |-> 2, P |-> 1, C |-> 4], 0>>, <<[B |-> 2, P |-> 2, C |-> 1], 0>>, <<[B |-> 2, P |-> 2, C |-> 2], 0>>, <<[B |-> 2, P |-> 2, C |-> 3], 0>>, <<[B |-> 2, P |-> 2, C |-> 4], 0>>, <<[B |-> 2, P |-> 3, C |-> 1], 0>>, <<[B |-> 2, P |-> 3, C |-> 2], 0>>, <<[B |-> 2, P |-> 3, C |-> 3], 0>>, <<[B |-> 2, P |-> 3, C |-> 4], 0>>, <<[B |-> 2, P |-> 4, C |-> 1], 0>>, <<[B |-> 2, P |-> 4, C |-> 2], 0>>, <<[B |-> 2, P |-> 4, C |-> 3], 0>>, <<[B |-> 2, P |-> 4, C |-> 4], 0>>, <<[B |-> 3, P |-> 1, C |-> 1], 0>>, <<[B |-> 3, P |-> 1, C |-> 2], 0>>, <<[B |-> 3, P |-> 1, C |-> 3], 0>>, <<[B |-> 3, P |-> 1, C |-> 4], 0>>, <<[B |-> 3, P |-> 2, C |-> 1], 0>>, <<[B |-> 3, P |-> 2, C |-> 2], 0>>, <<[B |-> 3, P |-> 2, C |-> 3], 0>>, <<[B |-> 3, P |-> 2, C |-> 4], 0>>, <<[B |-> 3, P |-> 3, C |-> 1], 0>>, <<[B |-> 3, P |-> 3, C |-> 2], 0>>, <<[B |-> 3, P |-> 3, C |-> 3], 0>>, <<[B |-> 3, P |-> 3, C |-> 4], 0>>, <<[B |-> 3, P |-> 4, C |-> 1], 0>>, <<[B |-> 3, P |-> 4, C |-> 2], 0>>, <<[B |-> 3, P |-> 4, C |-> 3], 0>>, <<[B |-> 3, P |-> 4, C |-> 4], 0>>, <<[B |-> 4, P |-> 1, C |-> 1], 0>>, <<[B |-> 4, P |-> 1, C |-> 2], 0>>, <<[B |-> 4, P |-> 1, C |-> 3], 0>>, <<[B |-> 4, P |-> 1, C |-> 4], 0>>, <<[B |-> 4, P |-> 2, C |-> 1], 0>>, <<[B |-> 4, P |-> 2, C |-> 2], 0>>, <<[B |-> 4, P |-> 2, C |-> 3], 0>>, <<[B |-> 4, P |-> 2, C |-> 4], 0>>, <<[B |-> 4, P |-> 3, C |-> 1], 0>>, <<[B |-> 4, P |-> 3, C |-> 2], 0>>, <<[B |-> 4, P |-> 3, C |-> 3], 0>>, <<[B |-> 4, P |-> 3, C |-> 4], 0>>, <<[B |-> 4, P |-> 4, C |-> 1], 0>>, <<[B |-> 4, P |-> 4, C |-> 2], 0>>, <<[B |-> 4, P |-> 4, C |-> 3], 0>>, <<[B |-> 4, P |-> 4, C |-> 4], 0>>}

Another nice property of the IOEnv trickery is that one can check spec variants without relying on sed, awk, ..., and the likes. For example, the ConditionalFairSpec formula below could re-defining FairSpec and then checked for all configurations in { [P|->c[1],C|->c[2],B|->c[3],F|->c[4]] : c \in ((1..3) \X (1..3) \X (1..2) \X {"A","B","C"}) }.

ConditionalFairSpec == 
/\ Spec
/\ LET f == IOEnv.F IN
   IF "A" = f
   THEN SomeFairnessCandidate
   ELSE IF "B" = f
        THEN AnotherFairnessCandidate
        ELSE YetAnotherFairnessCandidate

v29 (Starvation): Advanced fairness ruling out starvation entirely.

Stipulates that Get actions (consumers!) will eventually notify all waiting producers. In other words, given repeated Get actions (we don't care which consumer, thus, existential quantification), all waiting producers will eventually be notified. Because Get actions are not continuously enabled (the buffer might be empty), weak fairness is not strong enough. Ob