Practicum: Hyman's Algoritme

Achtergrond

Deze opgave gaat over wat op het eerste gezicht een goede oplossing lijkt te zijn voor het mutual exclusion probleem, maar waar bij nader inzien helemaal niets van blijkt te deugen.

Deze "oplossing" is bedacht, ter publicatie opgestuurd naar een vooraanstaand tijdschrift, gecheckt door de redacteur en een of meer reviewers, en geen van deze personen realiseerde zich dat de voorgestelde oplossing fout was. Het algoritme is gepubliceerd in het tijdschrift en de publicatie moest later teruggetrokken worden nadat de fout ontdekt was!

(Harris Hyman, Comments on a problem in concurrent programming control, Communications of the ACM, v.9 n.1, p.45, Jan. 1966)

initially turn=0, blocked[0]=blocked[1]=false ;
        
Elk van de twee processen, P0 en P1, voert de onderstaande code uit, P0
voert Protocol(0) uit, en P1 voert Protocol(1) uit.

void Protocol (int id)
     while (true)
      {
1.        blocked[id] = true ;
2.        while (turn != id)
            {
3.             while (blocked[1-id])
                 {
4.               /* do nothing */
                 };
5.             turn = id;
            };
6.        CriticalSection ;
7.        blocked[id] = false ;
      }

Opgave 1

Maak een Uppaal model van Hyman's algoritme en gebruik Uppaal om aan te tonen dat het algoritme niet voldoet aan mutual exclusion. Leg uit wat er fout gaat. Hint: ga uit van een van de modellen die tijdens het college is gepresenteerd, bijvoorbeeld het model van Peterson's oplossing. Lever behalve de toelichting ook je Uppaal model in.

Opgave 2

Er is nog een ander probleem met Hyman's oplossing. We zeggen dat een mutual exclusion algorime geen processen kan "uitsluiten" indien voldaan is aan de volgende voorwaarde:

Indien processen altijd de kritieke sectie na eindige tijd verlaten, dan zal ieder proces dat bij regel 2 van de code arriveert uiteindelijk in de kritieke sectie komen. Informeel komt dit er op neer dat ieder proces dat de kritieke sectie in wil er uiteindelijk ook in komt. Toon aan dat Hyman's algoritme niet aan deze voorwaarde voldoet. Uppaal is niet echt geschikt om dit soort eigenschappen aan te tonen dus je zult voor de verandering zelf moeten nadenken :-)