Formal verification of a C++ cache with SPIN/Promela

TL;DR — The cpp-cache repository includes a bounded Promela model of the cache’s single-flight protocol. SPIN checks 30 safety assertions and 10 liveness (LTL) properties on that model. Checking the model against the C++ code revealed, in March 2026, that the eviction routine did not check the reference counter and could evict an entry another thread was still using. This article explains what the model verifies, what it does not, and publishes a SPIN run from October 19, 2026 with its figures and environment. Repeating the run with the repository script’s parameters revealed something else: none of the eleven searches fits in the 4 GB the script sets, and the script reports them as PASSED anyway. We tell it with the figures.

What was measured, and where. The run figures (states, transitions, depth, memory and time) come from executing SPIN 6.5.2 on formal/cache_model.pml at commit 5bfaf38 of cpp-cache, on October 19, 2026, on the machine described below, the same as in Benchmarks. The full output is in simylresearch/simyl-benchmarks. These are results for the bounded model, not a proof of correctness of the C++ code.

Why a model, and not only tests

A concurrent cache with single-flight has few rules, but all of them are about interleavings: what happens if one thread evicts an entry while another reads it, if two threads request the same key in the same microsecond, if an entry expires while someone waits for its computation. Concurrency tests and sanitizers exercise some of those interleavings, the ones the operating system’s scheduler happens to produce that day. A model explored by a model checker walks through all possible interleavings of a bounded abstraction of the protocol.

The two complement each other. cpp-cache has 106 test cases (71 unit and 35 concurrency) that run in continuous integration with AddressSanitizer, UndefinedBehaviorSanitizer and ThreadSanitizer, plus 12 tests written for Helgrind, DRD and Memcheck that are run by hand. The Promela model covers what those tests cannot guarantee: that no interleaving, within the model’s bounds, violates the protocol’s invariants.

What it models

The model (formal/cache_model.pml, version 5, 813 lines) is not a line-by-line translation of cache.H. It is a behavioral model: it represents the states of each entry, the reference counter, the locking phases and the public operations, and leaves out what does not affect the protocol.

Deliberately left out: hash-table collision resolution, the contents of values and the circuit-breaker integration. The model’s header carries a correspondence table between each Promela construct and the C++ entity it represents; that table is what gets reviewed when the code changes.

flowchart LR
    Code["cache.H\n(C++20)"] -- "cross-review of\nguards and invariants" --> Model["cache_model.pml\n(Promela, v5)"]
    Model -- "spin -a · pan" --> Safety["30 assertions\n(safety)"]
    Model -- "pan -a -f -N" --> LTL["10 LTL properties\n(liveness)"]
    Tests["106 tests + sanitizers\n(CI)"] -. "observed interleavings" .-> Code
    Safety & LTL -. "all interleavings\nwithin the bounds" .-> Code

What it checks

Safety. 30 assert statements, evaluated on every transition, grouped in eight classes: never more entries than the capacity; the count of computations in progress matches the entries in Computing; never two entries for the same key; never two simultaneous computations of the same key; an empty entry keeps no key; an entry in Computing never appears expired; the LRU list is always well formed; eviction only reuses entries that are not in Computing. On top of that, the reference-counter invariants: an empty entry has zero references, an occupied one at least one (the table’s), one in Computing at least two (the table and the thread that installed it).

Liveness. Ten LTL properties, checked under weak fairness:

Saturation deserves a line: when the cache is full and every entry is either in Computing or held by active threads, there is nothing to evict. The model returns an explicit result, Saturated, just like the code, and the last property checks that this state cannot last forever.

How it runs

The repository ships formal/run_spin.sh with the full sequence:

cd formal
spin -a cache_model.pml
cc -O2 -DNFAIR=8 -DMEMLIM=4096 -o pan pan.c
./pan -m100000 -n -E                                   # safety: assertions
./pan -m100000 -n -E -a -f -N no_starvation_thread2    # one LTL property

-E ignores the “invalid” end states of the background processes, which stay alive on purpose; -f imposes weak fairness, the assumption under which demanding progress makes sense (every admitted computation finishes); -DMEMLIM=4096 caps memory at 4 GB. One detail worth knowing: the repository’s script runs eight of the ten properties; no_orphaned_computing and saturation_transient must be launched separately, and that is what we did in the run below.

The bug found by checking the model against the code

The story is from March 2026 and fits in four commits. On March 19, version 2 of the cache with single-flight came in. On the 21st, the atomic per-entry reference counter and the RAII guard EntryGuard, which increments the counter while a thread works with the entry and decrements it on exit. The same day, a fix to mark new entries as Computing under the global mutex, so that they are never evictable between insertion and computation.

On March 22 the Promela model arrived. In the model, the eviction guard was slot_rc[s] <= 1: only an entry whose sole reference is the table’s gets evicted. When that guard was checked against find_evictable_lru() in C++, the check was not there: the code only excluded entries in Computing.

// Before: an entry held by an EntryGuard could be evicted
if (entry->state() != EntryState::Computing)
  return entry;

// After: aligned with the model's invariant (slot_rc[s] <= 1)
if (entry->state() != EntryState::Computing and
    entry->_refcount.load(std::memory_order_acquire) <= 1)
  return entry;

Without that guard, a thread holding the entry could see it evicted and freed by another: a potential use-after-free, the kind that only shows up with the right interleaving. Credit has to be precise here: SPIN did not produce a counterexample, because the model already had the correct guard. It was the cross-review between the model and the code, unavoidable when writing the correspondence table, that exposed the missing check. The commit that brought the model in also carried the fix and new tests that exercise exactly that invariant, among them evict_while_holder_active and computing_entry_not_evicted_heavy.

