TLA+ pour les  ingénieurs logiciels

TLA+ pour les ingénieurs logiciels Frédéric G. MARAND / [email protected]
OpenSourceExperience Paris 2025-12 Nouveautés 4ème édition - La version Clarke - GenAI - Retours d’expérience

Qui suis-je ? • Architecte / lead dev consultant pour
OSInet.fr • Spécialité: scale up de backends • « Stacks » de référence: ◦ Go, Kafka, AWS, Terraform ◦ PHP, Drupal, MongoDB • Domaines techniques: media, paiements, infrastructure de plateforme • Domaines métier: ◦ Média: LeFigaro, Radio France, FranceTV… ◦ Retail: Deliveroo, LeBonCoin ◦ Gouvernement; Medicare, France.fr, CNRS, Sante.fr, ...

Plan 1. Introduction 2. Fondements logiques 3. Les bases de
TLA+ 4. PlusCal 5. Mise en pratique: GenAI, expériences

1. Introduction 1. Qu’est-ce que TLA+ ? 2. Pourquoi utiliser
des méthodes formelles ? 3. « Success stories » 4. Proposition de valeur

1.1 Qu’est-ce que TLA+ ? • Un langage de spécification
formelle pour les systèmes concurrents et répartis ◦ PAS un langage de programmation • Créé par Leslie Lamport (LaTeX) ◦ TLA+ a été créé comme une extension LaTeX pour la logique formelle • Fondement mathématique pour la description de systèmes ◦ Basé sur la théorie des ensembles de Zermelo–Fraenkel avec l’axiome du choix (ZFC) • Conçu pour décrire le comportement des systèmes, pas leur mise en œuvre. ◦ Donc pas prévu pour être transpilé dans les langages de programmation courants

Prix Turing: « Pour ses contributions fondamentales à la théorie
et la pratique des systèmes répartis et concurrents, notamment l’invention des concepts de causalité, horloges logiques, sûreté et vivacité, des automates à états finis, et de la cohérence séquentielle" Image: Autoportrait dans son cours TLA+ Leslie Lamport

1.2 Pourquoi l’utiliser ? • Éviter les bogues les plus
coûteux: les erreurs de conception ◦ La meilleure implémentation possible d’une conception avec une situation de compétition (race condition) ne peut pas l’éviter sans reconception ◦ Quant aux implémentations réelles… • Vérifier les algorithmes et protocoles complexes ◦ Les modèles TLA+ peuvent décrire toutes les combinaison temporelles pertinentes • Compléter les logiques de test traditionnelles ◦ Les test unitaires ne testent que les cas que les développeurs ont imaginé ◦ Les tests en fuzzing ne testent que les cas que les développeur ont été en mesure de produire à partir d’entrées pseudo-aléatoires

1.3 « Success stories » • Amazon S3: découverte de
bogues critiques dans les protocoles internes ◦ How formal methods helped AWS to design amazing services • Azure Cosmos DB: vérification de cohérence des protocole ◦ Understanding Inconsistency in Azure Cosmos DB with TLA+ • Apache Kafka: protocole de réplication validé ◦ KIP-966: KRaft, synchronisation des brokers sans Zookeeper, standard dans Kafka 4.0 ◦ Mais aussi d’autre KIPs comme KIP-848 : nouveau protocole de rééquilibrage des groupes de consommation • Pour tous la modélisation a évité des mois de déboguage et des incidents ◦ Après une première réussite, le projet Kafka a généralisé la modélisation pour les KIP complexes

1.4 Proposition de valeur • Coût des bogues - ordre
de grandeur: ◦ À la conception: 1x ◦ Durant le développement: 10x ◦ En production: 100x • TLA+ découvre les bogues que les tests ignorent ◦ Les tests privilégient le « happy path », la modélisation privilégie les situations d’erreur ◦ Même le fuzzing a tendance à trouver les bogues causant des crashes, pas les violations d’invariants • Valeur particulière pour les systèmes répartis et concurrents ◦ La compréhension humaine de la temporalité relative d’actions simultanées est faible

2. Fondement logique 1. Logique traditionnelle et temporelle 2. Les
systèmes comme états 3. Actions: les transitions d’état 4. Exemple simple example: Feux de circulation 5. Propriétés temporelles: sûreté et vivacité 6. Les bases de la vérification de modèles

