Qu’est-ce que l’exclusion mutuelle ?
L’exclusion mutuelle est la règle qui interdit à deux processus d’être en même temps dans la partie du programme qu’ils se partagent, la section critique. Un verrou la fait respecter, et SPIN vérifie qu’il le fait dans tous les ordres possibles.
Deux clients déposent de l’argent sur un même compte. Sans verrou, un dépôt peut se perdre. Avec un mauvais verrou, il peut se perdre aussi.
À la fin de cette leçon
Remarque
Je peux écrire un verrou et faire dire à SPIN qu’il ne trouve aucune erreur.
Mots-clés
| Mot | Ce que ça veut dire | Exemple |
|---|---|---|
| Section critique | la partie du programme que deux processus ne doivent pas faire ensemble | |
| Exclusion mutuelle | jamais deux processus dans la section critique | |
| Verrou | un mécanisme qui laisse un seul processus entrer à la fois | |
| Assertion | une condition que SPIN vérifie à cet endroit | assert(dedans == 1) |
| Interblocage | une situation où tous les processus attendent et aucun ne peut avancer | |
| Algorithme de Peterson | un verrou pour deux processus fait d’un drapeau chacun et d’un tour |
Les cellules que les étudiants remplissent restent vides dans cet aperçu.
Tester puis prendre un verrou est fautif
Le verrou le plus simple est une variable occupe. Un client attend qu’elle vaille 0, puis la met à 1. Ce sont deux pas.
Entre les deux, l’autre client peut passer. Un compteur dedans et une assertion, assert(dedans == 1), disent à SPIN qu’il ne doit jamais y avoir deux clients à l’intérieur.
Le client avec un verrou naïf
active [2] proctype client() {
byte lu;
occupe == 0;
occupe = 1;
dedans++;
assert(dedans == 1);
lu = solde;
solde = lu + 1;
dedans--;
occupe = 0;
fini++;
}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 du verrou naïf
printf '%s\n' 'bit occupe = 0;' 'byte dedans = 0;' 'byte solde = 0;' 'byte fini = 0;' 'active [2] proctype client() {' ' byte lu;' ' occupe == 0;' ' occupe = 1;' ' dedans++;' ' assert(dedans == 1);' ' lu = solde;' ' solde = lu + 1;' ' dedans--;' ' occupe = 0;' ' fini++;' '}' 'active proctype controle() {' ' fini == 2;' ' assert(solde == 2);' '}' > essais/verrou_naif.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.
Faire chercher l’erreur par SPIN
spinrun essais/verrou_naif.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.
Rejouer les trois premiers pas
spin -t -p essais/verrou_naif.pml | head -n 3Affiché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.
L’algorithme de Peterson protège deux processus
Chaque client lève son drapeau, puis donne le tour à l’autre. Il entre quand l’autre n’a pas levé son drapeau, ou quand c’est son tour.
Le tour ne peut désigner qu’un client à la fois, donc un seul des deux gagne. Le Run écrit ce modèle avec _pid, le numéro du client, 0 ou 1.
Exemple travaillé : deux clients arrivent ensemble
| Pas | Client 0 | Client 1 | Le tour |
|---|---|---|---|
| 1 | lève son drapeau | lève son drapeau | - |
| 2 | donne le tour au client 1 | - | 1 |
| 3 | - | donne le tour au client 0 | 0 |
| 4 | attend : le tour est à lui, il entre | attend : le tour n’est pas à lui | 0 |
Les cellules que les étudiants remplissent restent vides dans cet aperçu.
Écrire le modèle de Peterson
printf '%s\n' 'bool drapeau[2];' 'byte tour = 0;' 'byte dedans = 0;' 'byte solde = 0;' 'byte fini = 0;' 'active [2] proctype client() {' ' byte autre = 1 - _pid;' ' byte lu;' ' drapeau[_pid] = true;' ' tour = autre;' ' (drapeau[autre] == false || tour == _pid);' ' dedans++;' ' assert(dedans == 1);' ' lu = solde;' ' solde = lu + 1;' ' dedans--;' ' drapeau[_pid] = false;' ' fini++;' '}' 'active proctype controle() {' ' fini == 2;' ' assert(solde == 2);' '}' > essais/peterson.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.
Vérifier le verrou de Peterson
spinrun essais/peterson.pml | grep "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.
Un verrou peut aussi bloquer tout le monde
Retirons le tour. Le client attend seulement que l’autre baisse son drapeau. Si les deux lèvent le leur en même temps, chacun attend l’autre.
C’est un interblocage. SPIN le signale par « invalid end state » : plus aucun processus ne peut avancer, alors que le travail n’est pas fini.
Fabriquer la variante sans tour
sed -e '/tour = autre/d' -e 's/ || tour == _pid//' essais/peterson.pml > essais/sans_tour.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.
La faire vérifier
spinrun essais/sans_tour.pml | head -n 1Affiché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’un verrou est sûr dès qu’il teste une variable avant d’entrer. Tester puis prendre font deux pas, et l’autre processus peut s’intercaler entre les deux. Un verrou est sûr seulement si SPIN ne trouve aucun ordre où deux processus sont dedans.
Pour aller plus loin
Dans peterson.pml, remplacez tour = autre; par tour = _pid; avec sed, dans une copie. Relancez spinrun.
Dites si SPIN trouve encore une erreur, puis expliquez qui reçoit le tour dans la version correcte, et pourquoi cela compte.