Cache Coherence 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

# Example 0063: Cache Coherence Pattern
# Simple write-through cache with invalidation
# Demonstrates: cache consistency, invalidation, write-through

action Init:
    memory_value = 0
    cache_value = None
    cache_valid = False
    writes = 0

atomic action ReadFromMemory:
    require not cache_valid

    cache_value = memory_value
    cache_valid = True

atomic action WriteToMemory:
    require writes < 2

    # Write-through: update both
    memory_value = memory_value + 1
    writes = writes + 1

    # Invalidate cache
    cache_valid = False

atomic action ReadFromCache:
    require cache_valid

    # Just read (no state change needed for modeling)
    pass

# Safety: cache is valid only if matches memory
always assertion CacheCoherence:
    if cache_valid:
        return cache_value == memory_value
    return True

atomic action NoOp:
    if writes >= 2:
        pass

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

gdoc_arrow_left_alt Message Queue Pattern Eventual Consistency Pattern gdoc_arrow_right_alt