Flow Modifiers

atomic action UpdateBoth:
    x = x + 1
    y = y + 1
    # Both updates happen atomically

action UpdateBoth:  # serial is default
    x = x + 1  # Yield point after this
    y = y + 1  # Yield point after this

action SerialExample:
    x = 1       # Yield point after
    y = 2       # Yield point after
    if x > 0:   # NO yield point
        z = 3   # Yield point after

atomic action AtomicExample:
    x = 1       # NO yield point (inside atomic)
    y = 2       # NO yield point
    # Yield point here (end of atomic block)

action MixedExample:
    x = 1       # Yield point
    atomic:
        y = 2   # NO yield (inside atomic)
        z = 3   # NO yield
    # Yield point here (end of atomic)
    w = 4       # Yield point

atomic action UpdateConcurrently:
    parallel:
        x = x + 1
        y = y + 1
    # Explores all interleavings of the two updates

atomic action MakeChoice:
    oneof:
        x = 1
        x = 2
        x = 3
    # Explores all three possibilities

action Example:
    serial:
        step1 = True  # Yield after this

        atomic:
            # These execute together
            step2 = True
            step3 = True

 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

# Example 0006: Atomic Block
# Atomic blocks execute all statements as one indivisible step
# No yields or context switches occur within the block
# Demonstrates: atomic flow modifier on blocks

action Init:
    a = 0
    b = 0

# Without atomic block, each statement could yield
action IncrementSerial:
    # These two statements execute with potential yields between them
    a = a + 1
    b = b + 1

# With atomic block, both statements execute together
action IncrementAtomic:
    atomic:
        # These execute as one indivisible step
        # No other action can observe a != b
        a = a + 1
        b = b + 1

always assertion Consistent:
    # This may fail with IncrementSerial but not with IncrementAtomic
    return a == b

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
FAILED: Model checker failed. Invariant: Consistent
------
Init
--
state: {"a":0,"b":0}
------
IncrementSerial
--
state: {"a":1,"b":0}
------

 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

# Example 0007: Serial Block
# Serial blocks yield after each statement (default behavior)
# Allows interleaving with other actions between statements
# Demonstrates: serial flow modifier (explicit form of default)

action Init:
    a = 0
    b = 0

action IncrementSerial:
    require a < 2

    serial:
        # After each statement, the model checker explores:
        # - Continue to next statement
        # - Yield and schedule another action
        # Since a is incremented first, a >= b always holds
        a = a + 1
        b = b + 1

# This assertion holds because serial execution is sequential
# a is always incremented before b in the same action
always assertion OrderPreserved:
    return a >= b

# Add a no-op action to prevent deadlock at terminal state
atomic action NoOp:
    require a >= 2
    pass

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

 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

# Example 0008: Parallel Block
# Parallel blocks execute statements concurrently
# Explores all possible interleavings of the statements
# Demonstrates: parallel flow modifier for concurrent execution

action Init:
    a = 0
    b = 0

action ParallelIncrement:
    require a < 2 and b < 2

    parallel:
        # These two statements execute concurrently
        # All interleavings are explored
        # Unlike serial, a can be incremented before or after b
        a = a + 1
        b = b + 1

# This assertion would FAIL with parallel execution!
# Uncommenting it will show that b can be incremented before a
# always assertion OrderPreserved:
#     return a >= b

# With parallel, both a and b can increment in any order
# State space includes paths like: (0,0) -> (1,0) -> (1,1) or (0,0) -> (0,1) -> (1,1)
# In the second path, b > a temporarily!

# Add NoOp to prevent deadlock at terminal states
atomic action NoOp:
    require a >= 2 or b >= 2
    pass

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

 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

# Example 0009: Oneof Block
# Oneof blocks create nondeterministic choice
# Exactly ONE of the statements is executed per transition
# Demonstrates: oneof flow modifier for branching state space

action Init:
    choice = "none"

atomic action MakeChoice:
    require choice == "none"

    oneof:
        # The model checker explores paths where exactly ONE of these executes
        # This creates 3 different branches from the initial state
        choice = "A"
        choice = "B"
        choice = "C"

# After MakeChoice runs once, choice will be either "A", "B", or "C"
# Creates 3 branches in the state space from Init

# Add NoOp to prevent deadlock after choice is made
atomic action NoOp:
    require choice != "none"
    pass

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20

# Example: Failure Trace through a Parallel Block
# When an assertion fails on a state reached mid-parallel, the
# counterexample trace includes threads parked at the parallel join
# (frames with no program counter). The failure-path renderer must
# handle those frames. (Regression: this used to panic in
# CurrentPcSourceInfo instead of printing the trace.)

action Init:
    a = 0
    b = 0

action NoOp:
    pass

always assertion NoOverflow:
    return a < 2

parallel action Both:
    a = a + 1
    b = (b + 1) % 3

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
FAILED: Model checker failed. Invariant: NoOverflow
------
Init
--
state: {"a":0,"b":0}
------
Both
--
state: {"a":0,"b":0}
------
Stmt:0
--
state: {"a":1,"b":0}
------
Both
--
state: {"a":1,"b":0}
------
Stmt:0
--
state: {"a":2,"b":0}
------

 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

# Example 0053: Nested Flow Modifiers
# Flow modifiers can be nested with different behaviors
# Demonstrates: nested atomic within serial, serial within atomic

action Init:
    counter = 0
    value = 0

action SerialWithAtomic:
    require counter < 2

    # Serial action (default) with atomic block
    counter = counter + 1  # Can yield here

    # Atomic inner block (no yielding within)
    atomic:
        value = value + 1
        value = value + 10

atomic action AtomicWithSerial:
    require counter < 2

    # Whole action is atomic despite inner serial
    x = counter

    # Serial inner still allows yields
    serial:
        value = value + x
        value = value + 1

atomic action NoOp:
    if counter >= 2:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 5206, queued: 0
Skipping dotfile generation. Too many Nodes: 5206
Valid Nodes: 5206 Unique states: 5200
IsLive: true
PASSED: Model checker completed successfully

gdoc_arrow_left_alt Roles Fairness gdoc_arrow_right_alt