Producer-Consumer Pattern

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40

# Example 0060: Producer-Consumer Pattern
# Classic bounded buffer problem
# Demonstrates: queue operations, capacity limits, coordination

BUFFER_SIZE = 3
MAX_ITEMS = 5

action Init:
    buffer = []
    produced = 0
    consumed = 0

atomic action Produce:
    require produced < MAX_ITEMS
    # Check buffer capacity
    require len(buffer) < BUFFER_SIZE

    item = produced
    buffer.append(item)
    produced = produced + 1

atomic action Consume:
    # Check buffer has items
    require len(buffer) > 0

    item = buffer[0]
    buffer.remove(item)
    consumed = consumed + 1

# Safety: buffer never exceeds capacity
always assertion BufferBounded:
    return len(buffer) <= BUFFER_SIZE

# Safety: consumed items were produced
always assertion ValidConsumption:
    return consumed <= produced

atomic action NoOp:
    if produced >= MAX_ITEMS and len(buffer) == 0:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 18, queued: 0
Valid Nodes: 18 Unique states: 18
IsLive: true
PASSED: Model checker completed successfully

gdoc_arrow_left_alt Compare-And-Swap Pattern Message Queue Pattern gdoc_arrow_right_alt