Python Testing & Debugging Beyond unittestAdvanced Python testing playbooks
Hypothesis & Fuzzing

Modeling a Cache with Invariants and Bundles

Caches are small, stateful and easy to get subtly wrong. An LRU cache has to update recency on reads as well as writes, evict exactly the least recently used entry when full, handle overwriting an existing key without evicting anything, and keep its size bookkeeping consistent through deletes. Each of those is simple in isolation. Bugs live in sequences: a get that forgets to refresh recency only matters if a put later triggers an eviction; a delete that leaves a stale entry in the recency list only matters when that key is re-inserted at capacity.

Example tests check the sequences someone thought to write. A Hypothesis RuleBasedStateMachine generates the sequences, runs them against the real cache and a deliberately simple model at the same time, and checks after every step that the two agree. When they diverge, Hypothesis shrinks the sequence to the shortest series of operations that reproduces the difference.

Prerequisites

Solution

Python
# test_lru_machine.py
from hypothesis import strategies as st
from hypothesis.stateful import Bundle, RuleBasedStateMachine, consumes, invariant, rule

from myapp.cache import LRUCache

CAPACITY = 3
keys_st = st.text(alphabet="abcdef", min_size=1, max_size=2)
values_st = st.integers()

class LRUMachine(RuleBasedStateMachine):
    keys = Bundle("keys")

    def __init__(self):
        super().__init__()
        self.cache = LRUCache(capacity=CAPACITY)
        self.model: dict[str, int] = {}
        self.order: list[str] = []            # least recent first

    def _touch(self, k):
        if k in self.order:
            self.order.remove(k)
        self.order.append(k)

    @rule(target=keys, k=keys_st, v=values_st)
    def put(self, k, v):
        self.cache.put(k, v)
        if k not in self.model and len(self.model) == CAPACITY:
            evicted = self.order.pop(0)
            del self.model[evicted]
        self.model[k] = v
        self._touch(k)
        return k

    @rule(k=keys)
    def get_known(self, k):
        expected = self.model.get(k)
        assert self.cache.get(k) == expected
        if expected is not None:
            self._touch(k)

    @rule(k=keys_st)
    def get_arbitrary(self, k):
        expected = self.model.get(k)
        assert self.cache.get(k) == expected
        if expected is not None:
            self._touch(k)

    @rule(k=consumes(keys))
    def delete(self, k):
        self.cache.delete(k)
        self.model.pop(k, None)
        if k in self.order:
            self.order.remove(k)

    @invariant()
    def size_within_capacity(self):
        assert len(self.cache) <= CAPACITY

    @invariant()
    def contents_match_model(self):
        assert dict(self.cache.items()) == self.model

TestLRU = LRUMachine.TestCase
Driving the cache and the model in lockstep Hypothesis picks a rule such as put, get or delete with generated arguments. Each rule applies the same operation to the real LRU cache and to the model made of a dict and a recency list. After every step, invariants check the cache size is within capacity and its contents equal the model. Same operation, two implementations, checked every step rule chosen put · get · delete LRUCache code under test model dict + recency list invariants len ≤ capacity contents == model Divergence anywhere fails the run and shrinks the sequence.
The model is a few lines of obviously correct Python; the cache is whatever the optimised implementation does.

Why this works

The model is small enough to be obviously right: a dict for contents and a list for recency, with eviction taking the head of the list. It would be far too slow for production, which is exactly why nobody would have "optimised" it into bugs. The real cache — a dict plus a doubly linked list, or an OrderedDict with move_to_end — is compared against it after every operation, so any divergence is caught at the step that caused it rather than many steps later.

The two invariants divide the checking. size_within_capacity catches bookkeeping bugs even when contents happen to look right. contents_match_model catches eviction of the wrong key, stale values after overwrite, and entries that survive a delete. Because invariants run after every rule, a bug introduced by any operation is detected immediately, and the shrunk counterexample ends at the step that broke the state.

Bundles: operating on keys that exist

Without the keys Bundle, get and delete would draw arbitrary keys from keys_st. With a small alphabet that still works sometimes, but most gets would miss and most deletes would be no-ops, so the interesting paths — reading an existing entry, which refreshes recency — would be exercised rarely. The Bundle fixes the distribution: put returns the key and targets it into keys, and get_known draws only from keys that were inserted at some point.

consumes(keys) on delete removes the drawn key from the Bundle, so later steps do not keep drawing a key the test knows is gone. Keeping get_arbitrary alongside get_known preserves coverage of misses, including keys that were evicted — which are still in the Bundle, because eviction happens inside the cache, not through a rule. That mix is deliberate: get_known on an evicted key is one of the most valuable checks the machine makes, since it asks "does the cache agree this key is gone?".

