Qu’est-ce qu’une condition de concurrence ?
Une condition de concurrence (en anglais race condition) est une faute qui n’apparaît que si deux processus s’exécutent dans un certain ordre. Un test la rate presque toujours. SPIN essaie tous les ordres et montre celui qui échoue.
Deux clients d’une banque déposent chacun 1 euro sur le même compte, en même temps. Le solde devrait valoir 2. Parfois il vaut 1.
À la fin de cette leçon
Remarque
Je peux trouver, dans une trace de SPIN, l’ordre qui fait échouer deux processus.
Mots-clés
| Mot | Ce que ça veut dire | Exemple |
|---|---|---|
| Processus | un programme qui s’exécute en même temps que d’autres | |
| Variable partagée | une variable que plusieurs processus lisent et écrivent | solde |
| Entrelacement | un ordre possible des pas de plusieurs processus | |
| Condition de concurrence | une faute qui dépend de l’ordre des pas | |
| Promela | le langage dans lequel on décrit un modèle pour SPIN | |
| Trace | la liste des pas qui mènent à l’échec |
Les cellules que les étudiants remplissent restent vides dans cet aperçu.
Chaque client lit, puis écrit
Le modèle décrit deux clients. Chacun lit le solde dans lu, écrit lu + 1 dans le solde, puis compte qu’il a fini. Ce sont trois pas.
Un troisième processus, controle, attend que les deux aient fini. Il affirme alors, avec assert, que le solde vaut 2. Les deux Runs écrivent ce fichier dans un dossier à vous, essais.
Le modèle en Promela
byte solde = 0;
byte fini = 0;
active [2] proctype client() {
byte lu;
lu = solde;
solde = lu + 1;
fini++;
}
active proctype controle() {
fini == 2;
assert(solde == 2);
}Créer un dossier pour vos essais
mkdir -p essaisAffichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Écrire le modèle dans un fichier
printf '%s\n' 'byte solde = 0;' 'byte fini = 0;' 'active [2] proctype client() {' ' byte lu;' ' lu = solde;' ' solde = lu + 1;' ' fini++;' '}' 'active proctype controle() {' ' fini == 2;' ' assert(solde == 2);' '}' > essais/compte.pmlAffichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Les pas se mélangent de plusieurs façons
Les deux clients avancent en même temps. Entre deux pas de l’un, l’autre peut faire un pas, ou plusieurs. Chaque mélange possible est un entrelacement.
Avec trois pas par client, il y a 20 entrelacements. Le Run calcule 6 × 5 × 4 divisé par 3 × 2 × 1. Un test en essaie un ou deux. SPIN les essaie tous.
Compter les entrelacements
echo $((6 * 5 * 4 / (3 * 2 * 1)))Affichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Exemple travaillé : deux ordres
| Pas | Ordre calme : A puis B | Ordre mêlé : A et B se croisent |
|---|---|---|
| 1 | A lit solde (0) | A lit solde (0) |
| 2 | A écrit 1 | B lit solde (0) |
| 3 | B lit solde (1) | A écrit 1 |
| 4 | B écrit 2 | B écrit 1 |
| Solde à la fin | 2 : correct | 1 : un dépôt est perdu |
Les cellules que les étudiants remplissent restent vides dans cet aperçu.
Faire chercher l’erreur par SPIN
spinrun essais/compte.pml | grep -E "violated|errors"Affichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
La trace montre l’ordre qui échoue
Quand SPIN trouve une erreur, il garde la liste des pas qui y mènent, une trace, dans un fichier à côté du modèle. La commande spin -t -p la rejoue pas à pas.
Le Run affiche les six premiers pas. Cherchez les deux lignes lu = solde. Elles passent avant toute ligne solde = ....
Rejouer les six premiers pas de la trace
spin -t -p essais/compte.pml | head -n 6Affichée ici, non exécutée. Créez un compte gratuit pour appuyer sur Exécuter et la saisir dans le terminal de votre propre labo.
Erreur fréquente
Attention
Beaucoup de gens pensent qu’on trouve une condition de concurrence en relançant le programme plusieurs fois. Si le mauvais ordre arrive une fois sur un million, mille essais ne le voient pas. SPIN ne tire rien au hasard : il parcourt tous les ordres, donc il ne le rate pas.
Pour aller plus loin
Copiez le fichier dans essais/compte3.pml. Avec sed -i, changez active [2] en active [3], fini == 2 en fini == 3 et solde == 2 en solde == 3.
Lancez spinrun sur la copie. Dites si SPIN trouve encore une erreur, et pourquoi il a fallu changer trois valeurs.