2.1 Logique traditionnelle et temporelle • ∀P: P = P

• Est-ce TOUJOURS vrai ?

• Est-ce TOUJOURS Vrai ? • Et si les deux évaluations de P ont lieu à deux instants différents ?

• Est-ce TOUJOURS Vrai ? • Et si les deux évaluations de P ont lieu à deux instants différents ? • Et si P = “le processus est cours d’exécution maintenant” ?

• Est-ce TOUJOURS Vrai ? • Et si les deux évaluations de P ont lieu à deux instants différents ? • Et si P = “le processus est cours d’exécution maintenant” ? • La logique traditionnelle évalue à un instant abstrait dans le temps (« maintenant »)

• Est-ce TOUJOURS Vrai ? • Et si les deux évaluations de P ont lieu à deux instants différents ? • Et si P = “le processus est cours d’exécution maintenant” ? • La logique traditionnelle évalue à un instant abstrait dans le temps (« maintenant ») • La logique temporelle ajoute la dimension temps: « maintenant » change

2.2 Les systèmes comme états • La notion qu’un prédicat
peut être évalulé à des instants différents ajoute un composant de temps quantifié (penser au temps de Planck) • Les valeurs d’un système à chacun de ces quanta de temps sont les états ◦ À l’intérieur d’un état instantané, la logique traditionnelle s’applique • Les trois familles de logique temporelle ◦ Linear Temporal Logic (Pnueli, 77): évalue les propriétés au fil de séquences d’état ▪ Combinée avec la logique du premier ordre (alias calcul des prédicats), c’est la base de TLA+ et de nombreux outils dérivés ◦ Computation Tree Logic (Clarke/Emerson, 81): combine les opérateurs temporels avec des quantificateurs de chemins pour spécifier des propriétés sur un arbre calculatoire ◦ Branching Temporal Logic (multiple, 80s): évalue les propriétés sur les branches, capturant de multiples chemins futurs à partir de chaque état

2.2 Exemple: interrupteur push/pull

2.2 Exemple: interrupteur basculant: 2 actions

2.2 Exemple: interrupteur push/push: 1 action

2.3 Actions: les transitions d’état • Les actions: ◦ Définissent
comment le système fait un pas (« step ») d’un état au suivant ◦ Décrites par leurs préconditions et postconditions. ◦ Exemple: l’action « inverser » sur l’interrupteur push/push • Représentation formelle: une variable avec un symbole « prime » ◦ Précondition: Light = Off : la valeur dans l’état initial ◦ Postcondition: Light' = On : la valeur dans l’état suivant

2.4 Exemple simple: feux de circulation • En France, l’allumage
et l’extinction des feux de circulation parcourent un cycle ◦ Vert ◦ Orange ◦ Rouge ◦ recommencer

2.4 Exemple simple: feux de circulation

2.4bis Example: feux de circulation espagnols En Espagne en revanche,
le cycle des feux est différent, repassant par l’orange après le rouge. Mais ce modèle a un problème…

2.4bis Example: feux de circulation espagnols Le modèle autorise ceci:
1. Red 2. Yellow 3. Red 4. Yellow 5. … Ce n’est pas équitable!

2.4bis Example: feux de circulation espagnols Pour que le modèle
reste dans un cycle, ajoutons une autre variable au système, forçant le retour dans un cycle et ajoutant un état invisible

2.5 Propriétés temporelles: sûreté et vivacité • Les propriété de
sûreté: ◦ Garantissent que quelque chose de non désiré ne surviendra pas. ◦ Exemple: « Le feu n’est jamais au rouge et à l’orange à la fois » • Les propriétés de vivacité: ◦ Garantissent que quelque chose de désiré finira par survenir. ◦ Exemple: « Au bout d’un certain temps, le feu passera au vert » • Quiz: lequel des deux notre premier modèle de feux espagnols a-t-il manqué ?

