Verificación formal de una caché C++ con SPIN/Promela

TL;DR — El repositorio de cpp-cache incluye un modelo Promela acotado del protocolo single-flight de la caché. SPIN comprueba sobre ese modelo 30 aserciones de seguridad y 10 propiedades de vitalidad (LTL). Contrastar el modelo con el código C++ reveló en marzo de 2026 que la rutina de expulsión no comprobaba el contador de referencias y podía expulsar una entrada que otro hilo seguía usando. Este artículo explica qué verifica el modelo, qué no, y publica una corrida de SPIN del 19 de octubre de 2026 con sus cifras y su entorno. Al repetir la corrida con los parámetros del script del repositorio encontramos algo más: ninguna de las once búsquedas cabe en los 4 GB que fija el script, y el script las da por PASSED igual. Lo contamos con las cifras.

Qué se midió y dónde. Las cifras de la corrida (estados, transiciones, profundidad, memoria y tiempo) salen de ejecutar SPIN 6.5.2 sobre formal/cache_model.pml del commit 5bfaf38 de cpp-cache, el 19 de octubre de 2026, en la máquina descrita más abajo, la misma de Benchmarks. La salida completa está en simylresearch/simyl-benchmarks. Son resultados del modelo acotado, no una demostración de corrección del código C++.

Por qué un modelo y no solo pruebas

Una caché concurrente con single-flight tiene pocas reglas, pero todas tratan de intercalados: qué pasa si un hilo expulsa una entrada mientras otro la lee, si dos hilos piden la misma clave en el mismo microsegundo, si una entrada expira mientras alguien espera su cálculo. Las pruebas de concurrencia y los sanitizers ejercitan algunos de esos intercalados, los que la planificación del sistema operativo produce ese día. Un modelo explorado por un model checker recorre todos los intercalados posibles de una abstracción acotada del protocolo.

Las dos cosas se complementan. cpp-cache tiene 106 casos de prueba (71 unitarios y 35 de concurrencia) que corren en integración continua con AddressSanitizer, UndefinedBehaviorSanitizer y ThreadSanitizer, más 12 pruebas pensadas para Helgrind, DRD y Memcheck que se ejecutan a mano. El modelo Promela cubre lo que esas pruebas no pueden garantizar: que ningún intercalado, dentro de los límites del modelo, viola los invariantes del protocolo.

Qué modela

El modelo (formal/cache_model.pml, versión 5, 813 líneas) no es una traducción línea por línea de cache.H. Es un modelo de comportamiento: representa los estados de cada entrada, el contador de referencias, las fases de bloqueo y las operaciones públicas, y deja fuera lo que no afecta al protocolo.

Quedan fuera, a propósito, la resolución de colisiones de la tabla hash, el contenido de los valores y la integración con el cortacircuitos. La cabecera del modelo trae una tabla de correspondencia entre cada construcción Promela y la entidad C++ que representa; esa tabla es la que se revisa cuando cambia el código.

flowchart LR
    Code["cache.H\n(C++20)"] -- "revisión cruzada\nde guardas e invariantes" --> Model["cache_model.pml\n(Promela, v5)"]
    Model -- "spin -a · pan" --> Safety["30 aserciones\n(seguridad)"]
    Model -- "pan -a -f -N" --> LTL["10 propiedades LTL\n(vitalidad)"]
    Tests["106 pruebas + sanitizers\n(CI)"] -. "intercalados observados" .-> Code
    Safety & LTL -. "intercalados posibles\ndentro de los límites" .-> Code

Qué comprueba

Seguridad. 30 sentencias assert, evaluadas en cada transición, agrupadas en ocho clases: nunca hay más entradas que la capacidad; el contador de cómputos en curso coincide con las entradas en Computing; no hay dos entradas para la misma clave; no hay dos cómputos simultáneos de la misma clave; una entrada vacía no conserva clave; una entrada en Computing nunca aparece expirada; la lista LRU siempre está bien formada; la expulsión solo reutiliza entradas que no están en Computing. A eso se suman los invariantes del contador de referencias: una entrada vacía tiene cero referencias, una ocupada al menos una (la de la tabla), una en Computing al menos dos (la tabla y el hilo que la instaló).

Vitalidad. Diez propiedades LTL, comprobadas bajo weak fairness:

La saturación merece una línea: cuando la caché está llena y todas las entradas están en Computing o retenidas por hilos activos, no hay nada que expulsar. El modelo devuelve un resultado explícito, Saturated, igual que el código, y la última propiedad comprueba que ese estado no puede durar para siempre.

Cómo se ejecuta

El repositorio trae formal/run_spin.sh con la secuencia completa:

cd formal
spin -a cache_model.pml
cc -O2 -DNFAIR=8 -DMEMLIM=4096 -o pan pan.c
./pan -m100000 -n -E                                   # seguridad: aserciones
./pan -m100000 -n -E -a -f -N no_starvation_thread2    # una propiedad LTL

