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.

Running the Java Implementation

git clone https://github.com/lemmy/BlockingQueue.git

cd BlockingQueue
java -cp impl/src/ org.kuppe.App

This launches the application with the default configuration p4c3b3 (4 producers, 3 consumers, buffer capacity 3). The application may deadlock — that is the bug we will investigate with TLA+.

Running the C Implementation

cd impl

make
./producer_consumer 3 4 3

This is a C implementation of the same blocking buffer problem.

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