2.5 Propriétés temporelles: sûreté et vivacité • Les propriété de
sûreté: ◦ Garantissent que quelque chose de non désiré ne surviendra pas. ◦ Exemple: « Le feu n’est jamais au rouge et à l’orange à la fois » • Les propriétés de vivacité / progression: ◦ Garantissent que quelque chose de désiré finira par survenir. ◦ Exemple: « Au bout d’un certain temps, le feu passera au vert » • Quiz: lequel des deux notre premier modèle de feux espagnols a-t-il manqué ? ◦ Pas de propriété de vivacité, le fait que le feu passerait au vert ne pouvait pas être vérifié

2.6 Les bases de la vérification de modèles • Vérification
de modèle: ◦ Technique automatique de vérification des propriétés temporelles. ◦ Explore TOUS les états accessibles et TOUTES les transitions. ◦ Outils: TLC (inclus dans TLA+), Apalache (tierce partie) • Processus: ◦ Définir le système et ses propriétés. ▪ Dans notre exemple: un INVARIANT, une PROPERTY (temporelle), et une détection d’étreinte mortelle (« deadlock ») ◦ Utiliser un vérificateur de modèle pour explorer tous les comportements possibles ◦ Le vérificateur confirme que toutes les propriétés sont toujours respectées

2.6bis Vérification du modèle de feux espagnols \* traffic_lights_spain_inv.cfg INIT
Init NEXT Next INVARIANT TypeOK PROPERTY NoRegression CHECK_DEADLOCK TRUE % tlc traffic_lights_spain_inv.tla …snip… Starting... (2025-02-23 16:58:15) Computing initial states... Finished computing initial states: 1 distinct state generated at 2025-02-23 16:58:15. Model checking completed. No error has been found. …snip… 5 states generated, 4 distinct states found, 0 states left on queue. …snip… Finished in 00s at (2025-02-23 16:58:15)

3. Bases de TLA+ 1. États et variables 2. Opérateurs
de base: ≜, ⇒, ∧, ∨, =, ∈ 3. Actions et variables primées 4. Bégaiement 5. Formules temporelles 6. Spécifications: Init /\ [][Next]_vars 7. Exemple simple: Mutex 8. Vérifier le modèle de Mutex avec TLC

3.1 États et variables • Les états: ◦ Représentent la
configuration du système à un instant donné. ◦ Définis par les valeurs des variables. • Les variables: ◦ Composants de l’état du système ◦ Typées: entiers, ensembles, séquences, etc. • Exemple: ◦ Feux simples: light (avec les valeurs Red, Green, Yellow). ◦ Feux à l’espagnole: light et going_to_green

3.2 Opérateurs de base: ≜, ⇒, ∧, ∨, =, ∈
• Affectation: ≜ ◦ Affecte des valeurs aux variables ◦ Exemple: x ≜ 5 • Implication: ⇒ ◦ Implication logique, sans causalité ◦ Exemple: A ⇒ B (si A alors B) • Conjonction: ∧ ◦ ET logique ◦ Exemple: A ∧ B (A et B) • Disjonction: ∨ ◦ OU logique ◦ Exemple: A ∨ B (A ou B) • Égalité: = ◦ Exemple: x = 5 • Appartenance: ∈ ◦ Valeur membre d’un ensemble ◦ Exemple: x ∈ {1, 2, 3}

3.3 Actions et variables primées • Variables primées: ◦ Représentent
l’état suivant d’une variable. ◦ Utilisées pour décrire les transitions d’état. • Exemple: ◦ light' = "Green" signifie que le prochain état de light est Green. • Définition d’une action: ◦ Précondition: light = "Red" ◦ Postcondition: light' = "Green"

3.4 Bégaiement • Étapes de bégaiement (« stuttering steps »):
◦ Transitions durant lesquelles l’état ne change pas ▪ Aucun système ne change d’état à une vitesse infinie (vous avez déjà attendu à un feu rouge ?) ▪ Il évolue continûment d’un état vers le même état au fil du temps: c’est le bégaiement ◦ Essentiel pour modéliser des systèmes à exécution concurrente • Exemple: ◦ Dans un système concurrent, un processus peut ne pas changer d’état pendant qu’un autre change • Répresentation: ◦ light' = light (le feu allumé demeure inchangé)

