noxaur/verify-design-leases

Verify design leases

crates/server/tla/DesignLeases.tla ist ein TLA+ Modell von zwei Finite-Servern, die sich einen Speicher teilen, und einem Design, das zwischen ihnen wechselt. TLC, der TLA+ Modellprüfer, probiert jede Reihenfolge ihrer Schritte innerhalb kleiner Grenzen durch und prüft zwei Regeln:

• StoredEditsStay (Fencing): Sobald der Speicher eine Bearbeitung akzeptiert hat, überschreibt keine veraltete Kopie auf einem anderen Server sie jemals. Wenn dies bricht, wacht ein Server, der ausgesetzt war, auf und löscht Bearbeitungen, die der neue Besitzer gespeichert hat.
• AckedEditsStay: Eine Bearbeitung, die ein MCP-Tool als erledigt gemeldet hat, befindet sich im Speicher oder in einer Kopie, die sie noch speichern kann, es sei denn, ihr Server ist abgestürzt oder ihr Lease ist abgelaufen, bevor die Bearbeitung gespeichert wurde. Wenn dies bricht, wird einem Agenten mitgeteilt, dass seine Bearbeitung funktioniert hat, und dann ist die Bearbeitung verschwunden. Betrachter sehen sie verschwinden, und nichts teilt es dem Agenten mit.

Der Code besteht heute die erste Regel und bricht die zweite auf vier bekannte Arten. Sie sind unten unter „Bekannte Ergebnisse" aufgeführt.

Betrifft Ihre Änderung dies?

Ja, wenn sie eine Funktion in dieser Tabelle ändert. Jeder Modellschritt benennt den Code, den er repräsentiert, und ein Prüfer kann beide nebeneinander öffnen.

Modellschritt	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, Store writes	postgres/mod.rs claim, save, append, release, held; store.rs trait Store (der gemeinsam genutzte In-Memory-Speicher muss übereinstimmen)
Start, Crash	hub/mod.rs Hub::shared

Die Pfade liegen unter crates/server/src/.

Sync-Commit: 6606714. Das ist der letzte Commit, bei dem das Modell gegen diesen Code geprüft wurde. Um zu sehen, was sich im abgedeckten Code seitdem geändert hat, führen Sie aus:

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

Wenn der Diff eine Funktion in der Tabelle berührt, lesen Sie den Modellschritt daneben erneut, bevor Sie einem Bestehen vertrauen. Verschieben Sie den Sync-Commit in dieser Datei nur nach vorne, nachdem Sie bestätigt haben, dass jeder geänderte Schritt immer noch mit dem Code im neuen Commit übereinstimmt.

Ausführen

crates/server/tla/check.sh          # die alltägliche Prüfung, etwa 2 Minuten
crates/server/tla/check.sh --full   # fügt Finding4.cfg und AllFixes.cfg hinzu, etwa 3 Minuten mehr

Das Skript lädt TLC (tla2tools.jar v1.7.4, SHA-256 geprüft) bei der ersten Ausführung in ~/.cache/finite herunter. Sie benötigen Java 11 oder neuer. Jede Konfiguration gibt ok aus, wenn sie das für den heutigen Code aufgezeichnete Ergebnis liefert, und FAIL andernfalls. Wenn eine Regel bricht, wird TLCs Ausgabe mit dem kürzesten Pfad zum Bruch als crates/server/tla/<config>.out gespeichert. Git ignoriert diese Dateien.

Konfiguration	Behebt	Grenzen	Ergebnis heute
Fencing.cfg	keine	1 Bearbeitung, 1 Lesevorgang, 2 Handles, jedes Verhalten bis 18 Schritte	bestanden, etwa 2,8M Zustände, 2 Minuten
DesignLeases.cfg	keine	1 Bearbeitung, 2 Handles	Ergebnis 1, Sekunden
Finding2.cfg	FixRetire	1 Bearbeitung, 2 Handles	Ergebnis 2
Finding3.cfg	FixRetire, FixOrphan	2 Bearbeitungen, 2 Handles	Ergebnis 3
Finding4.cfg	+ FixStaleDrop	2 Bearbeitungen, 2 Handles	Ergebnis 4, etwa 1 Minute
AllFixes.cfg	alle vier	2 Bearbeitungen, 2 Handles	bestanden, etwa 16M Zustände, 2 Minuten

Jede Konfiguration begrenzt die Epoche des Speichers auf 3, und keine enthält einen Absturz oder einen fehlgeschlagenen Schreibvorgang. Ein Lesevorgang ist ein Aufruf, der das Design lädt, ohne es zu bearbeiten, wie ein MCP-Lesewerkzeug oder der Socket eines Betrachters. Fencing benötigt einen, weil eine veraltete Kopie nur existieren kann, wenn zwei Aufrufe das Design geladen haben. Sein vollständiger Zustandsraum mit diesem Lesevorgang wurde in 30 Minuten nicht fertig, daher führt check.sh ihn mit TLCs iterativer Vertiefung (-dfid 18) aus: jedes Verhalten von bis zu 18 Schritten. Der kürzeste veraltete Überschreibvorgang dauert 17. Die Ergebnis-Konfigurationen erkunden alles innerhalb ihrer Grenzen. TLC stoppt bei der ersten gebrochenen Regel, daher schaltet jede Ergebnis-Konfiguration die vorgeschlagenen Korrekturen für die Ergebnisse davor ein. Die Fix*-Konstanten sind Was-wäre-wenn-Schalter. Mit allen auf FALSE ist das Modell der Code, wie er heute ist.

