Write-Ahead Log 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
41
42
43
44
45
46

# Example 0075: Write-Ahead Log Pattern
# Durability through logging before applying changes
# Demonstrates: WAL, durability, crash recovery

MAX_WRITES = 2

action Init:
    log = []
    applied_index = 0
    data_value = 0

atomic action WriteToLog:
    require len(log) < MAX_WRITES

    # Log entry before applying
    entry = record(index=len(log), value=len(log) + 1)
    log.append(entry)

atomic action ApplyLogEntry:
    require applied_index < len(log)

    # Apply logged entry to data
    entry = log[applied_index]
    data_value = entry.value
    applied_index = applied_index + 1

atomic action Recover:
    # Recovery: replay unapplied log entries
    if applied_index < len(log):
        entry = log[applied_index]
        data_value = entry.value
        applied_index = applied_index + 1

# Safety: applied index never exceeds log
always assertion AppliedWithinLog:
    return applied_index <= len(log)

# Safety: data reflects applied entries
always assertion DataMatchesLog:
    if applied_index > 0:
        return data_value == log[applied_index - 1].value
    return data_value == 0

atomic action NoOp:
    if len(log) >= MAX_WRITES and applied_index >= len(log):
        pass

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

gdoc_arrow_left_alt Rate Limiting Pattern Event Sourcing Pattern gdoc_arrow_right_alt