3.5 Formules temporelles • Opérateurs temporels ◦ [] (toujours, «
always » alias box): La propriété est vraie dans tous les états ◦ <> (plus tard, « eventually » alias « diamond »): La propriété sera vraie dans au moins un état futur ◦ ~> (mène à): si la première propriété est vraie, la seconde finira par le devenir • Exemple: ◦ [](light = "Red" ⇒ <> light = "Green") ▪ Toujours, le feu est rouge implique que plus tard le feu sera vert ▪ C’est une propriété de vivacité (« liveness »): le système cessera de bégayer à un certain point pour transiter vers un autre état

3.6 Spécifications • La structure d’une spécification utilise des noms
de variables conventionnels, par défaut dans un fichier CFG ◦ Init: Prédicat décrivant l’état initial ◦ Next: Relation décrivant la transition à l’état suivant, pour tout état ◦ Spec: La spécification globale • Représentation formelle: ◦ Spec == Init ∧ [][Next]_vars ◦ Init définit l’état initial, Next les transitions possibles ◦ vars est le n-uplet (séquence finie) de toutes les variables du système. • Un fichier CFG pour TLS peut soit définir INIT et NEXT, soit SPECIFICATION, ◦ Leurs noms conventionnels respectifs sont Init, Next, Spec

3.7 Exemple simple: Mutex entre deux processus

3.7 Le même mutex avec trois processus • TLC est
un vérificateur par force brute avec des optimisations intelligentes, donc le temps d’exécution dépend du nombre d’états. • Votre équipe aurait-elle identifié et codé des tests pour tous ces états ? Et pour plus de processus ?

3.7 Vérification du Mutex: le coût de balayage de l’espace
des possibles explose vite

3.7 Mutex cost: le coût explose vite - bis Pouvez-vous
deviner à quel instant j’ai lancé TLC pour vérifier un modèle ?

3.7 Exemple: un Mutex vérifiable en 50 lines ---- MODULE
mutex_sweeping ---- EXTENDS Integers, FiniteSets CONSTANT N \* Number of processes ASSUME N \in Nat \* N must be a natural number ASSUME N > 1 \* Need at least 2 processes VARIABLES flag, \* Array of flags, one per process turn \* Who's turn is it to enter critical section Proc == 1..N \* N processes: that’s sweeping vars == <<flag, turn>> Init == /\ flag = [i \in Proc |-> FALSE] \* No one wants to enter initially /\ turn = 1 \* Process 1 goes first Try(i) == \* Process i wants to enter critical section /\ flag' = [flag EXCEPT ![i] = TRUE] /\ UNCHANGED turn Give(i) == \* Process i gives turn to other process /\ flag[i] = TRUE /\ \E j \in Proc \ {i} : turn' = j \* Give turn to any other process /\ UNCHANGED flag Enter(i) == \* Process i enters critical section if it's their turn /\ flag[i] = TRUE /\ turn = i /\ \A j \in Proc \ {i} : ~flag[j] \* No other process wants to enter /\ UNCHANGED vars Exit(i) == \* Process i leaves critical section /\ flag' = [flag EXCEPT ![i] = FALSE] /\ UNCHANGED turn Next == \E i \in Proc : Try(i) \/ Give(i) \/ Enter(i) \/ Exit(i) Spec == Init /\ [][Next]_vars \* Type correctness invariant TypeOK == /\ flag \in [Proc -> BOOLEAN] /\ turn \in Proc \* Safety: No two processes in critical section simultaneously Mutex == [][\A i,j \in Proc : i # j => ~(Enter(i) /\ Enter(j))]_vars ====

3.7 Vérifier le Mutex avec TLC \* mutex_sweep.cfg SPECIFICATION Spec
CONSTANT N = 3 \* Essayez plus INVARIANT TypeOK PROPERTY Mutex CHECK_DEADLOCK TRUE Lancer la vérification avec: tlc mutex_sweep.tla • SPECIFICATION désigne la formule temporelle Spec, qui DOIT avoir cette forme: Init /\ [][Next]_vars ◦ Init démarre vrai ET Next est TOUJOURS vrai ◦ Comme vars == <<flag, turn>> ceci est du sucre syntaxique pour: Init /\ [](Next \/ (flag' = flag /\ turn' = turn)) • La valeur de N est une CONSTANT TLA+ indéfinie dans le modèle, c’est le vérifieur qui définit sa valeur à la vérification • INVARIANT signifie que TypeOK est vrai dans chaque état • PROPERTY décrit la propriété de sûreté ([]) Mutex, qui énonce qu’aucun processus ne peut être actif simultanément avec un autre. Ce pourrait aussi être une propriété de vivacité (<> ou ~>), ou d’équité (WF_Vars / SF_Vars). • CHECK_DEADLOCK garantit que le système n’a pas d’état final

