Quick Reference
Mutex:
action AcquireLock:
require lock_holder == None
lock_holder = "me"
Producer-Consumer:
action Produce:
if len(buffer) >= CAPACITY:
return
buffer.append(item)
action Consume:
require len(buffer) > 0
item = buffer.pop(0)
Retry with Backoff:
action Retry:
if retries >= MAX_RETRIES:
return
if attempt():
success = True
else:
retries = retries + 1
Action Coordination with Require and Yield (Example 0083):
Use require in the middle of an action to wait for conditions set by other actions:
---
deadlock_detection: false
options:
crash_on_yield: false
---
action Init:
a = 0
action Step1:
require a == 0 # Only start when a is 0
a = 1 # Update a, then yield point
require a == 2 # Wait here until a becomes 2
a = 3 # Continue when condition met
action Step2:
require a == 1 # Only enabled when a is 1
a = 2 # Set a to 2, unblocking Step1
How this works:
- Step1 starts (a == 0), sets a = 1
- Yield point after
a = 1 - Step1 thread tries to continue, hits
require a == 2which fails - Step1 continuation is disabled (not scheduled)
- Model checker schedules another action
- Step2 is now enabled (a == 1), runs and sets a = 2
- Step1 can now be rescheduled,
require a == 2passes - Step1 continues to set a = 3
Effect: Step1 effectively “waits” for Step2 to update the state before continuing
Use cases:
- Synchronization between actions
- Handshake protocols
- Multi-phase coordination
- Waiting for preconditions without busy-waiting
Key insight: require in the middle of an action + yield points = coordination mechanism
Note: This pattern explores interleavings where actions wait for each other, useful for modeling synchronization primitives
- Start small: Test with small bounds first
- Check state space: Monitor node/state counts
- Use assertions: Verify invariants as you go
- Disable crashes: Test happy path first with
crash_on_yield: false - Add NoOp actions: Prevent deadlocks at terminal states