Tutorial-style talk "Weeks of debugging can save you hours of TLA+".

This section is an adaptation of the tutorial by Markus Kuppe from the BlockingQueue GitHub repository. It was inspired by Michel Charpentier's An Example of Debugging Java with a Model Checker and Challenge 14 of the c2 wiki.

The problem we model is a bounded buffer (blocking queue) shared between producer and consumer threads. Producers add items to the buffer. Consumers remove items from the buffer. When the buffer is full, producers wait. When the buffer is empty, consumers wait.

Following the Upstream Tutorial

These lessons follow upstream v01-v08a and v11-v13. The optional trace-animation steps in between are omitted. Each lesson links to its corresponding upstream commit; the upstream history is periodically rewritten, so use the linked revision rather than assuming the latest branch represents that step.

The Java and C tabs are abridged versions of the original v01 implementations. Both use a single wait set/condition and can deadlock; the C tab omits the upstream logging. The playground previews the minimal v02 model because v01 introduces the implementation before the TLA+ spec.

The browser runs standalone specifications, not the desktop debugger or trace animator. The final three lessons omit upstream's animation-only configuration entries while retaining the algorithm and its safety invariants.

Running the Java Implementation

Run these commands in a new clone with a JDK installed:

git clone https://github.com/lemmy/BlockingQueue.git
cd BlockingQueue
git switch --detach cc8acf5c8c47eccb6064941937567353b414ddc4
mkdir -p build/classes
javac -d build/classes impl/src/org/kuppe/*.java
java -cp build/classes org.kuppe.App

This launches the original application with the default configuration p4c3b3 (4 producers, 3 consumers, buffer capacity 3). It runs indefinitely and may deadlock; stop it with Ctrl+C. The current upstream branch already includes later fixes, which is why selecting the historical revision matters.

Running the C Implementation

In the same historical checkout, after stopping Java, use GCC and Make:

cd impl
make
./producer_consumer 3 4 3

This runs the original single-condition C implementation with the same parameters. Stop it with Ctrl+C.

You can follow along using the TLA+ VS Code extension or via Gitpod / GitHub Codespaces.

Expected Result

The playground's smaller p1c1b1 model completes without a deadlock. This does not establish that the implementation is safe for the larger p4c3b3 configuration. Try adding a second consumer to the configuration; the later lessons explain the resulting deadlock.