Practicum: Het Kiezen van een Leider in een Ring
Doel
Deze opdracht gaat over de algoritmen voor het kiezen van
een leider in een ring zoals die tijdens de les zijn besproken.
Het doel van de opdracht is om meer inzicht te verkrijgen in
de werking van deze algoritmen, en om te toetsen of je
overweg kunt met Uppaal en aanpassingen kunt maken aan
een model.
Instructie
Het Uppaal model
Open de onderstaande files in Uppaal:
Deze files bevatten een model van Peterson's algoritme voor het
kiezen van een leider in een ring met eenrichtingsverkeer.
Lees de onderstaande toelichting en experimenteer
wat met de simulator voordat je verder gaat met de opdrachten.
Het model bevat n processen ("Nodes") die deel uitmaken van een
ringvormig netwerk. De processen kunnen berichten naar hun directe
opvolger sturen (met de klok mee) via een n-tal kanalen ("Channels").
Hieronder een illustratie voor het geval n=4
De Node automaat
Om te beginnen krijgen iedere node een unieke naam.
Voor de eenvoud gebruiken we in ons model de namen 0, 1,..., n-1.
Er is een speiale automaat Allocate die de namen uitdeelt.
Alle nodes krijgen precies 1 naam, en omdat de volgorde waarin nodes worden
geselecteerd geheel willekeurig is, zijn alle toewijzingen van namen aan nodes mogelijk.
Een node slaat de ontvangen naam op in variabele me.
Vervolgens verstuurd hij deze naam via het uitgaande kanaal.
De node wacht nu (toestand Active2) tot er een bericht binnenkomt.
Dit bericht - de naam van de eerste actieve voorganger -
wordt opgeslagen in variabele left.
Indien left=me dan betekent dit dat de node zelf de enig overgebleven
actieve node is: alle concurrentie is uitgeschakeld en de node wordt de leider.
Indien left en me verschillen wordt de waarde left doorgestuurd.
De node wacht daarna weer tot een bericht wordt
ontvangen - de naam van de tweede actieve voorganger - en slaat het op in variabele left2.
Nu komt de cruciale stap van het Peterson algoritme:
-
indien left groter is dan zowel me als left2 dan blijft de
node actief en kiest left als nieuwe naam;
-
anders wordt de node passief; ontvangen berichten worden doorgestuurd maar de node doet er verder niets mee.
De Channel automaat
De code voor de automaat Channel(i) bespreken we hier niet in detail en die hoef je ook niet te begrijpen.
Het gedrag is uiteindelijk heel eenvoudig: het kanaal ontvangt berichten via poort send[i] en die komen
er uiteindelijk in dezelfde volgorde ("First-In-First-Out") uit via poort receive[(i+1)%n].
Het %-teken staat hier voor de modulo operator:
als i < n-1 dan is (i+1)%n gelijk aan i+1, en als i=n-1 dan is
(i+1)%n gelijk aan 0. Channel(i) kan maximaal m berichten bevatten.
Als het kanaal vol is en er komt toch een bericht binnen dan springt
de automaat naar een "overflow" toestand. Je kunt met behulp van Uppaal laten
zien dat de overflow toestand niet bereikbaar is wanneer m=n-1.
Met behulp van een variabele count houden we bij hoeveel
berichten er worden verstuurd: iedere keer wanneer er een send
actie plaatsvindt wordt de waarde van count opgehoogd.
De queries
In de query file staan een vijftal eigenschappen. Met de Uppaal verifier kun
je vaststellen dat al deze eigenschappen gelden voor het model. De eerste eigenschap zegt
dat in alle bereikbare toestanden hooguit 1 node tot leider is gekozen. Letterlijk staat
er dat er geen bereikbare toestand bestaat waarin twee verschillende nodes i
en j allebei leider zijn:
A[] not exists (i:Nodes) exists (j:Nodes) Node(i).Leader && Node(j).Leader && i != j
De tweede eigenschap zegt dat er in totaal hooguit 100 berichten verstuurd worden.
Letterlijk: in alle bereikbare toestanden is de waarde van teller count kleiner of
gelijk aan 100:
De derde eigenschap stelt dat de capaciteit van alle kanalen (maximaal m=4 berichten) voldoende is en
er nooit een overflow kan optreden:
A[] forall (i:Nodes) not Channel(i).Overflow
Eigenschap vier zegt dat het mogelijk is om met hooguit 50 berichten een leider te kiezen.
Letterlijk: er bestaat een run van het model naar een toestand waarin
Node(0) tot leider is gekozen en count kleiner of gelijk is aan 50.
E<> Node(0).Leader && count <= 50
Wanneer eenmaal een leider is gekozen dan worden er geen berichten meer verstuurd en is het algoritme klaar.
Uppaal noemt een toestand zonder uitgaande transities een "deadlock" maar in dit geval is dat niet ongewenst.
De vijfde eigenschap zegt dat er pas een deadlock op kan treden wanneer er een leider is gekozen.
Letterlijk: in alle bereikbare toestanden geldt dat er ofwel een leider is ofwel dat er geen deadlock is.
A[] (not deadlock) || (exists (i:Nodes) Node(i).Leader)
Vraag 1
Gebruik Uppaal om te bepalen hoeveel berichten minimaal
en maximaal verstuurd moeten worden voordat een leider
gekozen is. Gebruik hiervoor de 2de en 4de eigenschap
in de verifier. Door de getallen te veranderen kun je
er achterkomen wanneer de eigenschappen wel en niet gelden.
Geef voorbeelden van hoe namen toegekend worden aan nodes
in een kortste en in een langste executie. Hiervoor kun je
gebruik maken van de mogelijkheid van Uppaal om
tegenvoorbeelden te genereren.
Vraag 2
Herhaal vraag 1 voor de gevallen waarbij n=4 en n=3.
Vraag 3
Maak, uitgaande van het model van het Peterson algoritme,
een model van het Chang-Roberts algoritme, en check of alle
geformuleerde correctheidseigenschappen nog steeds gelden.
Ter opfrissing: dit algoritme werkt als volgt.
-
Elk proces stuurt een bericht rond met z'n naam.
-
Berichten met grotere namen stuur je door (en je wordt non-leader), met kleinere namen gooi je weg.
-
Als je eigen bericht weer terugkomt, win je.
Tip: Je hoeft alleen de automaat Node(i) aan te passen (en die wordt een stuk simpeler).
Om overflow te voorkomen moet je de capaciteit van de kanalen iets groter maken.
Vraag 4
Bepaal het minimale en maximale aantal berichten dat verstuurd
wordt in het Chang-Roberts algoritme voor n=3, 4, 5.
Bonusvraag
Vanaf welke waarde van n is Peterson's algoritme efficienter
(in termen van maximaal aantal benodigde berichten) dan Chang-Roberts?
Geef een zo goed mogelijke schatting.
(NB Voor het beantwoorden van deze vraag heb je niet meer zoveel
aan Uppaal. Vanaf n=6 wordt het aantal toestanden te groot om
snel met Uppaal door te rekenen.)