Het is de bedoeling dat je 1 week met
deze opdracht bezig bent, 2 uur op het practicum en 2 uur daarbuiten. © Harry Broeders.
Deze pagina is bestemd voor studenten van de Haagse Hogeschool - Faculteit Technologie, Innovatie & Samenleving groep MNES = minor Embedded Systems.
Het is de bedoeling dat je 1 week met
deze opdracht bezig bent, 2 uur op het practicum en 2 uur daarbuiten.
Bij deze opdracht maken we gebruik van JSpin. Op de academie TISD van de HHS is JSpin geïnstalleerd in Q:\Grp_Elektrotechniek\Embedded_systems\jspin. Je kunt het programma starten door dubbel te klikken op jspin.jar.
Het probleem van de dinerende filosofen wordt vaak gebruikt om de problemen
die kunnen ontstaan bij concurrent programmeren te illustreren. Dit beroemde
probleem wordt beschreven in bijna elk boek over operating systems en ook op Wikipedia 
. Lees dat nu even door!
Het hier gegeven Promela programma modelleert het probleem. Een filosoof wordt gemodelleerd met een proces en een vork wordt gemodelleerd met een message queue (waar 1 vork in past). Bij het starten van het programma wordt elke message queue gevuld met één vork. Een filosoof kan als hij wil gaan eten twee vorken pakken door een receive op zijn linker en rechter message queue uit te voeren. Als de filosoof klaar is met eten legt hij de vorken weer op de tafel. Dit wordt gemodelleerd door de vork naar de bijbehorende message queue te verzenden.
Bestudeer en simuleer het programma dat hierboven gegeven is, met behulp van SPIN, zodat je begrijpt hoe het werkt. Standaard simuleert SPIN in random mode maar 250 stappen. Hoe kun je dit aantal stappen vergroten? Bedenk eerst zelf of dit model een dead-lock op kan leveren. Verifeer dit met behulp van SPIN. Met guided simulation kun je achterhalen hoe deze deadlock ontstaat. Laat m.b.v een interactieve simulatie zien wat het probleem is. Tip: Je kunt in de output bepaalde dingen uitzetten via het menu Options, Common en variabelen filteren via het menu Output.
In het boek "Operating Systems" van Silberschatz and Galvin worden 3
oplossingen van dit probleem gepresenteerd. De eerste oplossing waarmee
deadlock voorkomen kan worden is er voor te zorgen dat het oppakken van de
linker en rechtervork een ondeelbare handeling wordt. Implementeer deze
oplossing in het PROMELA model en verifeer deze oplossing met SPIN. Een
simpel atomic statement rond de twee sends werkt niet goed omdat
de tweede send kan blokken.
Een alternatieve oplossing om te deadlock te voorkomen is om maximaal 4 (van de 5) filosofen aan de tafel te laten plaatsnemen. Om te kunnen denken hoeft een filosoof namelijk niet aan tafel te zitten (om te eten natuurlijk wel). Implementeer deze oplossing in het PROMELA model en verifeer deze oplossing met SPIN.
Nog een alternatieve oplossing om te deadlock te voorkomen is om de filosofen niet allemaal in dezelfde volgorde (eerst links dan rechts) hun vorken op te laten pakken. Laat de filosofen met een even nummer de vorken in de omgekeerde volgorde oppakken. Implementeer deze oplossing in het PROMELA model en verifeer deze oplossing met SPIN.
Het is dus op diverse manieren mogelijk om deadlock te voorkomen. We willen
daarnaast natuurlijk ook vookomen dat één (of meer) van de filosofen omkomt
van de honger. Dit kunnen we in SPIN controlleren met behulp van
progress labels (zie SPIN documentatie).
Controleer met behulp van een progress label dat de init
functie niet continue wordt gestart. Natuurlijk wordt de init functie niet
continue gestart, we testen dit alleen maar zodat we zien wat er gebeurd als
een executiepad bestaat waarbij je nooit meer langs een progress label komt.
Als je een model op "progress" wilt onderzoeken moet je in de dropdownbox
waarin standaard "Safety" geselecteerd staat "Non-progress" selecteren en
daarna op "Verify" drukken. Als er een executiepad bestaat waarbij je nooit
meer langs een progress label komt rapporteerd Spin een non-progress cycle. Als
je geen progress label in je code hebt gezet dan rapporteerd Spin dus altijd
een non-progress cycle.
Controlleer met behulp van een progress label dat er minstens
één filosoof is die niet verhongerd.
Het is wel mogelijk dat één bepaalde filosoof verhongerd. Toon aan dat
één bepaalde filosoof (bijvoorbeeld filosoof nummer 0) wel kan verhongeren.
Om dit te kunnen doen moet je een aparte state Eat0 toevoegen waar
alleen filosoof nummer 0 in kan komen en vervolgens op de juiste plaats een
progress label plaatsen.