noxaur/verify-design-leases

Vérifier les baux de design

crates/server/tla/DesignLeases.tla est un modèle TLA+ de deux serveurs Finite qui partagent un seul stockage, et d'un design se déplaçant entre eux. TLC, le vérificateur de modèle TLA+, essaie tous les ordres de leurs étapes dans des limites réduites et vérifie deux règles :

• StoredEditsStay (clôture) : une fois que le stockage accepte une modification, aucune copie obsolète sur un autre serveur ne l'écrase jamais. Si cette règle est violée, un serveur qui a calé se réveille et efface les modifications que le nouveau propriétaire a sauvegardées.
• AckedEditsStay : une modification qu'un outil MCP a signalée comme effectuée se trouve dans le stockage, ou dans une copie qui peut encore la sauvegarder, à moins que son serveur n'ait planté ou que son bail n'ait expiré avant que la modification ne soit sauvegardée. Si cette règle est violée, un agent reçoit la confirmation que sa modification a fonctionné, puis la modification disparaît. Les visualiseurs la voient disparaître, et rien n'avertit l'agent.

Le code actuel passe la première règle et enfreint la seconde de quatre façons connues. Elles sont listées dans « Résultats connus » ci-dessous.

Votre modification touche-t-elle ceci ?

Oui, si elle modifie une fonction de ce tableau. Chaque étape du modèle nomme le code qu'elle représente, et un relecteur peut ouvrir les deux côte à côte.

Étape du modèle	Code
CallStarts, CallFindsHandle, CallLoads, CallEdits, CallReads	mcp/mod.rs design, edit_checked ; api.rs open ; hub/mod.rs Hub::open, handle_for ; hub/design.rs DesignHandle::load, edit
SaveTakes, SaveWrites, SaveFenced, SaveFails, SaveReleases, SaveDrops	hub/mod.rs persist ; hub/design.rs take_save, save_failed
Unload	hub/mod.rs Hub::sweep ; hub/design.rs unload_if_idle, is_idle
TickRenews … TickDiscovers	hub/mod.rs Hub::tick, let_go, remove, drop_copy, discover, summaries ; hub/design.rs retire, end, lease
Owns, LeaseLapses, HeartbeatExpires	cluster.rs Members::now, lapsed, renewed, Cluster::owns, owner
CanClaim, Claimed, écritures de stockage	postgres/mod.rs claim, save, append, release, held ; store.rs trait Store (le stockage partagé en mémoire doit correspondre)
Start, Crash	hub/mod.rs Hub::shared

Les chemins sont sous crates/server/src/.

Validation à ce commit : 6606714. C'est le dernier commit sur lequel le modèle a été vérifié contre ce code. Pour voir ce qui a changé dans le code couvert depuis :

git diff 6606714 -- crates/server/src/hub crates/server/src/mcp/mod.rs crates/server/src/api.rs crates/server/src/cluster.rs crates/server/src/postgres/mod.rs crates/server/src/store.rs

Si la différence touche une fonction du tableau, relisez l'étape du modèle à côté avant de faire confiance à un succès. Avancez la validation à ce commit, dans ce fichier, seulement après avoir confirmé que chaque étape modifiée correspond toujours au code au nouveau commit.

Exécutez-le

crates/server/tla/check.sh          # la vérification quotidienne, environ 2 minutes
crates/server/tla/check.sh --full   # ajoute Finding4.cfg et AllFixes.cfg, environ 3 minutes de plus

Le script télécharge TLC (tla2tools.jar v1.7.4, somme SHA-256 vérifiée) dans ~/.cache/finite à son premier lancement. Java 11 ou plus récent est nécessaire. Chaque configuration affiche ok quand elle donne le résultat enregistré pour le code aujourd'hui, et FAIL sinon. Quand une règle est enfreinte, la sortie de TLC, avec le chemin le plus court vers l'infraction, est sauvegardée dans crates/server/tla/<configuration>.out. Git ignore ces fichiers.

Configuration	Corrections activées	Limites	Résultat aujourd'hui
Fencing.cfg	aucune	1 modification, 1 lecture, 2 handles, tout comportement jusqu'à 18 étapes	succès, environ 2.8M d'états, 2 minutes
DesignLeases.cfg	aucune	1 modification, 2 handles	constat n°1, quelques secondes
Finding2.cfg	FixRetire	1 modification, 2 handles	constat n°2
Finding3.cfg	FixRetire, FixOrphan	2 modifications, 2 handles	constat n°3
Finding4.cfg	+ FixStaleDrop	2 modifications, 2 handles	constat n°4, environ 1 minute
AllFixes.cfg	les quatre	2 modifications, 2 handles	succès, environ 16M d'états, 2 minutes

