Probleme – Vérifier un protocole en explorant tous les entrelacements

1. Le modèle. Un état est la donnée de :

• le compteur ordinal de chaque fil — à quelle ligne il en est ;
• la valeur de chaque variable partagée ;
• la valeur de chaque variable locale d'un fil, lorsqu'elle survit d'une ligne à la suivante (l'indice de boucle, le maximum en cours de calcul).

Une transition fait avancer un fil d'une ligne. Le graphe de tous les états atteignables depuis l'état initial contient, par construction, tous les entrelacements possibles — et rien d'autre.

C'est le graphe du chapitre chap:graphes, et l'exploration est celle du chapitre chap:parcours : un parcours en largeur avec un ensemble d'états visités.

2. L'exploration.

Entrée  : etat_initial, une fonction successeurs, un predicat en_section
Sortie  : le nombre d'etats atteignables, un contre-exemple s'il en existe

vus  <-- {etat_initial}
file <-- [etat_initial]
pere[etat_initial] <-- aucun
tant que la file n'est pas vide :
    e <-- defiler
    si  en_section(e) >= 2  :  contre-exemple trouve, remonter par pere
    succ <-- successeurs(e)
    si aucun element de succ ne differe de e, et qu'un fil est engage :
        etat d'INTERBLOCAGE
    pour chaque s de succ non deja vu :
        vus <-- vus + {s} ; pere[s] <-- e ; enfiler s

Elle cherche deux choses, et il faut les distinguer.

Les deux premières sont des propriétés d'états : on les teste en visitant. La troisième est une propriété de chemins infinis, et demande une analyse des cycles du graphe — on ne la traite pas ici. Le tableau du dictionnaire pere sert à reconstituer la trace : un contre-exemple sans sa trace n'apprend rien.

3. Les résultats, tous mesurés.

Deux lectures de ce tableau valent d'être relevées.

D'abord, les deux dernières lignes ont le même nombre d'états. Ce n'est pas un hasard : avec cinq philosophes, « prendre la fourchette de plus petit numéro » revient à ce que les philosophes $0$ à $3$ prennent leur gauche et que le philosophe $4$ prenne sa droite — c'est-à-dire exactement la parade 1, appliquée à un autre convive. La mesure confirme ce que le cours annonce : « la parade 2 est la généralisation de la parade 1 ».

Ensuite, les états ne se comptent pas en millions. Deux fils, deux variables : $42$ états. C'est infime, et pourtant aucun être humain ne parcourt $42$ entrelacements sans en oublier.

Le piège de la modélisation, et il est central : qu'a-t-on supposé atomique ? Une première version de ce programme traitait numero[i] = 1 + maximum(numero, N) comme une transition unique. Elle rendait alors « boulangerie sans choisit : exclusion respectée » — déclarant correct un protocole faux. Il a fallu décomposer la lecture du maximum en $N$ transitions, une par case, pour que le défaut réapparaisse.

4. Ce que l'exploration ne prouve pas.

• Elle ne prouve rien pour $n$ quelconque. On a vérifié la boulangerie pour $2$ et $3$ fils ; $10$ fils demanderaient un graphe hors de portée, et $n$ fils une preuve, pas un calcul. La vérification confirme, elle ne généralise pas.
• Elle ne dit rien de l'équité. Aucun interblocage n'est signalé pour les philosophes avec la parade 2, et pourtant la mesure du problème 22.4 montrera une famine sévère.
• Elle suppose la mémoire séquentiellement cohérente : que toute écriture soit vue immédiatement par tous, dans l'ordre du programme. Aucun processeur moderne ne le garantit — c'est la mise en garde du cours sur les barrières mémoire. Peterson est correct dans ce modèle, et faux sur une machine réelle sans barrières.

La conclusion est celle du chapitre chap:discipline, transposée : un contrôle exhaustif sur un modèle est infiniment supérieur à des tests aléatoires sur le vrai programme, et il ne remplace pas la compréhension de ce qu'on a modélisé.