Vérification formelle d’un cache C++ avec SPIN/Promela

En bref — Le dépôt de cpp-cache contient un modèle Promela borné du protocole single-flight du cache. Sur ce modèle, SPIN vérifie 30 assertions de sûreté et 10 propriétés de vivacité (LTL). En mars 2026, la confrontation du modèle avec le code C++ a révélé que la routine d’éviction ne vérifiait pas le compteur de références et pouvait évincer une entrée qu’un autre fil utilisait encore. Cet article explique ce que le modèle vérifie, ce qu’il ne vérifie pas, et publie une exécution de SPIN du 19 octobre 2026 avec ses chiffres et son environnement. En relançant l’exécution avec les paramètres du script du dépôt, nous avons trouvé autre chose : aucune des onze recherches ne tient dans les 4 Go que fixe le script, et le script les déclare quand même PASSED. Nous le racontons avec les chiffres.

Ce qui a été mesuré et où. Les chiffres de l’exécution (états, transitions, profondeur, mémoire et temps) proviennent de SPIN 6.5.2 lancé sur formal/cache_model.pml au commit 5bfaf38 de cpp-cache, le 19 octobre 2026, sur la machine décrite plus bas, la même que celle des Benchmarks. La sortie complète est dans simylresearch/simyl-benchmarks. Ce sont des résultats du modèle borné, pas une démonstration de la correction du code C++.

Pourquoi un modèle et pas seulement des tests

Un cache concurrent avec single-flight a peu de règles, mais toutes portent sur des entrelacements : que se passe-t-il si un fil évince une entrée pendant qu’un autre la lit, si deux fils demandent la même clé dans la même microseconde, si une entrée expire pendant que quelqu’un attend son calcul. Les tests de concurrence et les sanitizers exercent certains de ces entrelacements, ceux que l’ordonnancement du système d’exploitation produit ce jour-là. Un modèle exploré par un model checker parcourt tous les entrelacements possibles d’une abstraction bornée du protocole.

Les deux se complètent. cpp-cache compte 106 cas de test (71 unitaires et 35 de concurrence) qui tournent en intégration continue avec AddressSanitizer, UndefinedBehaviorSanitizer et ThreadSanitizer, plus 12 tests prévus pour Helgrind, DRD et Memcheck, lancés à la main. Le modèle Promela couvre ce que ces tests ne peuvent garantir : qu’aucun entrelacement, dans les limites du modèle, ne viole les invariants du protocole.

Ce qu’il modélise

Le modèle (formal/cache_model.pml, version 5, 813 lignes) n’est pas une traduction ligne à ligne de cache.H. C’est un modèle de comportement : il représente les états de chaque entrée, le compteur de références, les phases de verrouillage et les opérations publiques, et laisse de côté ce qui n’affecte pas le protocole.

Restent volontairement en dehors la résolution des collisions de la table de hachage, le contenu des valeurs et l’intégration avec le disjoncteur. L’en-tête du modèle contient une table de correspondance entre chaque construction Promela et l’entité C++ qu’elle représente ; c’est cette table qu’on relit quand le code change.

flowchart LR
    Code["cache.H\n(C++20)"] -- "revue croisée\ndes gardes et invariants" --> Model["cache_model.pml\n(Promela, v5)"]
    Model -- "spin -a · pan" --> Safety["30 assertions\n(sûreté)"]
    Model -- "pan -a -f -N" --> LTL["10 propriétés LTL\n(vivacité)"]
    Tests["106 tests + sanitizers\n(CI)"] -. "entrelacements observés" .-> Code
    Safety & LTL -. "entrelacements possibles\ndans les limites" .-> Code

Ce qu’il vérifie

Sûreté. 30 instructions assert, évaluées à chaque transition, regroupées en huit classes : il n’y a jamais plus d’entrées que la capacité ; le compteur de calculs en cours correspond aux entrées en Computing ; il n’y a pas deux entrées pour la même clé ; il n’y a pas deux calculs simultanés de la même clé ; une entrée vide ne garde pas de clé ; une entrée en Computing n’apparaît jamais expirée ; la liste LRU est toujours bien formée ; l’éviction ne réutilise que des entrées qui ne sont pas en Computing. S’y ajoutent les invariants du compteur de références : une entrée vide a zéro référence, une entrée occupée au moins une (celle de la table), une entrée en Computing au moins deux (la table et le fil qui l’a installée).

Vivacité. Dix propriétés LTL, vérifiées sous weak fairness :

La saturation mérite une ligne : quand le cache est plein et que toutes les entrées sont en Computing ou retenues par des fils actifs, il n’y a rien à évincer. Le modèle renvoie un résultat explicite, Saturated, comme le code, et la dernière propriété vérifie que cet état ne peut pas durer indéfiniment.

Comment on l’exécute

Le dépôt fournit formal/run_spin.sh avec la séquence complète :

