Komponenten-Lebenszyklus und Entladereihenfolge

论文版本948a07b (main)

Revertible Effects lösen "Rückgängigmachen", Reactive Coeffects lösen "Wahrnehmen von Abhängigkeitsänderungen". Damit beide auf einer Komponenteninstanz koordiniert ablaufen, ist ein vollständiger Lebenszyklus-Zustandsautomat nötig. Das Papier §4.3 gibt diesen Mechanismus; die Provider/Consumer-Entladereihenfolge ist das wichtigste Engineering-Detail.

Vollständiger Zustandsautomat

[Originale Schlussfolgerung des Papiers §4.3 Def 49] Der vollständige Lebenszyklus-Zustandsautomat einer Komponente (Fiber):

Die sieben L-Primitive:

Primitiv	Auslöser	Semantik
L-Begin	target ≠ ⊥ und Fiber in Inactive	tritt in Reloading ein, zeichnet den Committed View auf, startet den Effect-Iterator
L-Iter	In Reloading, target = ω, Iterator liefert Just(i')	Wendet den Effect einer Iteration an, komponiert den Inverse in den Akkumulator
L-Finish	In Reloading, Iterator liefert Nothing	Alle Effects installiert, tritt in Active ein
L-Divert	In Reloading, target ≠ ω (Abhängigkeit geändert)	Bricht/Landet die aktuelle Iteration, tritt in Unloading ein (entweder abort, oder land dann unload)
L-Raise	Iteration wirft Fehler ξ	tritt mit ξ in Unloading ein; das folgende L-Unload wendet den vorhandenen Akkumulator an
L-Leave	In Active, target ≠ ω	Markiert Unloading, wendet aber keinen Inverse an; stellt Coeffect-Bereitstellung ein
L-Unload	In Unloading, ¬ relied_n(γ)	Wendet Akkumulator g an, tritt in Inactive ein

Entladereihenfolge von Provider und Consumer

[Originale Schlussfolgerung des Papiers §4.3.1] Dies ist einer der wichtigsten Engineering-Mechanismen des Papiers. Das L-Unload des Basis-Kalküls legt "Provision entfernen" und "Inverse ausführen" zusammen, ohne ein Intervall für das Teardown des Consumers zu lassen. Wenn der Provider direkt den Inverse anwendet, um Ressourcen freizugeben, während ein Consumer noch die Abhängigkeit des Providers nutzt, kommt es zu Abstürzen wie "der Datenbank-Verbindungspool wurde geschlossen, aber die Transaktion ist noch nicht committet".

Das Papier führt einen Unloading-Zwischenzustand und einen Guard ¬ relied_n(γ) (kein Fiber hängt mehr von n ab) ein, um die richtige Reihenfolge zu garantieren:

1. L-Leave: Provider n markiert Unloading, stellt den Coeffect nicht mehr bereit (sein σ verlässt die Union von σ_γ), aber behält seinen eigenen Committed View und seinen Inverse unangetastet;
2. Consumer m erkennt, dass seine Abhängigkeit gleich verschwindet (Target View wird ⊥ oder verweist auf einen anderen Fiber);
3. Consumer m nutzt die alte Abhängigkeit aus seinem Committed View, um das Cleanup abzuschließen — weil σ_γ nur Active Fibers vereinigt, ist das Binding eines Unloading-Fibers für andere Fibers unsichtbar, aber der Committed View des Consumers zeigt noch auf ihn;
4. L-Unload läuft, sobald der Guard ¬ relied_n(γ) erfüllt ist — d. h. alle Consumer, die von n abhängen, haben sich deaktiviert;
5. Provider n führt erst dann seinen eigenen Inverse aus und gibt Ressourcen frei.

Dieser Mechanismus löst:

• Vor dem Schließen des Pools auf Rückgabe der Verbindungen warten
• Vor dem Schließen der Datenbank auf Commit der Transaktionen warten
• Vor dem Entladen eines Tool Providers auf Agents warten, die ihn noch nutzen
• Kaskadierendes Cleanup von Kindkomponenten beim Verlassen des Vaters

[Originale Schlussfolgerung des Papiers §4.4.4 Thm 66] Der Guard kann nicht deadlocks: σ_γ vereinigt nur Active Fibers; sobald L-Leave n markiert, verlässt seine Tabelle σ_γ, kein Target View kann mehr auf n zeigen, und alle Consumer, die auf n committet waren, werden in ihr eigenes Teardown gezwungen; der Abhängigkeitsgraph propagiert entlang der ≺-Relation nach unten, und Azylklizität + Endlichkeit garantieren die Guard-Freigabe (siehe das Progress-Theorem).

Inertia: Was passiert, wenn sich Abhängigkeiten während asynchronen Ladens ändern?

[Originale Schlussfolgerung des Papiers §4.3.3] Moderne Effects sind oft asynchron (Fetch, Datei-IO, Sub-Agent-Aufrufe). Sobald eine Iteration im Flug ist (ein async Future), muss sie landen, sie kann nicht abgebrochen werden. Wenn sich der Target View während des Flugs ändert, kann L-Divert nur den Zweig "landen und dann entladen" wählen; er kann nicht "die Iteration abbrechen" — sobald eine Iteration an ein Future committet wurde, ist sie nicht abbrechbar.

Drei verwandte Konzepte:

• Inertia: das Handle der im-Flug-Transition, nicht abbrechbar, man kann nur auf die Landung warten;
• Iteration Boundary: die Granularität, bei der L-Divert eingreift — Target-Änderung wird nur an Iterationsgrenzen geprüft;
• Partial Rollback: der akkumulierte Inverse wird angewendet, der unvollständige Teil wird zurückgerollt;
• Reload und Unload verkettet: nach Abschluss von reload, falls Target sich geändert hat, Verkettung in unload; nach Abschluss von unload, falls Target sich geändert hat, Verkettung in reload (Algorithm 5).

Dieser Mechanismus garantiert, dass beim asynchronen Laden von Komponenten niemals ein "halb alt, halb neu"-Zustand entsteht — entweder wird Active vollständig erreicht, oder die Komponente tritt über L-Divert/L-Raise in Unloading ein und rollt vollständig zurück (entspricht dem Resolution-Coherence-Theorem).

Theorie→Implementierung-Entsprechung

[Originale Schlussfolgerung des Papiers §5.1 Table 2] Mapping von formalen Konzepten des Papiers zur Cordis-Implementierung:

Theoretisches Konzept	Cordis-Implementierung
Unified Context Γ∞	ctx, First-Class-Kontext
Revertible Effect	ctx.effect(callback)
Coeffect-Registrierung und -Zugriff	ctx.set(key, value) / ctx.get(key)
Component Instantiation	ctx.use(component, config)
Dependency Specification	fiber.inject (das theoretische d)
Inverse Accumulator	fiber.dispose
Committed View	fiber.committed
Target View	fiber.target (von refresh neu berechnet)
Isolation	ctx.isolate(key, realm)
Interception	ctx.intercept(key, metadata)
Inertia	fiber.inertia (Handle der im-Flug-Transition)
Lifecycle State	fiber.state (LOADING=Reloading, FAILED=Inactive(ξ))

Unterschied zwischen Fiber und React Fiber

[Aus dem Papier abgeleitete Inferenz] Def 44 des Papiers definiert ein Fiber als eine Instanziierung einer Komponente, die (d, p, e, π, σ, τ, θ) trägt — Eltern-Fiber, eigene Coeffect-Tabelle, Retirement-Marker, Lebenszyklusstatus. Es teilt nur den Namen mit React Fiber, nicht das Konzept: React Fiber ist die interne Reconciliation-Einheit von React und trägt den Traversierungszustand des Komponentenbaums; Cordis Fiber ist eine Komponenteninstanz im dynamischen Kompositionskalkül und trägt den Effect-Akkumulator, den Committed View und den Lebenszyklus-Zustandsautomat. Beide leihen die Bedeutung "leichter Ausführungsstrang" des Wortes "fiber", aber die theoretischen Rahmen sind völlig unterschiedlich.

Als Nächstes betrachten wir, was dieser Mechanismus auf metatheoretischer Ebene garantiert: Engineering-Übersetzung der formalen Theoreme.