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 observe the state graph. With this minimal configuration, you can trace through every possible state by hand.

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: