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:

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: 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: 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. 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.

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. 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.)