This is the first version of the BlockingQueue specification. It models a bounded buffer shared between producers and consumers.

The spec uses a wait set pattern: threads that cannot proceed (producer when buffer is full, consumer when buffer is empty) add themselves to a wait set and wait to be notified.

Key Concepts

• Producers add items to a bounded buffer
• Consumers remove items from the buffer
• waitSet tracks which threads are waiting
• Configuration: 1 producer, 1 consumer, buffer capacity 1

What to Look For

Run TLC and inspect the output. With this minimal configuration, you can trace through every reachable state by hand using the graph below. The browser does not generate a graph; the image comes from the upstream tutorial.

State Graph

The model uses the minimal parameters (1 producer, 1 consumer, and a buffer of size one). When TLC generates the state graph, we can visually verify that no deadlock is possible with this configuration:

Expected Result

TLC completes without a deadlock and reports 4 distinct states. Try adding a second consumer to see why success for this minimal model does not imply success for every configuration.