cd formal
spin -a cache_model.pml
cc -O2 -DNFAIR=8 -DMEMLIM=4096 -o pan pan.c
./pan -m100000 -n -E                                   # sûreté : assertions
./pan -m100000 -n -E -a -f -N no_starvation_thread2    # une propriété LTL

-E ignore les états finaux « invalides » des processus de fond, qui restent vivants exprès ; -f impose la weak fairness, l’hypothèse sous laquelle il a un sens d’exiger un progrès (tout calcul admis se termine) ; -DMEMLIM=4096 borne la mémoire à 4 Go. Un détail à connaître : le script du dépôt exécute huit des dix propriétés ; no_orphaned_computing et saturation_transient doivent être lancées à part, et c’est ce que nous avons fait dans l’exécution ci-dessous.

Le bug né de la confrontation du modèle avec le code

L’histoire date de mars 2026 et tient en quatre commits. Le 19 mars est arrivée la version 2 du cache avec single-flight. Le 21, le compteur de références atomique par entrée et le gardien RAII EntryGuard, qui incrémente le compteur pendant qu’un fil travaille avec l’entrée et le décrémente à la sortie. Le même jour, une correction pour marquer les nouvelles entrées comme Computing sous le mutex global, afin qu’elles ne soient jamais évinçables entre l’insertion et le calcul.

Le 22 mars est arrivé le modèle Promela. Dans le modèle, la garde d’éviction était slot_rc[s] <= 1 : on n’évince qu’une entrée dont la seule référence est celle de la table. En confrontant cette garde avec find_evictable_lru() en C++, la vérification manquait : le code n’excluait que les entrées en Computing.

// Avant : une entrée retenue par un EntryGuard pouvait être évincée
if (entry->state() != EntryState::Computing)
  return entry;

// Après : aligné sur l’invariant du modèle (slot_rc[s] <= 1)
if (entry->state() != EntryState::Computing and
    entry->_refcount.load(std::memory_order_acquire) <= 1)
  return entry;

Sans cette garde, un fil qui avait l’entrée en main pouvait la voir évincée et libérée par un autre : un use-after-free potentiel, de ceux qui n’apparaissent qu’avec le bon entrelacement. Il faut être précis sur le mérite : SPIN n’a pas produit de contre-exemple, puisque le modèle avait déjà la bonne garde. C’est la revue croisée entre le modèle et le code, obligatoire pour écrire la table de correspondance, qui a mis au jour la vérification absente. Le commit qui a ajouté le modèle a aussi apporté la correction et de nouveaux tests qui exercent précisément cet invariant, dont evict_while_holder_active et computing_entry_not_evicted_heavy.

sequenceDiagram
    participant A as Fil A
    participant C as Cache
    participant E as Évinceur
    A->>C: get_or_compute(k) → EntryGuard (rc = 2)
    E->>C: a besoin d’une place
    rect rgb(255, 235, 235)
        Note over C,E: Avant : seul Computing était vérifié → évince l’entrée de A
    end
    rect rgb(235, 255, 235)
        Note over C,E: Après : rc = 2 > 1 → saute cette entrée et en cherche une autre
    end
    A->>C: fin de l’utilisation → release() (rc = 1)

Ce qu’il ne couvre pas

• C’est un modèle borné. Deux entrées, trois clés et six fils suffisent pour faire apparaître la contention par clé, l’éviction sous pression et la saturation, mais une propriété valide dans cet espace d’états n’est pas une démonstration pour n’importe quelle taille.
• Il vérifie le protocole, pas le binaire. Le modèle mémoire de C++, le compilateur et les exceptions restent en dehors. La correspondance entre le modèle et cache.H est maintenue par revue ; les tests de concurrence, les sanitizers et Valgrind couvrent ce que le modèle abstrait.
• Il ne tourne pas en intégration continue. La CI de cpp-cache compile et exécute les tests avec trois sanitizers ; SPIN se lance à la main. C’est pourquoi il est utile de publier des exécutions datées, avec leur commit.

L’exécution du 19 octobre 2026

Environnement : SPIN 6.5.2 (paquet d’Ubuntu 24.04), cc (Ubuntu 14.3.0-12ubuntu1~24~ppa1) 14.3.0, AMD Ryzen 7 PRO 7840U w/ Radeon 780M Graphics, 58 Gio de RAM, Ubuntu 24.04.5 LTS, noyau 6.8.0-146-generic. Modèle formal/cache_model.pml du commit 5bfaf38 (SHA-256 dans la sortie publiée). Nous avons d’abord lancé run_spin.sh tel quel, et il a déclaré PASSED pour la sûreté et pour ses huit propriétés. Nous avons ensuite relancé chaque recherche séparément, avec les mêmes commandes et options, pour conserver la sortie complète de pan et ajouter les deux propriétés que le script omet.