Ergebnis lesen

Lesen Sie jedes Ergebnis mit dem /statechart-Skill. Es verwandelt TLCs kürzesten Pfad zu einer gebrochenen Regel in eine nummerierte Liste von Schritten in einfachen Worten, und wenn eine Konfiguration bestanden wird, zeichnet es ein Diagramm, wie sich das Design zwischen Servern bewegt.

Wenn eine Konfiguration FAIL ausgibt, entscheiden Sie, ob der Fehler im Code oder im Modell liegt:

• Ein echter Fehler ergibt einen Pfad, den Sie im Code nachvollziehen können. Gehen Sie jeden Schritt durch, öffnen Sie die Funktion aus der Tabelle und prüfen Sie, ob der Code diesen Schritt in dieser Reihenfolge erlaubt. Melden Sie dann den Pfad in den Worten des Codes, wie die Ergebnisse unten. Schwächen Sie keine Regel oder Grenze, bis die Prüfung bestanden wird, und ändern Sie keinen Produktcode, es sei denn, Sie wurden dazu aufgefordert.
• Ein Modellierungsfehler ergibt einen Schritt, den der Code nicht ausführen kann. Beispiele: zwei Schritte, die der Code unter einer Sperre ausführt (der Zustands-Mutex, der Persistenz-Mutex), im Modell aufgeteilt; ein Modellschritt ohne eine Guard, die der Code hat; oder ein Heartbeat, der direkt nach einer Verlängerung abläuft. Korrigieren Sie das Modell, um dem Code zu entsprechen, und sagen Sie, was Sie korrigiert haben.
• Ein Bruch von Fencing.cfg stammt von der tiefenbegrenzten Ausführung, deren Pfad seine Schritte nicht benennt. Um einen benannten kürzesten Pfad zu erhalten, führen Sie die gleiche Konfiguration breitenorientiert aus: cd crates/server/tla && java -cp ~/.cache/finite/tla2tools-1.7.4.jar tlc2.TLC -workers auto -config Fencing.cfg DesignLeases.tla. Es stoppt beim ersten Bruch, was etwa 6 Sekunden für den Bruch unter „Wenn Sie den abgedeckten Code absichtlich ändern" dauerte.
• error bedeutet, TLC wurde nicht fertig: ein Parse-Fehler, oder eine Variable, die eine Aktion nicht zugewiesen lässt. Lesen Sie die .out-Datei.

Ein FAIL, bei dem der Code früher die Regel verletzt hat und jetzt besteht, sind gute Nachrichten. Die Ergebnistabelle unter „Bekannte Ergebnisse" zeigt, wie man es aufzeichnet.

Wenn Sie den abgedeckten Code absichtlich ändern

1. Ändern Sie den Modellschritt im gleichen Commit wie den Code und behalten Sie den Kommentar, der die Funktion benennt.
2. Wenn Ihre Änderung ein Ergebnis behebt, fügen Sie die Korrektur als Code in das Modell ein, nicht als Schalter: Löschen Sie die Fix*-Konstante, lassen Sie den Schritt sich wie der neue Code verhalten und entfernen Sie den Schalter aus jeder Konfiguration. Die Konfiguration des nächsten Ergebnisses wird zur Standardkonfiguration, und check.sh erhält die neuen erwarteten Ergebnisse.
3. Bevor Sie einem Bestehen vertrauen, brechen Sie den Code absichtlich in einer Testkopie, spiegeln Sie den Bruch im Modell wider und prüfen Sie, dass die Konfiguration ihn abfängt. Wenn Sie zum Beispiel AND epoch = $3 aus PgStore::save und x.ptok = store.epoch aus SaveWrites entfernen, bricht Fencing.cfg StoredEditsStay. Eine Prüfung, die Sie noch nie fehlschlagen gesehen haben, beweist nichts.
4. Führen Sie check.sh --full aus und verschieben Sie dann den Sync-Commit nach vorne.

Bekannte Ergebnisse

Jedes ist eine Race Condition im Code bei 6606714. In jedem Fall gibt der Tool-Aufruf des Agenten Erfolg zurück und die Bearbeitung ist verschwunden.

