La boulangerie : pourquoi la boucle while (choisit[j

L'hypothèse cachée d'abord, car tout en découle : maximum(numero, N) n'est pas une opération. C'est une boucle qui lit les $N$ cases une par une, et un autre fil peut écrire entre deux lectures. La ligne se décompose donc en $N + 1$ opérations : $N$ lectures, puis une écriture.

Le scénario, avec deux fils. Notons $n = (numero [0], numero [1])$ .

pas	qui	fait
$1$	fil $0$	`choisit[0] = true`
$2$	fil $0$	lit $numero [0] = 0$ puis $numero [1] = 0$ : son maximum vaut $0$
$3$	fil $1$	`choisit[1] = true`, lit les deux cases, maximum $0$
$4$	fil $1$	écrit $numero [1] = 1$ , puis `choisit[1] = false`
$5$	fil $1$	examine le fil $0$ : $numero [0] = 0$ , donc pas de ticket : il passe
$6$	fil $0$	écrit $numero [0] = 1$ — le même numéro que le fil $1$
$7$	fil $1$	entre en section critique (il a fini son examen)
$8$	fil $0$	examine : $numero [1] = 1 = numero [0]$ , et $1 < 0$ est faux : il passe
$9$	fil $0$	entre en section critique

Les deux y sont. Le pas $5$ est la faute : le fil $1$ a conclu que le fil $0$ n'avait pas de ticket, alors que le fil $0$ était en train d'en prendre un. Le départage lexicographique par l'indice n'a servi à rien — il n'a été appliqué que d'un côté.

Ce que la boucle while (choisit[j]) ajoute : elle interdit au fil $1$ d'examiner le fil $0$ tant que celui-ci n'a pas fini de choisir. Le pas $5$ deviendrait une attente, et au pas $8$ les deux comparaisons porteraient sur les mêmes valeurs $(1, 1)$ : le fil $0$ , d'indice plus petit, passerait, et le fil $1$ attendrait. Un seul entre.

Vérification exhaustive (problème 22.2), en modélisant la lecture du maximum case par case :

	états atteignables	exclusion mutuelle	contre-exemple
$2$ fils, avec `choisit`	$244$	respectée	—
$2$ fils, sans `choisit`	$301$	violée	$22$ pas
$3$ fils, avec `choisit`	$8804$	respectée	—
$3$ fils, sans `choisit`	$15429$	violée	$28$ pas

ImportantLe grain du modèle est le contrôle

Une première version de cette vérification traitait numero[i] = 1 + maximum(...) comme un pas atomique. Elle rendait « exclusion respectée » dans les quatre cas — c'est-à-dire qu'elle déclarait correct un protocole faux.

Un modèle trop grossier ne trouve pas le défaut : il le supprime. La leçon vaut au-delà de cet exercice : quand on vérifie du code concurrent, la première question n'est pas « le protocole est-il correct ? » mais « qu'ai-je supposé atomique ? ». Ici, la réponse est dans l'énoncé de l'exercice.

Énoncé

Corrigé

Exercices semblables