Peterson : ce que l'ordre des deux premières lignes garantit

Exercice · niveau 2 · informatique (MP2I/MPI), chapitre 22 — Concurrence et synchronisation

É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 $v = (veut [0], veut [1])$ .

pas	qui	fait	$v$	`tour`
		état initial	$(F, F)$	$0$
$1$	fil $0$	`tour = 1`	$(F, F)$	$1$
$2$	fil $1$	`tour = 0`	$(F, F)$	$0$
$3$	fil $1$	`veut[1] = true`	$(F, V)$	$0$
$4$	fil $1$	teste : $veut [0]$ est faux	$(F, V)$	$0$
$5$	fil $1$	entre en section critique	$(F, V)$	$0$
$6$	fil $0$	`veut[0] = true`	$(V, V)$	$0$
$7$	fil $0$	teste : $tour = 0 \neq = 1$	$(V, V)$	$0$
$8$	fil $0$	entre en section critique	$(V, V)$	$0$

Les deux y sont. Cet entrelacement a été trouvé par exploration exhaustive (problème 22.2) : la version inversée atteint $72$ états, et l'exclusion mutuelle y est violée ; la version du cours en atteint $42$ , et elle ne l'est jamais.

Où exactement l'ordre du cours interdit-il ce scénario ? Au pas $4$ . Le fil $1$ y lit $veut [0] = F$ et en conclut que le fil $0$ ne demande rien — alors que le fil $0$ a déjà commencé son protocole, puisqu'il a écrit tour au pas $1$ . Le fil $0$ 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é $veut [i] = true$ avant d'attendre », ce qui n'est vrai que dans cet ordre-là.

ImportantUne preuve dépend de l'ordre des instructions, et cela ne se voit pas

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 $72$ é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.

Les autres exercices de ce chapitre Le cours du chapitre

Un blocage sur cet exercice ? Le tuteur d'Adloun guide par questions, sans donner la réponse.