PWiR lab: zadanie 1

Termin przesłania rozwiązania przez moodle: 23.03.2014 23:59. Za każde rozpoczęte 12 godzin opóźnienia odejmujemy jeden punkt.

• dwóch modeli w Promeli, wyspecyfikowanych w punktach 1, 4 poniżej, oraz
• krótkiego raportu (w formacie PDF).

1. Wykonaj w Promeli model następującego protokołu wzajemnego wykluczania (patrz praca [1]), dla N procesów:

       (i = 0 .. N-1) proces P(i) {
           powtarzaj {
               chce[i] = true;
               czekaj, aż dla wszystkich k z [0..N-1] zachodzi !(chce[k] && we[k]);
               we[i] = true;
               jeśli dla pewnego k z [0..N-1] zachodzi chce[k] && !we[k], to wykonaj             (*)
               {    
                   chce[i] = false;
                   czekaj, aż dla pewnego k z [0..N-1] zachodzi wy[k];                          (**)
                   chce[i] = true;
               };
               wy[i] = true;
               czekaj, aż dla wszystkich k z [i+1..N-1] zachodzi !we[k] || wy[k];
               czekaj, aż dla wszystkich k z [0..i-1] zachodzi !we[k];
     
               /* SEKCJA KRYTYCZNA */
   
               wy[i] = false; we[i] = false; chce[i] = false;                                  (***)
           }
       }
   

   Intuicyjne znacznie zmiennych:
   • chce[i]   proces i rozpoczyna protokół wstępny
   • we[i]   proces i jest w poczekalni, z tym że
     • we[i] && chce[i]   proces i jest w poczekalni i chciałby ją opuścić (poczekalnie jako pierwszy opuszcza ostatni proces)
     • we[i] && !chce[i]   proces i jest w poczekalni i czeka, aż któryś inny proces ją najpierw opuści
   • wy[i]   proces i opuścił poczekalnię, i jest gotowy do wejścia (w odpowiedniej kolejności) do sekcji krytycznej, ale najpierw musi poczekać aż inne procesy opuszczą poczekalnię

   Model powinien powstać na bazie pliku prot.pml. Uwaga: nie wolno modyfikować zadnego z wierszy z tego pliku, można tylko dopisać nowy kod do już istniejącego.

2. Dla wartości parametru N >= 4 sprawdź, czy protokól ma następujące własności, używając dowolnych technik dostępnych w Spinie:
   • wzajemne wykluczanie
   • nieunikniona poczekalnia: każde wejście do sekcji krytycznej procesu i poprzedzone jest przez stan o własności we[i] && !chce[i]
   • wyjście z poczekalni: jeśli któryś z procesów i ma własność we[i] && !chce[i], to w końcu któryś z pozostałych procesów j będzie miał własność wy[j]
   • żywotność (brak zagłodzenia), nawet jeśli niektóre procesy utkną na zawsze we własnych sprawach
   • liniowy czas oczekiwania: podczas gdy jakiś proces czeka, żaden inny proces nie może wejść do sekcji krytycznej więcej niż stałą liczbę razy

3. Sprawdź, czy zmiana kolejności zmiennych w (***) wpływa na własności z punktu 2.

4. Zmodyfikuj model tak, by dopuszczał możliwość ,,awarii'' procesów. Awaria polega na ustawieniu wszystkich zmiennych procesu na false i restarcie. Zakładamy, że restartujący proces, zanim przystąpi ponownie do wykonywania protokołu, wykonuje

       czekaj, aż dla wszystkich k z [0..N-1] zachodzi (!we[k] || wy[k]);
   

   Zmodyfikuj protokół następująco (modyfikacja ta opisana jest w pracy [1]):

   Jeśli w punkcie (**) żaden z procesów nie spełnia warunku, a zarazem wszystkie procesy k spełniają warunek !chce[k] || we[k] (intuicyjnie: żaden proces nie czeka już na wejście do poczekalni), to wróć do (*)

5. Sprawdź, czy po modyfikacjach z punktu 4 protokół wciąż spełnia warunki z punktu 2.

[1]   Szymanski, Boleslaw K. A simple solution to Lamport's concurrent programming problem with linear wait. ICS '88: Proceedings of the 2nd international conference on Supercomputing, pp. 621–626, 1988.

• Czy warunki ,,TODO'' należy modelować jako atomowe?   Odp.: Niekoniecznie. To, w jakim stopniu te warunki będą atomowe, pozostawiamy do wyboru studentom.
• Czy rozwiązanie może mieć aktywne oczekiwanie?   Odp.: Tak.
• Czy wolno obkładać istniejące linie instrukcją atomic?   Odp.: Formalnie rzecz biorąc wolno. Pamietajmy jednak, jaki protokół modelujemy...
• Czy można generować model w Promeli automatycznie?   Odp.: Tak, można, chociaż nie polecam takiego rozwiązania. Należy wtedy dostarczyć plik Makefile służący do generowania modelu.
• Czy warunek wzajemnego wykluczania musimy testować pomiędzy dowolnymi dwoma procesami, czy wystarczy jak zweryfikujemy pomiędzy np. 0 a 1? A dla pozostałych własności?   Odp. W przypadku użycia formuł LTL, wystarczy wpisać do modelu formułę dla ustalonych nrów procesów, np. 0 i 1.
• Czy dozwolone jest pisanie formuł LTL ,,na sztywno'' dla N=4?   Odp.: Tak.
• Jak należy interpretować sformułowanie ,,proces czeka'' w warunku liniowego oczekiwania w puncie 2?   Odp.: ,,proces czeka'' = ,,proces rozpoczął protokół''.
• W punkcie 2, przy opisie własności żywotności znajduje się uwaga ,,nawet jeśli niektóre procesy utkną na zawsze we własnych sprawach''. Czy przy weryfikacji innych własności również należy umożliwić procesom ,,utknięcie na zawsze we własnych sprawach''?   Odp.: W przypadku pozostałych własności jest to niekonieczne, ale jak najbardziej dozwolone.
• Czy w ponumerowanych wierszach z pliku prot.pml można dodawać/usuwać białe znaki, np. tabulacje?   Odp.: Tak.

Uwagi i pytania proszę kierować do Sławka Lasoty.     Ostatnia modyfikacja: 20/03/2014