Toutes les configurations limitent l'époque du stockage à 3, et aucune n'inclut de crash ou d'échec d'écriture. Une lecture est un appel qui charge le design sans le modifier, comme un outil de lecture MCP ou une socket de visualiseur. La clôture en a besoin, car une copie obsolète ne peut exister que lorsque deux appels ont chargé le design. Son espace d'états complet avec cette lecture n'a pas fini en 30 minutes, donc check.sh l'exécute avec l'approfondissement itératif de TLC (-dfid 18) : tout comportement de jusqu'à 18 étapes. Le plus court écrasement obsolète en prend 17. Les configurations de constats explorent tout dans leurs limites. TLC s'arrête à la première règle enfreinte, donc chaque configuration de constat active les correctifs proposés pour les constats précédents. Les constantes Fix* sont des commutateurs hypothétiques. Avec toutes à FALSE, le modèle est le code tel qu'il est aujourd'hui.

Lire le résultat

Lisez chaque résultat avec le skill /statechart. Il transforme le plus court chemin de TLC vers une règle enfreinte en une liste numérotée d'étapes en langage clair, et quand une configuration réussit, il dessine un graphique de la façon dont le design se déplace entre les serveurs.

Quand une configuration affiche FAIL, décidez si le bogue est dans le code ou dans le modèle :