-E ignora los estados finales «inválidos» de los procesos de fondo, que están vivos a propósito; -f impone weak fairness, el supuesto bajo el que tiene sentido exigir progreso (todo cómputo admitido termina); -DMEMLIM=4096 acota la memoria a 4 GB. Un detalle que conviene saber: el script del repositorio ejecuta ocho de las diez propiedades; no_orphaned_computing y saturation_transient hay que lanzarlas aparte, y así lo hicimos en la corrida de abajo.

El bug que salió de contrastar el modelo con el código

La historia es de marzo de 2026 y cabe en cuatro commits. El 19 de marzo entró la versión 2 de la caché con single-flight. El 21, el contador de referencias atómico por entrada y el guardián RAII EntryGuard, que incrementa el contador mientras un hilo trabaja con la entrada y lo decrementa al salir. Ese mismo día, una corrección para marcar las entradas nuevas como Computing bajo el mutex global, de modo que nunca sean expulsables entre la inserción y el cálculo.

El 22 de marzo llegó el modelo Promela. En el modelo, la guarda de expulsión era slot_rc[s] <= 1: solo se expulsa una entrada cuya única referencia es la de la tabla. Al contrastar esa guarda con find_evictable_lru() en C++, la comprobación no estaba: el código solo excluía las entradas en Computing.

// Antes: una entrada retenida por un EntryGuard podía expulsarse
if (entry->state() != EntryState::Computing)
  return entry;

// Después: alineado con el invariante del modelo (slot_rc[s] <= 1)
if (entry->state() != EntryState::Computing and
    entry->_refcount.load(std::memory_order_acquire) <= 1)
  return entry;

Sin esa guarda, un hilo con la entrada en la mano podía verla expulsada y liberada por otro: un use-after-free potencial, de los que solo aparecen con el intercalado justo. Hay que ser preciso con el crédito: SPIN no produjo un contraejemplo, porque el modelo ya tenía la guarda correcta. Fue la revisión cruzada entre el modelo y el código, obligatoria al escribir la tabla de correspondencia, la que dejó a la vista la comprobación ausente. El commit que incorporó el modelo trajo también la corrección y pruebas nuevas que ejercitan justo ese invariante, entre ellas evict_while_holder_active y computing_entry_not_evicted_heavy.

sequenceDiagram
    participant A as Hilo A
    participant C as Caché
    participant E as Expulsor
    A->>C: get_or_compute(k) → EntryGuard (rc = 2)
    E->>C: necesita un hueco
    rect rgb(255, 235, 235)
        Note over C,E: Antes: solo se comprobaba Computing → expulsa la entrada de A
    end
    rect rgb(235, 255, 235)
        Note over C,E: Después: rc = 2 > 1 → salta esa entrada y busca otra
    end
    A->>C: fin del uso → release() (rc = 1)

Qué no cubre

• Es un modelo acotado. Dos entradas, tres claves y seis hilos bastan para que aparezcan la contención por clave, la expulsión bajo presión y la saturación, pero una propiedad válida en ese espacio de estados no es una demostración para cualquier tamaño.
• Verifica el protocolo, no el binario. El modelo de memoria de C++, el compilador y las excepciones quedan fuera. La correspondencia entre el modelo y cache.H se mantiene por revisión; las pruebas de concurrencia, los sanitizers y Valgrind cubren lo que el modelo abstrae.
• No corre en integración continua. La CI de cpp-cache compila y ejecuta las pruebas con tres sanitizers; SPIN se lanza a mano. Por eso tiene sentido publicar corridas con fecha y commit.

La corrida del 19 de octubre de 2026

Entorno: SPIN 6.5.2 (paquete de Ubuntu 24.04), cc (Ubuntu 14.3.0-12ubuntu1~24~ppa1) 14.3.0, AMD Ryzen 7 PRO 7840U w/ Radeon 780M Graphics, 58 GiB de RAM, Ubuntu 24.04.5 LTS, kernel 6.8.0-146-generic. Modelo formal/cache_model.pml del commit 5bfaf38 (SHA-256 en la salida publicada). Primero ejecutamos run_spin.sh tal cual, y reportó PASSED en la seguridad y en sus ocho propiedades. Después repetimos cada búsqueda por separado, con los mismos comandos y banderas, para guardar la salida completa de pan y añadir las dos propiedades que el script omite.