4. PlusCal 1. Des spécifications au code 2. Structure des
algorithmes en PlusCal 3. Variables et affectations 4. Étapes atomiques et étiquettes 5. Algorithmes multi-processus 6. Transpilation en TLA+ Seulement dans la version longue de cette présentation !

5. Mise en pratique 1. Quand utiliser TLA+ 2. Integration
avec le développement 3. Outils logiciels 4. Débuter avec TLA+ / PlusCal 5. Un dernier conseil de la part de LearnTLA+ 6. GenAI ? 7. Retours d’expérience personnels

5.1 Quand utiliser TLA+ / PlusCal • Pour les systèmes
concurrents complexes: ◦ Conception de systèmes concurrents complexes et/ou répartis (Microsoft: XBox 360) ◦ Exemples: base de données/stockage réparti (ex: MongoDB, Cosmos DB, AWS S3), algorithmes de consensus (variantes de Paxos, Raft, KRaft, réplication Kafka), protocoles réseau (Dropbox, Azure DNS) • Pour les systèmes critiques: ◦ Lorsque la fiabilité est cruciale: systèmes financiers, soutien vital, aérospatial, défense ◦ La modélisation aide à identifier et corriger les bogues de conception avant d’investir dans l’implémentation • Durant les étapes de conception à haut niveau: ◦ Les étapes préliminaires de conception de services pour spécifier et valider le comportement du système à haut niveau et éviter d’investir dans un projet condamné à l’avance ◦ Détection précoce des défauts de conception et garantie d’une fondation solide avant le codage. • Refactorisation et Maintenance: ◦ Refactorisation et maintenance de systèmes complexes et/ou avec une couverture de test insuffisante pour garantir que les changements n’introduisent pas de nouveaux bogues ◦ Pour comprendre et vérifier l’impact des évolutions

5.2 Intégration avec le développement • Écriture de spécifications: ◦
Créer les spécifications TLA+ en même temps que les documents de conception de haut niveau ◦ Envisager PlusCal pour une traduction du code vers TLA+ plus facile • Vérification des modèles: ◦ TLC ou Apalache pour vérifier les spécifications TLA+ ◦ Exécuter TLC dans le pipeline de CI pour bloquer les erreurs aussi tôt que possible. • Génération de code: ◦ Utiliser TLA+ pour générer et vérifier les cas de tests et invariants qui pourront être utilisés dans les tests unitaires. ◦ TLA+ n’est pas transpilé en code (quoique…) mais la vérification peut guider l’implémentation • Documentation: ◦ Inclure les spécifications TLA+ dans la documentation de projet (ADR…) pour fournir une référence formelle du comportement attendu du système. ◦ Utiliser TLA+ pour documenter les présupposés, invariants, et propriétés de sûreté et vivacité. • Collaboration: ◦ Utiliser TLA+ pour faciliter la collaboration entre développeurs, architectes et autres parties prenantes techniques. ◦ La spécification fournit un langage commun non ambigue pour la discussion/négotiation des comportements et livrables. • Formation et onboarding: ◦ Former les nouveaux collaborateurs pour une compréhension cohérente des systèmes plutôt qu’une interprétation du code ◦ Utiliser les exemples/exercices TLA+ durant l’onboarding.

