Cycle de vie du composant et ordre de déchargement

论文版本948a07b (main)

Les Revertible Effects résolvent « réverter » ; les Reactive Coeffects résolvent « percevoir les changements de dépendance ». Pour que les deux se coordonnent sur une instance de composant, une machine à états complète du cycle de vie est nécessaire. L'article §4.3 donne ce mécanisme, et l'ordre de déchargement Provider/Consumer en est le détail d'ingénierie le plus important.

Machine à états complète

[Conclusion originale de l'article §4.3 Def 49] La machine à états complète du cycle de vie d'un composant (fiber) :

Les sept primitives L- :

Primitive	Déclencheur	Sémantique
L-Begin	target ≠ ⊥ et fiber en Inactive	Entre dans Reloading, enregistre le committed view, démarre l'effect iterator
L-Iter	En Reloading, target = ω, l'iterator produit Just(i')	Applique l'effect d'une iteration, compose l'inverse dans l'accumulateur
L-Finish	En Reloading, l'iterator produit Nothing	Tous les effects installés, entre dans Active
L-Divert	En Reloading, target ≠ ω (dépendance changée)	Aborte/atterrit l'iteration courante, entre dans Unloading (soit abort, soit land puis unload)
L-Raise	L'iteration lève une erreur ξ	Entre dans Unloading en portant ξ ; le L-Unload suivant applique l'accumulateur existant
L-Leave	En Active, target ≠ ω	Marque Unloading mais n'applique pas l'inverse ; arrête de fournir le coeffect
L-Unload	En Unloading, ¬ relied_n(γ)	Applique l'accumulateur g, entre dans Inactive

Ordre de déchargement Provider et Consumer

[Conclusion originale de l'article §4.3.1] C'est l'un des mécanismes d'ingénierie les plus importants de l'article. Le L-Unload du calcul de base met « retirer la provision » et « exécuter l'inverse » ensemble, sans laisser d'intervalle pour le teardown du consumer. Si le provider applique directement l'inverse pour libérer des ressources pendant qu'un consumer utilise encore la dépendance du provider, on obtient des crashes comme « le pool de connexions à la base de données est fermé alors qu'une transaction n'est pas encore committée ».

L'article introduit un état intermédiaire Unloading et un guard ¬ relied_n(γ) (aucun fiber ne dépend plus de n) pour garantir l'ordre correct :

1. L-Leave : le Provider n marque Unloading, cesse de fournir le coeffect (son σ quitte l'union de σ_γ), mais conserve intact son propre committed view et son inverse ;
2. Le Consumer m détecte que sa dépendance est sur le point de disparaître (target view devient ⊥ ou pointe vers un autre fiber) ;
3. Le Consumer m utilise l'ancienne dépendance de son committed view pour terminer son nettoyage — parce que σ_γ n'unionne que les fibers Active, le binding d'un fiber Unloading est invisible pour les autres fibers, mais le committed view du consumer pointe encore vers lui ;
4. L-Unload s'exécute quand le guard ¬ relied_n(γ) est satisfait — c.-à-d. tous les consumers dépendant de n se sont désactivés ;
5. Le Provider n exécute alors seulement son propre inverse et libère les ressources.

Ce mécanisme résout :

• Attendre le retour des connexions avant de fermer le pool
• Attendre le commit des transactions avant de fermer la base de données
• Attendre les Agents utilisant encore un Tool Provider avant de le décharger
• Nettoyage en cascade des composants enfants quand le parent sort

[Conclusion originale de l'article §4.4.4 Thm 66] Le guard ne peut pas deadlock : σ_γ n'unionne que les fibers Active ; une fois L-Leave marque n, sa table quitte σ_γ, aucun target view ne peut plus pointer vers n, et tous les consumers committés vers n sont forcés dans leur propre teardown ; le graphe des dépendances se propage vers le bas le long de la relation ≺, et acyclicité + finitude garantit la libération du guard (voir le théorème de Progress).

Inertia : que se passe-t-il si la dépendance change pendant un chargement asynchrone ?

[Conclusion originale de l'article §4.3.3] Les effects modernes sont souvent asynchrones (fetch, IO fichier, appels de sous-Agent). Une fois qu'une iteration est en vol (un async Future), elle doit atterrir, elle ne peut pas être abortée. Quand le target view change pendant le vol, L-Divert ne peut choisir que la branche « atterrir puis unload » ; il ne peut pas « aborter l'iteration » — une fois qu'une iteration est committée vers un Future, elle ne peut être annulée.

Trois concepts liés :

• Inertia : le handle de transition en vol, non annulable, on ne peut qu'attendre l'atterrissage ;
• Iteration boundary : la granularité à laquelle L-Divert intervient — le changement de target n'est vérifié qu'aux frontières d'iteration ;
• Partial rollback : l'inverse accumulé est appliqué, la partie inachevée est révertie ;
• reload et unload interlinkés : après achèvement de reload, si le target a changé, enchaîne vers unload ; après achèvement de unload, si le target a changé, enchaîne vers reload (Algorithm 5).

Ce mécanisme garantit qu'un composant chargé de façon asynchrone ne se retrouve jamais « à moitié ancien, à moitié nouveau » — soit il termine en entrant dans Active, soit il entre dans Unloading via L-Divert/L-Raise et se révertit complètement (correspond au théorème de Resolution Coherence).

Correspondance théorie→implémentation

[Conclusion originale de l'article §5.1 Table 2] Mapping entre les concepts formels de l'article et l'implémentation Cordis :

Concept théorique	Implémentation Cordis
Unified Context Γ∞	ctx, contexte de première classe
Revertible Effect	ctx.effect(callback)
Enregistrement et accès de coeffect	ctx.set(key, value) / ctx.get(key)
Component Instantiation	ctx.use(component, config)
Dependency Specification	fiber.inject (le d théorique)
Inverse Accumulator	fiber.dispose
Committed View	fiber.committed
Target View	fiber.target (recalculé par refresh)
Isolation	ctx.isolate(key, realm)
Interception	ctx.intercept(key, metadata)
Inertia	fiber.inertia (handle de transition en vol)
Lifecycle State	fiber.state (LOADING=Reloading, FAILED=Inactive(ξ))

Différence entre Fiber et React Fiber

[Inference basée sur l'article] La Def 44 de l'article définit un fiber comme une instanciation d'un composant, portant (d, p, e, π, σ, τ, θ) — fiber parent, sa propre table de coeffect, marqueur de retirement, état du cycle de vie. Il partage seulement le nom avec React Fiber, pas le concept : React Fiber est l'unité interne de reconciliation de React, portant l'état de parcours de l'arbre des composants ; Cordis Fiber est une instance de composant dans le calcul de composition dynamique, portant l'accumulator d'effects, le committed view et la machine à états du cycle de vie. Les deux empruntent le sens « thread d'exécution léger » du mot « fiber », mais les cadres théoriques sont entièrement différents.

Ensuite, ce que ce mécanisme garantit au niveau métathéorique : Traduction ingénierie des théorèmes formels.