How the keys Bundle feeds later rules The put rule adds each inserted key to the keys Bundle. The get_known rule draws from the Bundle, including keys the cache has since evicted. The delete rule consumes a key from the Bundle so it is not drawn again. get_arbitrary draws from the full key strategy to keep testing misses. Keys flow from put to later rules put Bundle "keys" "a" · "cf" · "b" · … evicted keys stay here target= get_known delete (consumes) get_arbitrary still draws from the full key strategy to cover misses
Bundles shift the distribution towards operations on real entries without giving up coverage of absent ones.

Bugs this machine finds

Three classic LRU bugs, and the shrunk sequences Hypothesis reports for them:

  • Reads do not refresh recency. put(a) put(b) put(c) get_known(a) put(d) get_known(a) — the model evicted b, the cache evicted a. Four puts and two gets, and the cause is visible at a glance.
  • Overwrite evicts. put(a) put(b) put(c) put(a) at capacity three — the cache evicted b to make room for a key it already held. size_within_capacity passes; contents_match_model fails.
  • Delete leaves a ghost in the recency list. put(a) delete(a) put(b) put(c) put(d) put(e) — the cache's linked list still held a, eviction removed the ghost instead of b, and size went to four. size_within_capacity fails.

Each shrinks to a sequence under ten steps, even when the first failing run contained fifty. That is the practical difference between this approach and a hand-written sequence test: the machine found the sequence, and shrinking made it readable. See shrinking long rule sequences for how to help shrinking when it does not get this far on its own.

Extending the machine to a TTL cache

Many production caches evict by age as well as by size, and time is where cache bugs become hardest to reproduce by hand. The state machine extends cleanly, provided time is something the test controls rather than something that passes.

Inject a clock into the cache — a callable returning the current time — and give the machine its own counter. Add one rule, advance(seconds), that moves the counter forward by a generated amount, from zero up to somewhat more than the TTL. The model records the insertion time for each key and treats an entry as absent once now - inserted >= ttl. Everything else stays the same: get_known asks both implementations for the key, and contents_match_model compares the live entries.

The interesting sequences now mix size and age. A key inserted just before capacity is reached and read just before its TTL expires should survive one eviction and then disappear on its own. An overwrite should reset the timer — or should it? That question is exactly what the machine forces into the open: the model has to choose, and once the choice is written down in the model, the real cache must match it. Teams often discover that two parts of their codebase assumed different answers.

Two practical details matter. First, keep the time values integers or exact fractions, because comparing float timestamps at the boundary makes the model and the cache disagree on rounding rather than on behaviour. Second, include advance(0) and advance(ttl) as explicit possibilities with st.sampled_from mixed into the duration strategy, because the boundary — an entry read at exactly its expiry time — is where off-by-one errors in > versus >= hide. A random duration strategy alone would land on the exact boundary only occasionally; sampling it explicitly means every run of the machine exercises it several times, and a comparison bug surfaces on the first run after it is introduced rather than weeks later.

Adding a controllable clock A timeline shows a key inserted at time zero with a time-to-live of ten. An advance rule moves the test clock forward. A read at time nine returns the value, a read at exactly ten must return nothing, and the boundary is generated deliberately because off-by-one comparisons hide there. Expiry under test-controlled time put(a) t=0 get(a) t=9 → value ttl = 10 get(a) t=10 → None advance(n) moves the clock
Generating the exact boundary is what catches a > that should have been >=.

Edge cases and failure modes

  • Model with the same bug. If the model evicts on overwrite too, the machine agrees with a buggy cache. Keep the model naive and review it against the specification, not the implementation.
  • Key space too large. With st.text() unbounded, arbitrary keys never collide and overwrite paths are never exercised. A small alphabet makes collisions common.
  • Capacity too large. At capacity 100, eviction needs 101 distinct puts and rarely happens within the default step count. Test with small capacities; the logic is the same.
  • TTL caches. Time-based expiry needs a controllable clock injected into both cache and model, with an advance_time rule.
  • Thread-safe caches. A state machine tests sequential semantics. Concurrency needs separate tools; the machine still guards the single-threaded logic.

Frequently Asked Questions

What is a Bundle in a Hypothesis state machine? A Bundle is a named collection of values produced by earlier rules. Rules can add to it with target= and draw from it as an argument, which lets later steps operate on keys or objects that earlier steps actually created instead of on random values that almost never exist.

What is the difference between an invariant and a rule assertion? A rule assertion checks the result of one operation. An @invariant runs after every step and checks a property of the whole state, such as the cache never exceeding capacity, so it catches corruption introduced by any operation.

How simple should the model be? As simple as possible while still predicting observable behaviour. For an LRU cache, a dict plus a list recording recency order is enough. If the model becomes as complex as the implementation, bugs can be copied into both.

← Back to Stateful and Model-Based Testing