Le problème du consensus se traduit formellement de la façon suivante:
{(x0,x0,...,x0), |
(x1,x1,...,x1), |
..., |
(xn-1,xn-1,...,xn-1)} |
La généralisation de cette représentation des états des processeurs, sous forme de graphe, est très simple. L'état global de trois processus sera représenté par l'enveloppe convexe des trois points qui sont les états locaux de chacun des trois processus, comme à la figure 11.8. Pour n processus en général, l'état global sera représenté par l'enveloppe convexe de n points distincts, ce que l'on appelle un n-simplexe: pour n=3 c'est un triangle, pour n=4 c'est un tétraèdre etc.
De même que dans le cas n=2, certaines faces d'un n-simplexe, qui sont des m-simplexes, c'est-à-dire qui représentent les états locaux d'un sous-groupe de m processeurs, peuvent être communes à plusieurs n-simplexes, voir par exemple l'ensemble d'états représenté géométriquement à la figure 11.9. Ces collages de n-simplexes le long de leurs faces sont ce que l'on appelle en général un ensemble simplicial. Il y a une très riche théorie des ensembles simpliciaux, aussi bien combinatoire que topologique. En effet, on peut toujours associer un ensemble simplicial à tout espace topologique, et à ``déformation'' près (homotopie), la théorie des ensembles simpliciaux est équivalente à celle des espaces topologiques. On utilisera plus loin des intuitions topologiques quand on aura à décrire certains ensembles simpliciaux.
Avec cette représentation des états, la spécification d'une tâche de décision devient une relation ``graphique'' comme à la figure 11.10, dans le cas du consensus binaire. Les états globaux en relations sont indiqués par les flèches en pointillé. Ainsi, le ``segment'' ((P,0),(Q,1)) peut être mis en relation par d avec ((P,0),(Q,0)) où ((P,1),(Q,1)).
s = empty; for (i=0; i<r; i++) { broadcast messages; s = s + messages received; } return delta(s);A chaque tour de boucle correspond un ensemble d'états accessibles, représentés géométriquement, comme aux figures 11.12, 11.13, 11.14. Ceci dépend essentiellement du modèle de communication que l'on a, et sera développé dans deux cas aux sections 11.3 et 11.4.
Sans vouloir définir de façon générale ce que l'on entend par obstruction topologique, il nous faut quand même expliciter les cas d'intérêt pour la suite de la formalisation. Quand on dit ici obstruction topologique, cela veut dire obstruction à l'existence d'une fonction continue f d'un espace topologique (typiquement ici ce sera la réalisation géométrique d'un espace simplicial d'états) X vers un espace topologique Y vérifiant certaines conditions. Par exemple, si on impose f(x0)=y0 et f(x1)=y1 avec x0 et x1 dans la même composante connexe et y0 et y1 qui ne sont pas dans la même composante connexe, alors un tel f continu ne peut pas exister (car l'image d'une composante connexe par une fonction continue est une composante connexe). De même, si f va de la n-sphère pleine (le n-disque) vers la n-sphère vide, de telle façon que f est l'identité sur la n-sphère vide, alors f ne peut pas être continue. Cela est lié à la notion de n-connexité, qui est une généralisation de la connexité. Déjà, la 1-connexité (ou simple connexité) est un invariant plus subtil que la connexité (ou 0-connexité), par exemple le cercle est connexe mais pas 1-connexe. Dit de façon brève, la n-sphère vide est (n-1)-connexe (la 0-connexité correspond à la connexité habituelle) et pas n-connexe, alors que la n-sphère pleine est n-connexe.
Dans le modèle synchrone, à l'étape 1 (voir la figure 11.12), soit aucun processus n'est mort, donc tout le monde a reçu le message des autres (d'où le segment central), soit un processus est mort, d'où les deux points comme états possibles.
On va faire ici une application simple de cette stratégie de preuve. On considère le problème du consensus binaire entre trois processus, dans le modèle synchrone (et passage de messages) Le complexe d'entrée est composé de 8 triangles: (0,0,0), (0,0,1), (0,1,0), (0,1,1), (1,0,0), (1,0,1), (1,1,0) et (1,1,1). Il est en fait homéomorphe à une sphère (une seule composante connexe): les quatre premiers triangles déterminent l'hémisphère ``nord'' alors que les quatre derniers déterminent l'hémisphère ``sud''. Le complexe de sortie est composé de deux triangles: (0,0,0) et (1,1,1) (donc, deux composantes connexes).
On considère au plus n-2 plantages, comme à la figure 11.19.
On peut prouver de façon plus générale que, dans tout complexe de protocole à jusqu'à l'étape n-2, le sous-complexe où les processus ont tous 0 comme valeur locale, et le sous-complexe où les processus ont tous 1 comme valeur locale, sont connexes. Par le même raisonnement, il s'en suit aisément qu'on ne peut pas résoudre le problème du consensus en moins de n-2 étapes.
On suppose que l'on dispose d'une machine comme à la figure 11.20, dans laquelle n processus partagent une mémoire de taille infinie, partitionnée de la manière suivante. Chaque processus peut écrire de façon atomique sur sa partie (update) et lire de façon atomique toute la mémoire partagée dans sa propre mémoire locale. C'est un modèle équivalent, en ce qui nous concerne, au modèle plus classique de lecture/écriture atomique en mémoire partagée (sans partitionnement). On cherche maintenant des protocoles sans attente, c'est-à-dire robustes jusqu'à n-1 pannes.
On a le théorème suivant, que l'on ne prouvera pas, et qui est du à Maurice Herlihy et Sergio Rajsbaum (voir par exemple [HR00]):
Le complexe de sortie, illustré à la figure 11.23 est composé de 3 sphères collées ensemble, moins le simplexe formé des 3 valeurs distinctes. Il n'est pas simplement connexe.
Alors, comme illustré à la figure 11.25, il y a au moins un simplexe qui possède toutes les couleurs (lemme de Sperner).
De façon générale, comme le complexe de protocole est simplement connexe, on peut ``remplir'' l'intérieur des chemins combinatoires. Les coins du complexe de protocole sont coloriés avec la valeur initiale sur ces processeurs (voir remarque en dimension 1). Il nous reste seulement à appliquer le lemme de Sperner. On en déduit qu'il existe un simplexe qui a toutes les 3 couleurs. Ce simplexe correspondrait à une exécution du protocole dans laquelle les trois processeurs décideraient trois valeurs différentes, ce qui contredit l'hypothèse du 2-consensus!
P | = | update; | P' | = | update; |
scan; | scan; | ||||
case (u,v) of | case (u,v) of | ||||
(x,y'): u=x';update;[] | (x,y'): v=y;update;[] | ||||
default: update | default: update |
Cela est facile à voir, en utilisant la sémantique des opérations de lecture/écriture atomiques. En fait, on n'a que trois traces intéressantes possibles, correspondant aux trois segments:
Dans le cas de test&set par exemple, les complexes de protocoles sont tous (n-3)-connexes. On en déduit bien évidemment que le consensus entre deux processus est implémentable, et donc que c'est une primitive ``plus puissante'' que la lecture/écriture atomique. Mais on en déduit aussi assez facilement que le consensus entre trois processus n'est pas implémentable.