PWiR lab: zadanie 1

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

W Promeli nie ma konstrukcji do modelowania upływu czasu - spróbujmy obejść to ogranicznenie. Założmy, że czas jest dyskretny, tzn. że jego upływ mierzymy liczbą tiknięć jakiegoś abstrakcyjnego globalnego zegara. Dodatkowo załóżmy, że szybkość wykonywania instrukcji Promeli jest dowolna, tzn. tiknięcia zegara nie wpływają na ich wykonanalność.

1. Zdefiniuj w Promeli makra do modelowania:
   • uśpienia procesu sleep(T) na podaną liczbę jednostek czasu T -- proces jest wstrzymywany aż do upłynięcia wymaganego czasu
   • czynności pilnych, tzn. takich, które muszą się zakończyć przed upływem podanej liczby jednostek czasu T
   Można założyć, że jedynymi procesami, które wywołują powyższe makra, są procesy active [N] proctype P() { ... }, o identyfikatorach 1 .. N. Być może warto użyć dyrektyw preprocesora #define i/lub inlinowania inline x(a,b,c) { ... }.

2. Użyj makr z poprzedniego punktu do opisania w Promeli następującego protokołu wzajemnego wykluczania, opartego na zależnościach czasowych:

   kto : {0 ... N} = 0;
   
   (i = 1 .. N) proces P(i) {
                    powtarzaj 
                    {
                        jeśli (kto == 0) 
                        {
                            kto = i;   /* zakładamy, że przypisanie zakończy się najpoźniej po T1 jednostkach czasu od wykonania testu ,,kto == 0'' */
                            sleep(T2);
                            jeśli (kto == i) {
                                critical_section
                                kto = 0;
                            }
                        }
                    }
   }
   

3. Jaki warunek ograniczający T1 i T2 gwarantuje wzajemne wykluczanie?

4. Dla wybranych poprawnych wartości T1 i T2 niemniejszych niż 2, i dla N niemniejszego niż 4 sprawdź, czy protokól ma następujące własności, używając dowolnych technik dostępnych w spinie:
   • wzajemne wykluczanie
   • żywotność
   • jeśli któryś proces rozpocznie protokół wstępny, to po upływie nie więcej niż T1 + T2 jednostek czasu króryś proces znajdzie się w sekcji krytycznej
   • ten proces, który jako pierwszy ustawi zmienną kto, wejdzie jako pierwszy do sekcji krytycznej

Ostatnia modyfikacja: 05/03/2013