Teoria współbieżności

Informatyka

Symulator Pipe2.
Jest napisany w Javie i jego uruchomienie nie wymaga uprawnień administratora (jest dostępny pod Windows i Linux).

Maszyna stanów. Prosty model maszyny stanów swiateł ulicznych przedstawia sieć na rysunku poniżej:

Stanami są miejsca sieci, zaś znacznik pokazuje w jakim stanie aktualnie się znajdujemy.

Narysować przykład w symulatorze.
Sprawdzić własciwości sieci (ograniczoność, bezpieczeństwo i możliwy deadlock) w symulatorze Pipe w menu "State Space Analysis".
Wygenerować graf osiągalności "Reachability/Coverability Graph". Zaobserwować:
- Jakie znakowania są osiągalne?
- Ile wynosi maksymalna liczba znaczników w każdym ze znakowań ? Jakie mozemy wyciągnac z tego wnioski n.t. ograniczoności i bezpieczenstwa?
- Czy kazde przejście jest przedstawione jako krawędz w grafie? Jaki z tego wniosek n.t. żywotnosci przejść?
- Czy wychodząc od dowolnego węzła grafu (znakowania) można wykonać dowolne przejście ? Jaki z tego wniosek n.t. żywotności sieci? Czy są możliwe zakleszczenia ?
Wykonać analizę niezmienników (wybrać w menu "Invariant Analysis").
- wynik analizy niezmienników przejść (T-invariants) pokazuje nam, ile razy trzeba odpalić dane przejście (T), aby przekształcić znakowanie początkoweg z powrotem do niego samego (wynik nie mowi nic o kolejności odpaleń). Z wyniku możemy m.in. wnioskować o odwracalności sieci.
- wynik analizy niezmienników miejsc (P-invariants) pokazuje nam zbiory miejsc, w których łączna suma znaczników się nie zmienia. Pozwala to wnioskować n.t. zachowawczości sieci (czyli własności, gdzie suma znaczników pozostaje stała) oraz o ograniczoności miejsc.

Rozwiązania do zadań wraz z dyskusją należy zawrzeć w sprawozdaniu !

Zadanie 1 - wymyślić własną maszynę stanów, zasymulować przykład i dokonać analizy grafu osiągalności oraz niezmienników j.w.
Zadanie 2 - zasymulować sieć jak poniżej.

Dokonać analizy niezmienników przejść. Jaki wniosek można wyciągnać o odwracalności sieci? Wygenerować graf osiągalności. Proszę wywnioskować z grafu, czy sieć jest żywa. Proszę wywnioskować czy jest ograniczona. Objasnić wniosek.
Zadanie 3 - zasymulować wzajemne wykluczanie dwóch procesów na wspólnym zasobie. Dokonać analizy niezmienników. Wyjasnić znaczenie równań (P-invariant equations). Które równanie pokazuje działanie ochrony sekcji krytycznej ?
Zadanie 4 - uruchomić problem producenta i konsumenta z ograniczonem buforem (można posłuzyć się przykładem, menu:file, examples). Dokonać analizy niezmienników. Czy sieć jest zachowawcza ? Które równanie mówi nam o rozmiarze bufora ?
Zadanie 5 - stworzyć symulację problemu producenta i konsumenta z nieograniczonym buforem. Dokonać analizy niezmienników. Zaobserwować brak pełnego pokrycia miejsc.
Zadanie 6 - zasymulować prosty przykład ilustrujący zakleszczenie. Wygenerować graf osiągalności i zaobserwować znakowania, z których nie można wykonać przejsć. Zaobserwować własciwosci sieci w "State Space Analysis". Poniżej przykład sieci z możliwoscią zakleszczenia (można wymyślić inny):

Marcin Szpyrka, Sieci Petriego w modelowaniu i analizie systemów współbieznych, WNT Warszawa 2008

Maciej Malawski, malawski at agh.edu.pl
Katarzyna Rycerz, kzajac at agh.edu.pl