L’exclusion avec jeton circulant

Objectif : étudier en détail le jeton circulant

Inspiration : une solution partielle de l’exclusion mutuelle à base d’un jeton circulant, vu en TD. Il s’agit d’une solution basique qui assure l’exclusion mutuelle mais n’assure ni la vivacité de la circulation du jeton, ni la vivacité d’obtention de l’accès exclusif.

1. Énoncer les propriétés attendues pour le protocole : ExclMutuelle, VivaciteIndividuelle, VivaciteGlobale ; pour le jeton : JetonVaPartout; pour le lien jeton-protocole : Sanity.
2. Avec quelles contraintes d’équité forte est-il possible de vérifier VivaciteIndividuelle ?
3. Donner une solution qui ne nécessite que de l’équité faible.
4. Scinder la variable entière jeton en un tableau de N booléens. Le déplacement du jeton est encore atomique. Énoncer soigneusement les propriétés attendues pour le jeton (par exemple l’unicité).
5. Démontrer que cette version est un raffinage de la version précédente. En particulier, énoncer proprement le mapping entre les variables des deux modules.
6. Rendre non atomique le déplacement du jeton : on introduit un canal de communication entre chaque couple de sites i et i+1. La précédent action de transmission devient deux actions : une action d’envoi du jeton (ajout dans le canal) et une action de réception du jeton (extraction du canal).
   Pour représenter un canal, un modèle simple est la séquence de booléens.
   Bien penser à spécifier les propriétés attendues (par exemple : au plus un canal non vide).
7. Démontrer que cette version est un raffinage de la version précédente. On prendra soin au mapping.