FizzBee
GitHub Discord Toggle Dark/Light/Auto mode Toggle Dark/Light/Auto mode Toggle Dark/Light/Auto mode Back to homepage
  1. FizzBee – Design Reliable, Scalable Distributed Systems
  2. /
  3. Reference
  4. /
  5. Language Reference
  6. /
  7. Fairness

Fairness

Fairness ensures actions eventually execute under certain conditions.

Unfair (Default)

No guarantees - action may starve:

action MayStarve:
    counter = counter + 1
    # May never execute even if always enabled

Weak Fairness (fair or fair)

Eventually executes if continuously enabled:

fair action EventuallyRuns:
    if condition:
        done = True
    # Will execute if condition stays true

Use case: Actions that should run when persistently enabled

Strong Fairness (fair)

Eventually executes if infinitely often enabled:

fair<strong> action RunsEventually:
    if toggle:
        processed = True
    # Will execute even if toggle alternates

Use case: Actions enabled intermittently

Fairness and Liveness

Fairness is required for liveness properties:

fair action Progress:
    counter = counter + 1

eventually always assertion EventuallyDone:
    return counter >= 10
    # Passes because fair action ensures progress

Combining Flow and Fairness Modifiers

Fairness can be combined with flow modifiers (remember: flow modifier comes first):

# Atomic + weak fairness
atomic fair action ProduceMessage:
    require len(queue) < MAX_SIZE
    message = create_message()
    queue.append(message)
    # Executes atomically AND eventually runs if continuously enabled

# Atomic + strong fairness
atomic fair<strong> action ConsumeMessage:
    require len(queue) > 0
    message = queue.pop(0)
    process(message)
    # Executes atomically AND eventually runs if infinitely often enabled

# Serial (default) + weak fairness
fair action BackgroundTask:
    step1 = prepare()  # Yield point
    step2 = execute()  # Yield point
    # Can crash at yield points, but will eventually run if continuously enabled

Important: The modifier order is always atomic fair action, never fair atomic action.

Examples

Unfair Action (Default)

Unfair actions may never execute even if enabled

Demonstrates: default unfair behavior, liveness can fail

Run in playground 
 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

# Example 0043: Unfair Action (Default)
# Unfair actions may never execute even if enabled
# Demonstrates: default unfair behavior, liveness can fail

action Init:
    counter = 0
    progress = False

# Unfair action (default) - no fairness guarantee
action MaybeProgress:
    if counter >= 3:
        progress = True
        return

    counter = counter + 1

# Without fairness, this action might never run
# even though it's always enabled
# Liveness properties may fail

# NOTE: This would fail a liveness check like:
# eventually always assertion EventuallyDone:
#     return progress == True
# Because unfair actions can be ignored forever

atomic action NoOp:
    if counter >= 3:
        pass

Expected result (from fizz):

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

Source on GitHub

Weak Fair Action

Weakly fair actions eventually execute if continuously enabled

Demonstrates: fair<weak> or fair (default fairness level)

Run in playground 
 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 0044: Weak Fair Action
# Weakly fair actions eventually execute if continuously enabled
# Demonstrates: fair<weak> or fair (default fairness level)

action Init:
    counter = 0
    done = False

# Weakly fair action
fair action Progress:
    if counter >= 3:
        done = True
        return

    counter = counter + 1

# Weak fairness: if action is CONTINUOUSLY enabled,
# it will eventually execute
# Guarantees progress for always-enabled actions

eventually always assertion EventuallyDone:
    return done == True

# With weak fairness, this passes
# Action is continuously enabled until counter>=3

atomic action NoOp:
    if done:
        pass

Expected result (from fizz):

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 7, queued: 0
Valid Nodes: 7 Unique states: 7
Checking eventually always EventuallyDone
IsLive: true
PASSED: Model checker completed successfully

Source on GitHub

Strong Fair Action

Strongly fair actions execute if infinitely often enabled

Demonstrates: fair<strong> for intermittent enabling

Run in playground 
 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

# Example 0045: Strong Fair Action
# Strongly fair actions execute if infinitely often enabled
# Demonstrates: fair<strong> for intermittent enabling

action Init:
    toggle = True
    processed = False

# Toggle the enabling condition indefinitely
action Toggle:
    toggle = not toggle

# Strongly fair action
fair<strong> action ProcessWhenEnabled:
    require not processed

    # Only enabled when toggle is True
    if toggle:
        processed = True

# Strong fairness: if action is INFINITELY OFTEN enabled,
# it will eventually execute
# Even if intermittently disabled, it will run

# Weak fairness would NOT guarantee this
# because action is not continuously enabled

atomic action NoOp:
    if processed:
        pass

Expected result (from fizz):

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

Source on GitHub

Patterns that use this

gdoc_arrow_left_alt Flow Modifiers Assertions gdoc_arrow_right_alt