1. Eine Bearbeitung landet auf einer Kopie, die bereits ihren letzten Snapshot speichert. Server A hat das Design geladen, und ein MCP-Aufruf hat Hub::open passiert. Server B tritt bei und gewinnt das Design (ein abgelaufener Lease auf A tut dies auch). A's Tick ruft let_go auf, also markiert retire die Kopie als Retiring. Die Save-Task take_save nimmt den letzten Snapshot. Dann nimmt der Aufruf DesignHandle::edit die Sperre und committet auf die sich zurückziehende Kopie, weil edit nie auf life schaut. Die Save-Task speichert den Snapshot ohne die Bearbeitung, gibt den Lease frei, und drop_copy löscht pending. B lädt das Design ohne die Bearbeitung. Um dies in der echten App auszulösen, müssen Bearbeitungen bereits auf der Sperre des Designs warten, wenn der Tick läuft, wie mehrere Agenten, die große write_html-Aufrufe ausführen. Rückgängig, Wiederherstellen, Import und Kommentar-Aktualisierungen nehmen den gleichen Pfad.
2. Eine Bearbeitung landet auf einem Handle, das der Hub bereits aus seiner Liste entfernt hat. Ein Aufruf handle_for gibt ein Handle zurück, das nicht geladen ist. B tritt bei, und A's let_go sieht nichts geladen, also ruft es remove auf. Der Aufruf load beansprucht den Lease und lädt eine Kopie auf diesem Handle. Die loaded-Liste des nächsten Ticks kommt von der Liste des Hubs, die dieses Handle nicht mehr enthält. Also gibt der Tick den Lease frei, und das nächste Speichern der Kopie schlägt mit Fenced fehl. Dies benötigt keinen Aussetzer, nur einen beitretenden Server.
3. Der Tick verwirft eine Kopie, die nach dem Lesen durch den Tick erneut geladen wurde. Ein Server, keine Mitgliedschaftsänderung. Der Tick liest lease() (Token 1). Dann wird das Design entladen, und ein Aufruf lädt es erneut (Token 2) und commitet eine Bearbeitung. Der Tick liest held() (Token 2), sieht, dass 2 ≠ 1, und ruft drop_copy auf. drop_copy beendet die neue Kopie, einschließlich ausstehender Bearbeitung. Das Fenster ist zwei Lesevorgänge weit, also ist es schmal, aber es läuft bei jedem Tick.
4. Ein Server, der gerade seinen Lease verlängert hat, bedient seine veraltete Kopie. B setzt über seine Lease hinaus aus, A übernimmt das Design und speichert eine Bearbeitung. B wacht auf. Sein Tick verlängert den Heartbeat, und von diesem Moment an zählt Members::now B als lebendig und wieder als Eigentümer. Aber die let_go-Schleife ist noch nicht gelaufen. Ein Aufruf auf B lädt die noch Live-veraltete Kopie und commitet eine Bearbeitung, die später mit Fenced fehlschlägt. Es erfordert zuerst einen Aussetzer.

AllFixes.cfg prüft einen vorgeschlagenen Fix für jedes Ergebnis: edit verweigert eine Kopie, die nicht Live ist (1) oder ein Handle, das nicht aufgeführt ist (2). Der Tick verwirft eine Kopie nur, wenn ihr Token der ist, den er gelesen hat (3). Ein Server, der sich nach einer Unterbrechung verlängert hat, zählt sich selbst aus, bis er losgelassen hat (4). Mit allen vier hält AckedEditsStay bei diesen Grenzen.

Was dies nicht abdeckt

• Ein Design, zwei Server, MCP-Bearbeitungen. Rückgängig, Wiederherstellen, Import, Kommentare und Umbenennungen nehmen den gleichen Sperr-und-Commit-Pfad, sind aber nicht eigenständig modelliert. Auch nicht Hub::delete.
• Der Dateispeicher und FINITE_NODES-Übergaben (hand_off_one, adopt) und der Router.
• Hub::flush beim Herunterfahren, Journal-Kompaktierungsschwellen (COMPACT_AFTER, COMPACT_BYTES) und Recent, der Puffer hinter der Betrachter-Wiederaufnahme.
• Timing. TLC probiert jede Reihenfolge von Schritten, also zeigt das Modell, dass eine Race existiert, nicht wie oft sie auftritt. Es nimmt an, dass der eigene Lease-Timer eines Servers (Members::lapsed) nicht später abläuft, als die Datenbank seinen Heartbeat als abgelaufen zählt. Das gilt, wenn die beiden Uhren mit der gleichen Rate laufen.
• Größere Grenzen. Mehr Bearbeitungen, Lesevorgänge, Handles oder Epochen, Abstürze und fehlgeschlagene Schreibvorgänge sind nicht in den alltäglichen Konfigurationen. AllFixes.cfg bestand auch mit 1 Bearbeitung, 1 Absturz und 1 fehlgeschlagenem Schreibvorgang (3,4 Mio. Zustände). Fencing nach 18 Schritten ist noch nicht fertig: mit 1 Bearbeitung und 1 Lesevorgang bestand es 50 Mio. verschiedene Zustände und lief noch. Vertrauen Sie keinem älteren Fencing-Bestehen ohne Lesevorgang: eine Bearbeitung allein lädt nur eine Kopie, also kann nichts veralten.