informatique (MP2I/MPI) · Chapitre 22 · Exercice de TD
Peterson : ce que l'ordre des deux premières lignes garantit
Concurrence et synchronisation · niveau 2
Énoncé
On échange les deux premières lignes de entrer :
void entrer(int i) {
int j = 1 - i;
tour = j; /* 1'. je cède le tour -- ÉCHANGÉES */
veut[i] = true; /* 2'. j'annonce mon intention */
while (veut[j] && tour == j) { }
}Exhiber un entrelacement qui met les deux fils en section critique.
Corrigé
L'entrelacement, en huit pas. On note .
| pas | qui | fait | tour | |
|---|---|---|---|---|
| état initial | ||||
| fil | tour = 1 | |||
| fil | tour = 0 | |||
| fil | veut[1] = true | |||
| fil | teste : est faux | |||
| fil | entre en section critique | |||
| fil | veut[0] = true | |||
| fil | teste : | |||
| fil | entre en section critique |
Les deux y sont. Cet entrelacement a été trouvé par exploration exhaustive (problème 22.2) : la version inversée atteint états, et l'exclusion mutuelle y est violée ; la version du cours en atteint , et elle ne l'est jamais.
Où exactement l'ordre du cours interdit-il ce scénario ? Au pas . Le fil y lit et en conclut que le fil ne demande rien — alors que le fil a déjà commencé son protocole, puisqu'il a écrit tour au pas . Le fil est engagé sans l'avoir annoncé. C'est là toute la faute : la version inversée laisse une fenêtre où un fil a déjà agi sur la variable commune sans avoir levé son drapeau.
Dans l'ordre du cours, poser veut[i] = true d'abord rend l'engagement visible avant toute autre action. On peut le formuler comme un invariant : dès qu'un fil a touché tour, son drapeau est levé. La preuve du cours l'utilise sans le dire — elle affirme que « les deux ont posé avant d'attendre », ce qui n'est vrai que dans cet ordre-là.
Le programme inversé se lit exactement comme l'autre. Il a les mêmes variables, la même boucle, le même nombre de lignes. Aucun compilateur, aucun test unitaire, aucune relecture rapide ne les distingue.
C'est la raison d'être des méthodes formelles pour ce type de code : sur états, l'exploration exhaustive du problème 22.2 trouve le contre-exemple en une fraction de seconde. Un être humain peut y passer une heure.