Las once búsquedas terminaron sin errores en lo explorado, pero las once alcanzaron el límite de 4 GB que fija el script del repositorio (-DMEMLIM=4096) y se detuvieron antes de agotar el espacio de estados: pan lo anuncia con «reached -DMEMLIM bound» y aun así imprime «errors: 0», que es lo que run_spin.sh comprueba para declarar PASSED en las ocho búsquedas LTL; en la de seguridad imprime PASSED en cuanto pan termina, sin mirar la salida. El vector de estado es de 168 bytes; «estados almacenados» cuenta estados distintos hasta la parada y «transiciones» los pasos explorados. En total, 62 minutos de verificador.

Un PASSED que no era una verificación completa

pan recorre el espacio de estados en profundidad y, cuando toca el límite de memoria, se detiene e informa de los errores encontrados hasta ahí. «errors: 0» en una búsqueda truncada significa «ningún error en la parte explorada», no «propiedad verificada». El script del repositorio declara PASSED en las ocho búsquedas LTL cuando grep encuentra errors: 0, y en la de seguridad en cuanto pan termina; en ambos casos una búsqueda truncada pasa igual. Hay un segundo detalle: el script lanza la búsqueda de seguridad sin elegir claim, y entonces pan toma el primero del modelo (lo dice en su primera línea de salida); una búsqueda con claim solo recorre las ejecuciones compatibles con ese claim, así que para comprobar únicamente las aserciones hay que compilar con -DNOCLAIM.

Actualización del 21 de octubre de 2026: el repositorio ya corrigió el script (PR #2 de cpp-cache, commit 8065a65). Ahora comprueba las aserciones sin claim y las diez propiedades, y marca como INCOMPLETE cualquier búsqueda truncada; el documento LaTeX también presenta ya las cifras de esta corrida. Lo que describe este artículo corresponde al commit 5bfaf38.

Los números del documento LaTeX que acompaña al repositorio (unos 3.500.000 estados y 4 segundos para la seguridad) corresponden a una versión anterior y más pequeña del modelo: ese documento se editó por última vez el 25 de marzo de 2026 y el modelo cambió hasta el 30. En la corrida del 19 de octubre de 2026, la sola búsqueda de seguridad almacenó más de 33 millones de estados antes de quedarse sin memoria.

Por eso intentamos una búsqueda de seguridad sin claim (-DNOCLAIM -DSAFETY) con la compresión COLLAPSE que el propio pan sugiere y un límite de 40 GB, con un tope de 90 minutos, y después una propiedad de vitalidad con los mismos recursos. La segunda no llegó a ejecutarse: el sistema detuvo la primera antes de tiempo, como se ve en la tabla.

Seguridad (30 aserciones), sin claim, COLLAPSE, 40 GB: el sistema operativo detuvo el proceso por falta de memoria a los 38 minutos, con 537.000.000 estados almacenados, 2.530.000.000 transiciones y 31,1 GB ocupados según la última línea de progreso de pan; sin errores hasta ahí y sin informe final.

Todo esto está en la salida publicada; cualquiera puede repetirlo con los comandos del repositorio y comparar. Lo que no cambia es el contenido del modelo: las 30 aserciones y las 10 propiedades son las mismas. Lo que cambia es cuánto del espacio de estados se ha explorado al comprobarlas, y eso hay que decirlo junto a cada cifra.

Lecciones

1. La tabla de correspondencia es la herramienta. El valor no estuvo en que SPIN dijera «0 errores», sino en escribir, guarda por guarda, qué línea de C++ representa cada construcción del modelo. Ahí apareció la comprobación ausente.
2. Modelar el contador de referencias, no solo los estados. La versión 4 del modelo añadió slot_rc[]; sin él, el invariante de expulsión no se puede expresar.
3. Declarar la cota y las abstracciones en el mismo sitio que las propiedades. Un «verificado formalmente» sin eso dice menos de lo que parece.
4. Leer el informe completo de pan, no solo «errors: 0». Una búsqueda truncada por memoria imprime la misma cadena; un script de verificación tiene que fallar cuando aparezca «reached -DMEMLIM bound», y la seguridad hay que comprobarla sin claim. Publicar la corrida entera (versión del verificador, commit, comandos, máquina y salida) es lo que permite ver esto.
5. El modelo y las pruebas se reparten el trabajo. Las pruebas y los sanitizers ven el intercalado que ocurrió; el modelo, todos los posibles dentro de la cota. Ninguno sustituye al otro.

Resumen

El modelo, el script y el código están en lrleon/cpp-cache; la corrida, en simylresearch/simyl-benchmarks. Si tu sistema depende de infraestructura concurrente parecida, así trabajamos: consultoría técnica en rendimiento y arquitectura y desarrollo de backends y APIs de alto rendimiento; el diagnóstico de rendimiento y arquitectura es un primer paso con alcance cerrado y precio de referencia.

Corrección del 20 de octubre de 2026: el modelo tiene 30 sentencias assert. La primera versión de este artículo decía 33, porque contaba las líneas que contienen la palabra, entre ellas un comentario, la definición de assert_consistent() y su llamada.