Peterson's Algoritme voor Mutual Exclusion

Achtergrond

Deze opdracht gaat over Peterson's algoritme voor mutual exclusion, dat eerder al aan bod is gekomen tijdens de les. Open het Uppaal model voor Peterson's algoritme in Uppaal:

Experimenteer wat met de simulator voordat je verder gaat met de opdrachten.

Vraag 1

Wikipedia heeft een speciale pagina gewijd aan Peterson's algoritme. Op deze pagina wordt letterlijk geclaimd dat Toon aan dat dit niet klopt door een executie te geven die eindigt in een toestand waarin bovenstaande eigenschap niet geldt. Formuleer de eigenschap in Uppaal en gebruik Uppaal om een tegenvoorbeeld te genereren. Hint: De logische "of" schrijf je in Uppaal als || en de logische "implicatie" als imply. Gebruik haakjes om de structuur van je formule aan te geven. Raadpleeg indien nodig het Uppaal help menu en kijk bij "Language Reference -> Requirement Specification" en "Language Reference -> Expressions" voor voorbeelden van correctheidseigenschappen.

Vraag 2

In het model gaan we er van uit dat in locatie try2 eerst de conditie flag[1-pid] wordt geëvalueerd en pas daarna (indien nodig) conditie turn == 1-pid. Beschrijf een aanpassing van het model waarbij deze volgorde is omgekeerd en eerst turn == 1-pid wordt geëvalueerd en pas daarna flag[1-pid]. Maakt dit wat uit voor de correctheid van het algoritme? Beschrijf ook een aanpassing waarbij evaluatie van de conditie steeds zowel in de ene als in de andere volgorde kan plaatsvinden. Maakt dit uit?

Vraag 3

Een belangrijke eigenschap van Peterson's algoritme is dat een proces hooguit 1 keer het andere proces voor hoeft te laten gaan. We kunnen dit aantonen door een aanpassing te maken van het model waarbij timing informatie wordt toegevoegd. We nemen aan dat het uitvoeren van een toekenning of test maximaal l tijdseenheden kost, en dat een proces maximaal c tijdseenheden in de kritieke sectie mag verblijven. Het aangepaste model vind je hier:

In het model hebben we bij de algemene declaraties twee constanten l en c ingevoerd en waarden 4 respectievelijk 100 gegeven; deze waarden kun je zelf makkelijk aanpassen. Het idee is dat ieder proces een locale klok x heeft, die op 0 wordt gezet steeds wanneer het proces naar een nieuwe toestand springt. De invariant x<=1 bij locatie try0 zorgt ervoor dat het proces hooguit l tijdseenheden mag doorbrengen in deze locatie. Op deze manier modelleren we dat het uitvoeren van de instructie flag[pid]=true hooguit l tijdseenheden kost. Op vergelijkbare wijze is de rest van de automaat aangepast. Om te bepalen hoeveel tijd er maximaal kan verstrijken tussen het moment waarop een proces te kennen geeft dat het in de kritieke sectie wil (door naar try0 te springen) en het moment dat het proces de kritieke sectie in gaat, voeren we voor ieder proces een hulpklok y in, die op 0 wordt gezet wanneer het proces naar try0 springt. We kunnen Uppaal nu vragen of de volgende eigenschap geldt: 


 A[] (P(0).try0 || P(0).try1 || P(0).try2 || P(0).try3) imply P(0).y <= 1000
Met andere woorden: zolang proces P(0) in een van de toestanden try0-try3 kan klok y nooit een waarde aannemen groter dan 1000. Dit betekent dat proces P(0) altijd hooguit 1000 tijdseenheden hoeft te wachten voordat het de kritieke sectie in mag. Immers, de enige manier waarop het proces de verzameling toestanden try0-try3 kan verlaten is door naar de kritieke sectie te gaan!

Bepaal de maximale wachttijd m, dat wil zeggen de maximale tijd die kan verstrijken tussen het moment waarop een en proces te kennen geeft dat het in de kritieke sectie wil en het moment dat het proces de kritieke in gaat. Je kunt dit doen door te spelen met de bovengrens 1000 in bovenstaande formule. Herhaal dit voor alle mogelijke combinaties waarbij l = 1, 2, 4 en c = 50, 100. Kun je een formule geven voor m in termen van l en c? Beschrijf in woorden een run van het protocol waarbij het maximaal lang duurt voordat proces P(0) de kritieke sectie in komt.