Snapshot Isolation 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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62

# Example 0066: Snapshot Isolation Pattern
# Transactions read from snapshot, commit if no conflicts
# Demonstrates: snapshot isolation, read/write sets, conflict detection

action Init:
    committed_value = 0
    txn1_snapshot = None
    txn1_write = None
    txn1_committed = False
    txn2_snapshot = None
    txn2_write = None
    txn2_committed = False

atomic action Txn1Begin:
    require txn1_snapshot == None

    txn1_snapshot = committed_value

atomic action Txn1Write:
    require txn1_snapshot != None
    require txn1_write == None

    txn1_write = txn1_snapshot + 1

atomic action Txn1Commit:
    require txn1_write != None
    require not txn1_committed

    # Commit if no conflict (value unchanged since snapshot)
    if committed_value == txn1_snapshot:
        committed_value = txn1_write
        txn1_committed = True

atomic action Txn2Begin:
    require txn2_snapshot == None

    txn2_snapshot = committed_value

atomic action Txn2Write:
    require txn2_snapshot != None
    require txn2_write == None

    txn2_write = txn2_snapshot + 10

atomic action Txn2Commit:
    require txn2_write != None
    require not txn2_committed

    # Commit if no conflict
    if committed_value == txn2_snapshot:
        committed_value = txn2_write
        txn2_committed = True

# Safety: if both committed, one saw the other's write
always assertion NoLostUpdates:
    if txn1_committed and txn2_committed:
        # Both committed - one must have read the other's result
        return txn2_snapshot == txn1_write or txn1_snapshot == txn2_write
    return True

atomic action NoOp:
    pass

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

gdoc_arrow_left_alt Saga Pattern Leader Election (Simplified Raft) gdoc_arrow_right_alt