5.3 Outils logiciels • Fournis par la TLA+ Foundation ◦
Au 2025-12-10, la version courante est Clarke, tag 1.8.0 , publiée en 09/2025 et toujours en pré-version ◦ Les outils CLI sont fournis ensemble dans un JAR: tlatools.jar ▪ tlc2: le vérificateur de modèle - à utiliser au quotidien ▪ tlc2.REPL: un interpréteur - la grand nouveauté de Clarke, après 5 years de développement - voir le démo ▪ pcal: le transpileur PlusCal vers TLA+ ▪ tla2tex: formatteur des sources TLA+ pour LaTeX. Combiner avec pdflatex pour des rendus en PDF. ▪ tla2sany: vérificateur de syntaxe - mieux vaut utiliser le plugin de votre IDE JetBrains ou VSCode ◦ La « Toolbox » était l’IDE par défaut, basé sur Eclipse. Il n’est plus recommandé au quotidien mais utilie pour suivre les didacticiels et contient l’interface utilisateur du profileur. Fourni dans les paquets TLAToolbox*.(zip|deb) • Apalache est un vérificateur symbolique pour les grands modèles, qu’il traduit dans un format utilisateur par les résolveurs SMT • Le TLA Proof System est utile si vos modèles sont de taille infinie ◦ Un vérificateur en force brute comme TLC, par conception, ne peut pas vérifier un modèle infini ◦ Actuellement limité aux propriétés de sûreté, la validation des propriétés de vivacité est encore en travaux

5.3 Outils logiciels: l’UI profileur dans Toolbox Source: INRIA

5.4 Débuter avec TLA+ / PlusCal • Commencez petit: ◦
Débutez avec des composants de votre système à la fois petits et critiques. ◦ N’étendez l’utilisation de TLA+ qu’après avoir acquis suffisamment de confiance • Itérez: ◦ Comme un programme, un modèle change: évoluez votre modèle TLA+ par itérations pour raffiner vos spécifications et conceptions. ◦ Vérifiez vos spécification en CI au fil des évolutions pour ne pas diverger • Collaborez: ◦ Le travail d’écriture et de revue des spécifications TLA+ est un travail d’équipe: sans cela, une fois le créateur inévitablement parti, le projet perdra ses garanties ◦ Entretenez une culture de la vérification formelle.

5.5 Un dernier conseil de la part de “Learn TLA+”
« The dirty secret of formal methods is that the only way we know to scale it up is to use state machines »

5.6 GenAI ? • Cette page vieillit vite: elle a
été actualisée en 2025 Q1, Q2, Q3, Q4… • Les agents interactifs (Claude, ChatGPT, Gemini) étaient incroyablement inappropriés début 2025 ◦ Hallucinations de code incorrect, assurance de correction, et ré-émission du même code incorrect. La situation est bien meilleure pour TLA+ fin 2025, mais pas encore pour PlusCal ◦ Aucun ne « comprend » qu’un seul langage comme Pluscal a DEUX syntaxes distinctes, et ils émettent généralement de la C-syntax en l’appelant P-syntax, passant à côté des éléments syntaxiques nécessaire à du code correct • Fin 2025, les premiers outils de génération de code exécutable à partir de spécifications commencent à devenir réalité: 2026 devrait être intéressant. • À ce jour, l’utilisation pratique la plus opérationnelle est la revue de code

5.7 Retours d’expérience • Sur le premier projet, le code
échouait quand même. Mais pourquoi ? ◦ La partie modélisée, basée sur un automate, était sans bogue ◦ Mais le package Go qui la contenait ne l’était pas: ▪ J’avais oublié d’envisage ce qui se passait après l’état final de l’automate ▪ L’implémentation avait des dépendances d’observabilité. Devinez quoi… • Leçons à retenir ◦ Vérifier ce que fait le code avant l’état initial et après l’état final d’un modèle ◦ Ne pas s’arrêter au premier composant modélisé ◦ Les dépendances doivent figurer dans le modèle ◦ Parfois ajouter une simple propriété d’état additionnelle peut autoriser de grandes économies d’exécution concurrente (CPU pour le GC et le planificateur, maintenance)

Just une dernière chose … • Lisez les livres publiés
sur TLA+ (liens Amazon) ◦ Wayne Hillel “Practical TLA+” https:/ /amzn.to/3HYU7Sx ◦ Le livre original de Leslie Lamport https:/ /amzn.to/4l31t64 • Ou contactez-moi pour vos prochains projets ! ◦ LinkedIn: https:/ /linkedin.com/in/marand ◦ Bluesky: https:/ /bsky.app/profile/fgmarand.bsky.social

Mon LinkedIn Ces diapos

TLA+ pour les ingénieurs logiciels

TLA+ pour les ingénieurs logiciels

More Decks by Frédéric G. MARAND

Other Decks in Programming

Featured

Transcript

TLA+ pour les  ingénieurs logiciels

TLA+ pour les  ingénieurs logiciels