• Un vrai bogue donne un chemin que vous pouvez rejouer dans le code. Parcourez chaque étape, ouvrez la fonction du tableau, et vérifiez que le code permet cette étape dans cet ordre. Signalez ensuite le chemin dans les termes du code, comme le font les constats ci-dessous. N'affaiblissez pas une règle ou une limite avant que la vérification réussisse, et ne modifiez pas le code du produit sauf si on vous l'a demandé.
• Une erreur de modélisation donne une étape que le code ne peut pas exécuter. Exemples : deux étapes que le code exécute sous un même verrou (le mutex d'état, le mutex de persistance), séparées dans le modèle ; une étape du modèle sans garde que le code a ; ou un battement de cœur qui expire juste après un renouvellement. Corrigez le modèle pour qu'il corresponde au code, et dites ce que vous avez corrigé.
• Une rupture de Fencing.cfg provient de l'exécution à profondeur limitée, dont le chemin ne nomme pas ses étapes. Pour obtenir un chemin nommé le plus court, exécutez la même configuration en largeur d'abord : cd crates/server/tla && java -cp ~/.cache/finite/tla2tools-1.7.4.jar tlc2.TLC -workers auto -config Fencing.cfg DesignLeases.tla. Elle s'arrête à la première rupture, ce qui a pris environ 6 secondes pour la rupture décrite dans « Quand vous modifiez intentionnellement le code couvert ».
• error signifie que TLC n'a pas terminé : une erreur d'analyse, ou une variable qu'une action laisse non assignée. Lisez le fichier .out.

Un FAIL là où le code violait la règle et réussit maintenant est une bonne nouvelle. Le tableau des constats sous « Résultats connus » montre comment l'enregistrer.

Quand vous modifiez intentionnellement le code couvert

1. Modifiez l'étape du modèle dans le même commit que le code, et conservez le commentaire qui nomme la fonction.
2. Si votre modification corrige un constat, intégrez la correction dans le modèle comme du code, pas comme un commutateur : supprimez la constante Fix*, faites en sorte que l'étape se comporte comme le nouveau code, et retirez le commutateur de chaque configuration. La configuration du constat suivant devient la configuration par défaut, et check.sh obtient les nouveaux résultats attendus.
3. Avant de faire confiance à un succès, cassez intentionnellement le code dans une copie de travail, reflétez la cassure dans le modèle, et vérifiez que la configuration la détecte. Par exemple, si vous supprimez AND epoch = $3 de PgStore::save et supprimez x.ptok = store.epoch de SaveWrites, alors Fencing.cfg viole StoredEditsStay. Une vérification que vous n'avez jamais vue échouer ne prouve rien.
4. Exécutez check.sh --full, puis avancez la validation à ce commit.

Résultats connus

Chacun est une condition de course sur le code à 6606714. Dans chaque cas, l'appel d'outil de l'agent renvoie un succès et la modification est perdue.

1. Une modification atterrit sur une copie qui est déjà en train de sauvegarder son dernier instantané. Le serveur A a le design chargé, et un appel MCP a passé Hub::open. Le serveur B rejoint et gagne le design (un bail expiré sur A fait aussi l'affaire). Le tick de A appelle let_go, donc retire marque la copie Retiring. La tâche de sauvegarde take_save prend le dernier instantané. Ensuite, l'appel DesignHandle::edit prend le verrou et valide dans la copie en cours de retraite, car edit ne regarde jamais life. La tâche de sauvegarde sauvegarde l'instantané sans la modification, libère le bail, et drop_copy efface pending. B charge le design sans la modification. Pour déclencher cela dans l'application réelle, des modifications doivent déjà attendre sur le verrou du design quand le tick s'exécute, par exemple plusieurs agents exécutant de grands appels write_html. Annuler, refaire, importer et mettre à jour les commentaires empruntent le même chemin.
2. Une modification atterrit sur un handle que le hub a déjà retiré de sa liste. L'appel handle_for d'un appel renvoie un handle qui n'est pas chargé. B rejoint, et let_go de A ne voit rien chargé, donc il appelle remove. L'appel load revendique le bail et charge une copie sur ce handle. La liste loaded du tick suivant provient de la liste du hub, qui n'a plus ce handle. Ainsi le tick libère le bail, et la prochaine sauvegarde de la copie échoue avec Fenced. Cela ne nécessite aucun calage, seulement qu'un serveur rejoigne.
3. Le tick supprime une copie qui a été rechargée après que le tick l'a lue. Un serveur, aucun changement d'appartenance. Le tick lit lease() (jeton 1). Ensuite le design se décharge, et un appel le recharge (jeton 2) et valide une modification. Le tick lit held() (jeton 2), voit que 2 ≠ 1, et appelle drop_copy. drop_copy met fin à la nouvelle copie, modification en attente comprise. La fenêtre est de deux lectures d'écart, donc étroite, mais elle se produit à chaque tick.
4. Un serveur qui vient de renouveler son bail sert sa copie obsolète. B cale au-delà de son bail, A prend le design en charge et sauvegarde une modification. B se réveille. Son tick renouvelle le battement de cœur, et à partir de ce moment Members::now considère B comme actif et de nouveau propriétaire. Mais la boucle let_go n'a pas encore tourné. Un appel sur B charge la copie obsolète toujours Live et valide une modification, qui échoue plus tard avec Fenced. Cela nécessite d'abord un calage.

AllFixes.cfg vérifie un correctif proposé pour chaque constat : edit refuse une copie qui n'est pas Live (1) ou un handle qui n'est pas listé (2). Le tick supprime une copie seulement si son jeton est celui qu'il a lu (3). Un serveur qui a renouvelé après une expiration se compte lui-même hors service jusqu'à ce qu'il ait laissé tomber (4). Avec les quatre, AckedEditsStay tient dans ces limites.

Ce qui n'est pas couvert

• Un design, deux serveurs, modifications MCP. Annuler, refaire, importer, commentaires et renommer empruntent le même chemin verrou-et-validation mais ne sont pas modélisés séparément. Hub::delete non plus.
• Le stockage fichier et les transferts FINITE_NODES (hand_off_one, adopt), et le routeur.
• Hub::flush à l'arrêt, les seuils de compactage du journal (COMPACT_AFTER, COMPACT_BYTES), et Recent, le tampon derrière la reprise du visualiseur.
• Le timing. TLC essaie tous les ordres d'étapes, donc le modèle montre qu'une condition de course existe, pas sa fréquence. Il suppose que le temporisateur de bail d'un serveur (Members::lapsed) expire au plus tard quand la base de données considère son battement de cœur comme expiré. Cela tient quand les deux horloges tournent à la même vitesse.
• Des limites plus grandes. Plus de modifications, lectures, handles ou époques, les crashs et les échecs d'écriture ne sont pas dans les configurations quotidiennes. AllFixes.cfg a aussi réussi avec 1 modification, 1 crash et 1 échec d'écriture (3,4M d'états). La clôture au-delà de 18 étapes n'a pas terminé : avec 1 modification et 1 lecture, elle a passé 50M d'états distincts et continuait. Ne faites pas confiance à une ancienne réussite de clôture sans lecture : une seule modification ne charge qu'une seule copie, donc rien ne peut devenir obsolète.