Les onze recherches se sont terminées sans erreur dans la partie explorée, mais toutes les onze ont atteint la limite de 4 Go que fixe le script du dépôt (-DMEMLIM=4096) et se sont arrêtées avant d’épuiser l’espace d’états : pan l’annonce par « reached -DMEMLIM bound » et affiche pourtant « errors: 0 », ce que run_spin.sh vérifie pour déclarer PASSED dans les huit recherches LTL ; pour la sûreté, il affiche PASSED dès que pan se termine, sans regarder la sortie. Le vecteur d’état fait 168 octets ; « états stockés » compte les états distincts jusqu’à l’arrêt et « transitions » les pas explorés. Au total, 62 minutes de vérificateur.

Un PASSED qui n’était pas une vérification complète

pan parcourt l’espace d’états en profondeur et, quand il touche la limite de mémoire, il s’arrête et rapporte les erreurs trouvées jusque-là. « errors: 0 » dans une recherche tronquée signifie « aucune erreur dans la partie explorée », pas « propriété vérifiée ». Le script du dépôt déclare PASSED dans les huit recherches LTL quand grep trouve errors: 0, et pour la sûreté dès que pan se termine ; dans les deux cas, une recherche tronquée passe quand même. Il y a un second détail : le script lance la recherche de sûreté sans choisir de claim, et pan prend alors le premier du modèle (il le dit dans sa première ligne de sortie) ; une recherche avec claim ne parcourt que les exécutions compatibles avec ce claim, si bien que pour vérifier uniquement les assertions il faut compiler avec -DNOCLAIM.

Mise à jour du 21 octobre 2026 : le dépôt a déjà corrigé le script (PR #2 de cpp-cache, commit 8065a65). Il vérifie désormais les assertions sans claim et les dix propriétés, et marque INCOMPLETE toute recherche tronquée ; le document LaTeX présente aussi désormais les chiffres de cette exécution. Ce que décrit cet article correspond au commit 5bfaf38.

Les chiffres du document LaTeX qui accompagne le dépôt (environ 3 500 000 états et 4 secondes pour la sûreté) correspondent à une version antérieure et plus petite du modèle : ce document a été modifié pour la dernière fois le 25 mars 2026 et le modèle a changé jusqu’au 30. Dans l’exécution du 19 octobre 2026, la seule recherche de sûreté a stocké plus de 33 millions d’états avant de manquer de mémoire.

Nous avons donc tenté une recherche de sûreté sans claim (-DNOCLAIM -DSAFETY) avec la compression COLLAPSE que pan suggère lui-même et une limite de 40 Go, plafonnée à 90 minutes, puis une propriété de vivacité avec les mêmes ressources. La seconde n’a pas pu être lancée : le système a arrêté la première avant la fin, comme le montre le tableau.

Sûreté (30 assertions), sans claim, COLLAPSE, 40 Go : le système d’exploitation a arrêté le processus faute de mémoire au bout de 38 minutes, avec 537 000 000 états stockés, 2 530 000 000 transitions et 31,1 Go occupés selon la dernière ligne de progression de pan ; aucune erreur jusque-là et pas de rapport final.

Tout cela est dans la sortie publiée ; chacun peut le reproduire avec les commandes du dépôt et comparer. Le contenu du modèle, lui, ne change pas : les 30 assertions et les 10 propriétés sont les mêmes. Ce qui change, c’est la part de l’espace d’états explorée pour les vérifier, et il faut le dire à côté de chaque chiffre.

Leçons

1. La table de correspondance est l’outil. La valeur n’a pas été que SPIN dise « 0 erreur », mais d’écrire, garde par garde, quelle ligne de C++ représente chaque construction du modèle. C’est là qu’est apparue la vérification absente.
2. Modéliser le compteur de références, pas seulement les états. La version 4 du modèle a ajouté slot_rc[] ; sans lui, l’invariant d’éviction ne peut pas s’exprimer.
3. Déclarer la borne et les abstractions au même endroit que les propriétés. Un « vérifié formellement » sans cela dit moins qu’il n’y paraît.
4. Lire le rapport complet de pan, pas seulement « errors: 0 ». Une recherche tronquée faute de mémoire affiche la même chaîne ; un script de vérification doit échouer quand apparaît « reached -DMEMLIM bound », et la sûreté doit être vérifiée sans claim. Publier l’exécution entière (version du vérificateur, commit, commandes, machine et sortie) est ce qui permet de le voir.
5. Le modèle et les tests se partagent le travail. Les tests et les sanitizers voient l’entrelacement qui s’est produit ; le modèle, tous les entrelacements possibles dans la borne. Aucun ne remplace l’autre.

Résumé

Le modèle, le script et le code sont dans lrleon/cpp-cache ; l’exécution, dans simylresearch/simyl-benchmarks. Si votre système dépend d’une infrastructure concurrente semblable, voici comment nous travaillons : conseil technique en performance et architecture et développement de backends et d’API à haute performance ; le diagnostic de performance et d’architecture est un premier pas à périmètre fermé et prix de référence.

Correction du 20 octobre 2026 : le modèle contient 30 instructions assert. La première version de cet article en indiquait 33, parce qu’elle comptait les lignes contenant le mot, dont un commentaire, la définition de assert_consistent() et son appel.