3.2.6.1 La K-exclusion mutuelle
Pour prouver que cet algorithme assure la K-exclusion
mutuelle, on doit assurer que K sites au plus exécutent la SC
simultanément : dans les algorithmes utilisant les jetons, seule la
possession d'un jeton permet à un site l'exécution de la SC,
puisqu'on a K jetons dans l'algorithme, alors au plus K sites peuvent entrer en
SC. la K-exclusion mutuelle est donc assurée.
3.2.6.2 Absence d'interblocage
Nous allons montrer l'absence d'interblocage par
l'absurde, on suppose que le système est en interblocage, il existe donc
un cycle des sites x1, x2, ..., xn, tel
que x1 attend un jeton de x2, x2 attend un jeton de
x3, ..., et xn attend un jeton de x1
[Lai02].
Dans l'algorithme, seules les racines peuvent demander
des jetons via l'anneau, un site racine ne demande un jeton que s'il ne peut
pas satisfaire ses requêtes locales, avant de satisfaire ses
requêtes, cette racine n'a pas le droit de stocker de nouvelles
requêtes, si ce site reçoit une requête, il va la propager
vers un voisin, le cycle donné ci-dessus ne peut jamais apparaître
dans notre algorithme. Cet algorithme est donc exempt de
l'interblocage.
3.2.6.3 Absence de la famine
Un site demandeur i sera ajouté
à la file d'attente, toutes les requêtes qui arrivent après
cette requête seront ajoutées à la fin de la file
d'attente. La famine aura lieu si ces requêtes obtiennent un jeton avant
le site i, c'est à dire, une décision injuste est faite
au niveau du site racine. Dans notre algorithme, le site racine ajoute les
requêtes dans la file d'attente selon leur ordre d'arrivée, la
tête de la file est toujours la requête la plus ancienne. Si un
jeton libre est disponible, le site racine va l'envoyer vers la tête de
la file, les autres requêtes doivent attendre la libération de ce
jeton ou la disponibilité d'un autre. Notre algorithme n'a pas de
problèmes de famine.
| 
