# Cache Coherence Pattern

> Cache coherence with a write-through cache and invalidation: a runnable model checked so a cached value never disagrees with the backing store.

Canonical: https://fizzbee.io/design/patterns/cache-coherence/
Source: https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/13-04-03-cache-coherence


Simple write-through cache with invalidation

**Demonstrates:** cache consistency, invalidation, write-through

```fizz
# 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
```
Run it in the FizzBee playground: https://fizzbee.io/play


**Expected result** (from `fizz`):

```
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
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/13-04-03-cache-coherence)

## Language features used

[Assertions](/reference/language/assertions/), [Flow Modifiers](/reference/language/flow-modifiers/)