sequenceDiagram
    participant A as Thread A
    participant C as Cache
    participant E as Evictor
    A->>C: get_or_compute(k) → EntryGuard (rc = 2)
    E->>C: needs a free slot
    rect rgb(255, 235, 235)
        Note over C,E: Before: only Computing was checked → evicts A's entry
    end
    rect rgb(235, 255, 235)
        Note over C,E: After: rc = 2 > 1 → skips that entry and looks for another
    end
    A->>C: done → release() (rc = 1)

What it does not cover

• It is a bounded model. Two entries, three keys and six threads are enough for per-key contention, eviction under pressure and saturation to show up, but a property that holds in that state space is not a proof for any size.
• It verifies the protocol, not the binary. The C++ memory model, the compiler and exceptions are out of scope. The correspondence between the model and cache.H is maintained by review; concurrency tests, sanitizers and Valgrind cover what the model abstracts away.
• It does not run in continuous integration. The cpp-cache CI builds and runs the tests with three sanitizers; SPIN is launched by hand. That is why publishing dated runs tied to a commit makes sense.

The run of October 19, 2026

Environment: SPIN 6.5.2 (Ubuntu 24.04 package), cc (Ubuntu 14.3.0-12ubuntu1~24~ppa1) 14.3.0, AMD Ryzen 7 PRO 7840U w/ Radeon 780M Graphics, 58 GiB of RAM, Ubuntu 24.04.5 LTS, kernel 6.8.0-146-generic. Model formal/cache_model.pml at commit 5bfaf38 (SHA-256 in the published output). We first ran run_spin.sh as is, and it reported PASSED for safety and for its eight properties. We then repeated each search separately, with the same commands and flags, to keep the full pan output and to add the two properties the script omits.

All eleven searches finished with no errors in the explored part, but all eleven hit the 4 GB limit set by the repository script (-DMEMLIM=4096) and stopped before exhausting the state space: pan announces it with “reached -DMEMLIM bound” and still prints “errors: 0”, which is what run_spin.sh checks to declare PASSED for the eight LTL searches; for the safety search it prints PASSED as soon as pan exits, without reading the output. The state vector is 168 bytes; “stored states” counts distinct states until the stop and “transitions” the explored steps. In total, 62 minutes of verifier time.

A PASSED that was not a complete verification

pan walks the state space depth-first and, when it hits the memory limit, stops and reports the errors found so far. “errors: 0” in a truncated search means “no error in the explored part”, not “property verified”. The repository script declares PASSED for the eight LTL searches when grep finds errors: 0, and for the safety search as soon as pan exits; either way, a truncated search passes. There is a second detail: the script launches the safety search without selecting a claim, and pan then takes the first one in the model (it says so in its first output line); a search with a claim only follows the executions compatible with that claim, so to check only the assertions you have to compile with -DNOCLAIM.

Update, October 21, 2026: the repository has fixed the script (cpp-cache PR #2, commit 8065a65). It now checks the assertions without a claim and all ten properties, and marks any truncated search as INCOMPLETE; the LaTeX document now reports the figures of this run too. What this article describes corresponds to commit 5bfaf38.

The figures in the LaTeX document that accompanies the repository (about 3,500,000 states and 4 seconds for safety) correspond to an earlier and smaller version of the model: that document was last edited on March 25, 2026 and the model kept changing until the 30th. In the October 19, 2026 run, the safety search alone stored more than 33 million states before running out of memory.

That is why we attempted a safety search without a claim (-DNOCLAIM -DSAFETY) with the COLLAPSE compression that pan itself suggests and a 40 GB limit, with a 90-minute cap, and then one liveness property with the same resources. The second one never ran: the system stopped the first one early, as the table shows.

Safety (30 assertions), no claim, COLLAPSE, 40 GB: the operating system stopped the process for lack of memory after 38 minutes, with 537,000,000 stored states, 2,530,000,000 transitions and 31.1 GB in use according to pan’s last progress line; no errors up to that point and no final report.

All of this is in the published output; anyone can repeat it with the repository’s commands and compare. What does not change is the content of the model: the 30 assertions and the 10 properties are the same. What changes is how much of the state space has been explored when checking them, and that has to be stated next to every figure.

Lessons

1. The correspondence table is the tool. The value was not in SPIN saying “0 errors” but in writing, guard by guard, which line of C++ each construct of the model stands for. That is where the missing check showed up.
2. Model the reference counter, not only the states. Version 4 of the model added slot_rc[]; without it, the eviction invariant cannot be expressed.
3. Declare the bounds and the abstractions in the same place as the properties. A “formally verified” without them says less than it seems.
4. Read the full pan report, not only “errors: 0”. A search truncated by memory prints the same string; a verification script has to fail when “reached -DMEMLIM bound” shows up, and safety has to be checked without a claim. Publishing the whole run (verifier version, commit, commands, machine and output) is what makes this visible.
5. The model and the tests split the work. Tests and sanitizers see the interleaving that happened; the model, all the possible ones within the bounds. Neither replaces the other.

Summary

The model, the script and the code are in lrleon/cpp-cache; the run is in simylresearch/simyl-benchmarks. If your system depends on similar concurrent infrastructure, this is how we work: technical consulting on performance and architecture and high-performance backend and API development; the performance and architecture diagnostic is a first step with a fixed scope and a reference price.

Correction, October 20, 2026: the model has 30 assert statements. The first version of this article said 33 because it counted the lines that contain the word, including a comment, the definition of assert_consistent() and its call.