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.

Rozwiązanie powinno składać się z Na początku raportu należy umieścić sumarycznie, w tabelce, odpowiedzi na wszystkie pytania z punktów 2, 3 i 5. Poza tym w raporcie omawiamy krótko przeprowadzone eksperymenty. Ocena 0-10 punktów, przy czym 0-5 punktów za punkty 1, 2, 3 poniżej oraz 0-5 punktów za punkty 4, 5.

  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:

    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:

  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.


Pytania i odpowiedzi


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