Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

ADR-058 — loom : activation du modèle de concurrence (outil de vérification test-only)

Statut : Accepté (2026-07-01, par délégation d’autonomie BDFL pour ce lot ; gravé pour revue a posteriori). RFC de structure (ADR-015). Companion de ADR-030 (dépendances test-only, jamais livrées), ADR-021 (EINTR remonté, la boucle EST la reprise), ADR-031 (la vraie garantie = couverture per-crate, pas un plancher global), et de la roadmap docs/roadmap-couche1-libc-pal-fr.md (§3.1).

Catégorie : Outillage de vérification (test-only). Pas de surface livrée, pas d’impact ABI.

Contexte

La variance run-to-run de la couverture lignes (95,89 ↔ 96,12 %, qui a forcé le plancher 96→94, #189) provient de branches de contention concurrentes (chemins LOCKED/ LOCKED_CONTENDED des primitives futex) dont l’exécution dépend de l’ordonnancement : une ligne est couverte certains runs seulement. Un test classique ne peut pas forcer déterministe­ment un entrelacement précis.

loom (projet tokio-rs) est l’outil Rust de référence pour cela : sous --cfg loom, il remplace le modèle mémoire (atomiques, UnsafeCell, threads) par un ordonnanceur qui explore exhaustivement tous les entrelacements d’un modèle borné, et signale toute violation (course de données, non-exclusion). Il prouve la sûreté d’un protocole concurrent, là où un test ordinaire ne fait qu’échantillonner un ordonnancement.

Le pré-câblage existait déjà (workspace : cfg(loom) déclaré + alias d’atomique commuté ; air-sys-syscall : un modèle loom_refcount dormant), mais la dépendance n’était pas activée — le commentaire du Cargo.toml de tête notait explicitement « décision de gouvernance Principe 6 / ADR-024 en attente ». Cette ADR tranche cette attente.

Décision

  1. Activer loom comme outil de modèle de concurrence, dépendance test-only tirée uniquement sous --cfg loom ([target.'cfg(loom)'.dependencies]), hors du graphe de build normal — donc jamais livrée (ADR-030). Ce n’est pas une exception à la règle des 80 % (ADR-024, qui vise les dépendances de production) : loom est un outil de vérification, au même titre que proptest (déjà dev-dep du workspace, sans entrée EXCEPTIONS.md). Il n’entre donc pas dans docs/EXCEPTIONS.md. Licence MIT (liste blanche deny.toml).

  2. Idiome d’aliasing (recommandation loom, déjà l’intention du commentaire workspace) : le même code de production est exercé sous loom et en production, via un alias d’atomique commuté core/loom. Seul l’AirMutex d’air-thread est modélisé dans ce premier lot ; AirRwLock/AirSemaphore (et les autres primitives) suivront — d’où un alias local à l’AirMutex, pas global.

  3. Shim de blocage sous loom. loom ne modélise pas futex(2). Le chemin contendu (futex_wait) est remplacé, sous --cfg loom, par un réveil coopératif (loom::thread::yield_now) et le réveil (futex_wake) par un no-op : la boucle du chemin lent relit l’état à sa prochaine planification (un futex_wait a toujours le droit de revenir « spurious » — la boucle EST la reprise, ADR-021 §2). Ce modèle est sound pour la SÛRETÉ (l’exclusion mutuelle ne dépend que de la sémantique atomique CAS/swap, fidèlement modélisée par loom).

  4. Garde-fou de fidélité (non négociable). loom prouve la sûreté (exclusion mutuelle, absence de course sur la donnée protégée) ; il ne prouve pas la vivacité (le réveil futex réel), qui reste validée on-target (selftest 2 arches + stress). Un modèle loom ne remplace jamais la preuve on-target — il ajoute une garantie déterministe sur le protocole atomique. (Piège du mock : une couverture verte sur un modèle simplifié ne vaut pas exécution réelle.)

  5. Tests réguliers hors du run loom. Les modules #[cfg(test)] d’air-thread qui instancient des primitives sont gardés #[cfg(all(test, not(loom)))] (ils créeraient des atomiques loom hors loom::model → panique). Sous --cfg loom, seul mod loom_airmutex s’exécute.

  6. Invocation (documentée, pas dans la barrière bloquante pour l’instant) :

    RUSTFLAGS="--cfg loom" cargo test -p air-thread --lib --release loom_airmutex

    Un job CI loom optionnel (hors barrière pré-merge) pourra suivre quand plusieurs primitives seront modélisées.

Conséquences

  • Positif : les branches de contention de l’AirMutex sont désormais couvertes par construction (tous les entrelacements), pas au hasard de l’ordonnancement → attaque directe de la variance de couverture. Base réutilisable (le shim futex-loom sert aussi air-alloc, AirRwLock, AirSemaphore).
  • Coût : sous --cfg loom (jamais un build normal), les tests réguliers sont désactivés ; un recompile complet sous le cfg est nécessaire. Le pré-câblage loom_refcount dormant d’air-sys-syscall émet quelques warnings sous loom (pré-existant, hors périmètre de ce lot).
  • Neutre : zéro impact sur les builds de production, la couverture mesurée (le code cfg(loom) n’est pas compilé hors loom), l’ABI, la cible *-linux-air.

Alternatives rejetées

  • Rendez-vous déterministe par test (barrières/atomiques dans le test) : marche au cas par cas (déjà employé, #187) mais ne systématise pas et n’explore pas l’espace des entrelacements. Complémentaire, pas substitut.
  • Réécrire un ordonnanceur maison : refaire loom, coûteux et moins éprouvé.
  • shuttle (AWS) : exploration randomisée-rejouable plutôt qu’exhaustive ; loom (exhaustif, borné) est préférable pour prouver la sûreté d’un petit protocole.

Suite

  • Étendre les modèles loom à AirRwLock, AirSemaphore, puis au verrou futex d’air-alloc (même shim). Puis, quand plusieurs modèles existent, envisager un job CI loom optionnel.
  • Nettoyer les warnings loom dormants d’air-sys-syscall (loom_refcount) — hors périmètre ici.