Attendre que les race conditions apparaissent en production n’est pas du testing. C’est de l’espoir déguisé en diligence.
Vous pouvez faire tourner votre app pendant des semaines, surveiller vos dashboards de métriques et quand même livrer un bug de concurrence qui ne se déclenche que lorsque deux requests frappent exactement la même fenêtre d’éviction de cache. Le problème n’est pas que vous avez de la malchance. Le problème est que votre stratégie de testing repose sur le fait que le scheduler soit malveillant en votre faveur, à l’instant exact, pendant que vous avez le hasard de regarder.
Il y a une meilleure façon. Le model checking vous permet d’explorer tous les interleavings possibles de votre logique concurrente en quelques secondes, pas en jours. Il trouvera la race condition à laquelle vous n’avez pas pensé à écrire un test.
Ce que fait réellement le model checking
Le model checking n’est pas un fuzzer. Il ne jette pas des inputs aléatoires sur votre code et ne prie pas. Il construit un modèle mathématique des états possibles de votre système et les traverse de manière exhaustive.
Imaginez votre programme concurrent comme un graphe. Chaque nœud est un état : les valeurs de vos variables, le contenu de vos queues, quel thread détient quel lock. Chaque arête est une étape : un thread lisant une valeur, acquérant un mutex ou envoyant un message. Le scheduler choisit quel thread s’exécute ensuite, et ce choix fait bifurquer le graphe.
Un model checker parcourt chaque chemin dans ce graphe. Si un chemin mène à deux threads écrivant dans la même mémoire sans synchronisation, il rapporte un counterexample : la séquence exacte d’étapes qui déclenche le bug.
L’idée clé est que le model checker contrôle le scheduler. En production, vous êtes à la merci du système d’exploitation. Dans un model checker, vous êtes le système d’exploitation. Vous pouvez mettre en pause un thread avant qu’il n’exécute une ligne critique, laisser un autre thread exécuter toute sa méthode, puis reprendre le premier. Vous pouvez explorer l’interleaving qui nécessiterait un rayon cosmique et un hoquet réseau pour être reproduit dans la vraie vie.
Une race condition que les model checkers attrapent en millisecondes
Voici un bug classique : deux goroutines incrémentant un counter partagé.
package main
import (
"fmt"
"sync"
)
func main() {
var counter int
var wg sync.WaitGroup
for i := 0; i < 2; i++ {
wg.Add(1)
go func() {
defer wg.Done()
// Read, increment, write: three steps
val := counter
val++
counter = val
}()
}
wg.Wait()
fmt.Println(counter) // Expected 2, often prints 1
}Exécutez cela mille fois et il pourrait afficher 2 à chaque fois. Le scheduler n’est pas votre ennemi à la demande. Mais un model checker voit la séquence read-increment-write en trois étapes et sait : si la goroutine A lit 0, puis la goroutine B lit 0, puis les deux incrémentent et écrivent 1, le counter finit à 1 au lieu de 2.
Il n’a pas besoin de tourner pendant des jours. Il doit explorer deux branches.
Comment faire du model checking sur votre propre code
Vous n’avez pas besoin de vérifier formellement toute votre codebase pour tirer profit du model checking. La plupart des équipes obtiennent 80 % du bénéfice en modélisant les 20 % de leur code où la concurrence compte réellement.
Le workflow ressemble à ceci :
-
Isolez le composant concurrent. Retirez les HTTP handlers, les requêtes de base de données et le logging. Concentrez-vous sur la state machine : quels threads ou goroutines existent, quel shared state touchent-ils et quelles sont les primitives de synchronisation ?
-
Écrivez un modèle abstrait. Remplacez les structures de données réelles par des versions simplifiées qui capturent le comportement qui vous intéresse. Si vous vérifiez une job queue, vous n’avez pas besoin du payload réel du job. Vous avez besoin d’une queue, de workers et d’un flag indiquant si un job est en cours.
-
Définissez les properties que vous voulez maintenir. Ce sont vos invariantes. « Deux workers ne traitent jamais le même job. » « Un job ne se perd jamais. » « Le cache et la base de données ne sont jamais en désaccord. »
-
Laissez le model checker tourner. Il dira soit « toutes les invariantes sont maintenues » soit vous remettra un counterexample trace.
Voici à quoi ressemble un modèle minimal en Python utilisant un simple explicit-state checker :
from collections import namedtuple
# Abstract model of a counter with two threads
State = namedtuple('State', ['counter', 'pc1', 'pc2'])
def successors(state):
"""Return all states reachable in one step."""
results = []
c, pc1, pc2 = state
# Thread 1: three-step increment
if pc1 == 0:
results.append(State(c, 1, pc2)) # read
elif pc1 == 1:
results.append(State(c, 2, pc2)) # increment
elif pc1 == 2:
results.append(State(c + 1, 3, pc2)) # write
# Thread 2: three-step increment
if pc2 == 0:
results.append(State(c, pc1, 1))
elif pc2 == 1:
results.append(State(c, pc1, 2))
elif pc2 == 2:
results.append(State(c + 1, pc1, 3))
return results
def check():
initial = State(0, 0, 0)
visited = set()
stack = [initial]
while stack:
state = stack.pop()
if state in visited:
continue
visited.add(state)
# Invariant: if both threads finished, counter must be 2
if state.pc1 == 3 and state.pc2 == 3 and state.counter != 2:
print(f"BUG: counter={state.counter}")
return
stack.extend(successors(state))
print("No race condition found in model.")
check()Ce n’est pas de qualité production. Ce sont vingt lignes de Python qui démontrent l’idée. Un vrai model checker comme TLA+, Spin ou mCRL2 gère la déduplication d’états, les properties de logique temporelle et la partial-order reduction pour que vous puissiez vérifier des systèmes avec des millions d’états. Mais le modèle mental est le même : encodez votre système, énoncez les invariantes, explorez.
L’inconvénient : l’explosion de l’espace d’états
Le model checking n’est pas gratuit. Si vous avez quatre threads, chacun avec dix pas possibles suivants, votre graphe d’états croît de manière exponentielle. Ajoutez un entier 64 bits et l’espace d’états devient littéralement incheckable.
La solution est l’abstraction. Vous ne modélisez pas votre cache réel. Vous modélisez « le cache a la key » ou « le cache n’a pas la key ». Vous ne modélisez pas votre base de données réelle. Vous modélisez « committed » ou « uncommitted ».
C’est la partie qui fait trébucher les gens. Ils essaient de faire du model checking sur leur vrai code et le checker tourne indéfiniment. Puis ils abandonnent complètement le model checking, ce qui est comme abandonner les unit tests parce que vous avez essayé de tester toute l’application en un seul test case.
La discipline est : modélisez la concurrence, pas la business logic. Si votre race condition dépend de la valeur exacte d’un user ID, vous avez déjà perdu. Les race conditions se produisent à cause de l’interleaving, pas à cause des valeurs de données.
Des outils qui fonctionnent réellement
Si vous voulez commencer à faire du model checking sur du vrai code, vous avez des options.
Pour Go : gosim vous permet d’exécuter des programmes Go avec un scheduler déterministe que vous contrôlez depuis un model checker. Il trouvera l’interleaving qui brise vos hypothèses sur sync.Mutex.
Pour Rust : shuttle est un framework de testing de concurrence déterministe d’AWS Labs. Il exécute votre code async des milliers de fois avec différents choix de scheduler et trouvera des races que loom (un autre outil excellent) vérifie au niveau du memory model.
Pour les systèmes distribués : TLA+ est le choix de calibre industriel. Amazon l’a utilisé pour trouver des bugs dans DynamoDB et S3 avant leur livraison. La courbe d’apprentissage est réelle, mais le retour sur investissement pour les systèmes critiques est mesurable.
Pour un démarrage en douceur : Écrivez un script Python comme celui ci-dessus. Cela prend une heure, cela trouve des bugs et cela construit l’intuition qui rend TLA+ moins mystérieux quand vous en avez besoin.
Ce que cela ne remplace pas
Le model checking trouve des logic errors dans du code concurrent. Il ne trouve pas de performance regressions, de memory leaks ou de bugs qui n’apparaissent que sous charge de production. Il ne vous dira pas que votre contention de mutex explose à 10 000 requests par seconde.
Utilisez-le aux côtés du stress testing, pas à sa place. Le stress testing vous dit si votre système survit à la charge. Le model checking vous dit si votre système survit aux interleavings que cette charge crée.
Par où commencer
Choisissez un composant concurrent qui vous a déjà mordu auparavant. Une job queue, un connection pool, un rate limiter. Écrivez les invariantes en plain English. Puis passez un après-midi à construire un tout petit modèle.
Vous trouverez probablement un bug dont vous ignoriez l’existence. Ou vous gagnerez en confiance que le bug qui vous inquiétait ne peut pas se produire. L’un ou l’autre résultat vaut plus qu’une autre semaine à regarder des graphes de production et à espérer.
Si vous voulez une prochaine étape concrète, le tutoriel Learn TLA+ vous mènera de zéro à vérifier un protocole de consensus distribué en un week-end. Pour Go et Rust, ajoutez shuttle ou loom à votre test suite et exécutez-le en CI. La première fois qu’il attrape une race avant la code review, vous vous demanderez pourquoi vous avez jamais fait confiance au scheduler pour faire votre testing à votre place.