ALR - ćw - temat E, weryfikacja, "model checking"

czyli automatyczne dowodzenie poprawności algorytmów asynch,
zarówno message passing, jak i shared memory;
chodzi nie tylko o algorytmy ale także: urządzenia, systemy, ...
/// slajdy z wykładu ///

jest to jedynie krótkie wprowadzenie do tej tematyki, która jest b. szeroka ...

Spin/Promela

system modelujemy pisząc kod w j. Promela...
weryfikację programu w Promeli przeprowadza się programem spin...

http://spinroot.com/, Language Reference, Basic Spin Manual, Spin Online Reference
SpinIntro.pdf: slajdy opisujące zasadę działania spin-a (bardzo przystępnie!)

+ inne potrzebne materiały/programy są w folderze, inne binarki
+ uruchamianie spin poprzez nakładkę okienkową ispin.tcl:
tclkit8.6b1 ispin.tcl &
ispin.tcl wymaga aby na PATH-ie był program spin (32 lub 64 bitowy, w zależności od os - to konieczne!)
potem otworzyć plik.pml i wybierać różne taby...
+ uruchamianie spin bez ispin.tcl:
spin -a plik.pml; gcc -o pan pan.c
./pan -a -N label_LTL; # z formułą LTL
./pan; # tylko zakleszczenie
obserwować wydruki programu pan...

+ literatura:
Holzmann "The Model Checker SPIN"
Ben-Ari "Principles of the Spin Model Checker"


Zadanie E.1
W algorytmie wzajemnego wykluczania Petersena wykryj błąd, który
pojawia się po przestawieniu 2 pierwszych linii "sekcji we" ...
Do sprawozdania wstaw program .pml, jak i wydruki z okna ispin.

Zadanie E.2
Zaimplementuj prosty algorytm LE (O(n^2) kom.) w promeli,
i sprawdź czy rzeczywiście zawsze działa ...
Dla jak dużej liczby wierzchołków weryfikacja jest "praktyczna" ?
Pamiętać o id_los (id nie powinny być kolejne), oraz o zawiadamianiu nie-liderów!

Problem A: (to nie jest zadanie tylko tekst używany przez 2 zadania!)
Mamy dwa węzły, 1 i 2, połączone dwoma jednokierunkowymi łączami,
w taki sposób, że dane mogą przechodzić od w.1 do w.2 i z powrotem.
"Łącze jednokierunkowe" to rozwiązanie problemu producenta/konsumenta,
z ograniczonym buforem (patrz temat D).
Zakładamy, że:
węzeł 1, na przemian, wysyła 7 i odczytuje 6 bajtów,
węzeł 2, na przemian, odczytuje 7 i wysyła 6 bajtów,
pojemność bufora obu łączy wynosi 5 bajtów,
na początku węzeł 1 ma 23 bajty, a węzeł 2 ma 0 bajtów.
Pytanie: czy wystąpi zakleszczenie?

Zadanie E.3, 1.5pkt
Rozwiąż problem A za pomocą narzędzia spin/promela.
Zbadaj także co się zmieni jeśli węzeł 1 wysyła tyle elem ile ma (gdy jest ich < 7).
Wskazówki:
Możesz wykorzystać przykład prod_kons_siec_4b.pml z folderu;
chyba zamiast ispin.tcl lepiej używać "czystego" spina:
spin -a prod_kons_siec_4b.pml
gcc pan.c -o pan
./pan
./pan -m40000; # jeśli będzie "error: max search depth too small"
Należy starannie czytać wyświetlane przez prog ./pan napisy.
Jeśli ./pan wygeneruje plik plik.pml.trail to można:
1. użyć cmd "spin -t plik.pml" aby zobaczyć zmienne na końcu symulacji,
2. uruchomić ispin.tcl w trybie symulacji wg pliku .trail i prześledzić co się działo.
Komunikat "invalid end state" wyświetlony przez ./pan świadczy o zakleszczeniu!
Uwaga: spin potrafi(!) analizować nieskończone egzekucje...

Zadanie E.4
Zbadaj poprawność rozwiązania problemu producenta i konsumenta ze skończonym buforem,
w którym używa się wyłącznie semaforów binarnych (i pomocniczych zmiennych);
(patrz: zadanie 8 z tematu D).
Skąd wziąć semafory binarne w Promeli? Odp:
inline wait(sem) { atomic { sem; sem=false } }
inline signal(sem) { sem=true }
gdzie sem to zmiena typu bool.

Zadanie E.5
Zdefiniuj semafor ogólny podobnie jak w zadaniu E.4, a następnie
zbadaj poprawność rozwiązania problemu czytelników i pisarzy,
gdy rozmiar czytelni jest znany.
(patrz: zadanie 9 z tematu D).

Zadanie E.6a (1.5pkt) fun. barierowa - weryfikacja
Zbadać przy pomocy spin/promela poprawność rozwiązania
zadania D.1a z "zadań dodatkowych" do tematu D,
dla kilku wątków.

Zadanie E.6b (1.5pkt)
To samo co poprzednio dla D.1b

Sieci Petriego

system modelujemy "graficznie", przy pomocy "miejsc" i "tranzycji" ...

TINA to środowisko wspierające używanie sieci petriego (jedno z wielu!)
obsługuje tpn (=time petri nets), ale także zwykłe pn (=petri nets)
http://projects.laas.fr/tina//papers.php

po zamodelowaniu systemu można przy pomocy TINA:
1. przeprowadzić symulacji pn (prog. nd, Tools| stepper simulator)
2. przeprowadzić standardową analizę pn (prog. nd, Tools| reachability analysis)
3. zbadać czy wyrażenie LTL jest spełnione dla każdej egz. (prog. selt)

+ której wersji tiny używać? 3.4.4
+ inne potrzebne materiały/programy są w folderze
+ nd - graficzny edytor pn
program "nd" to gui dla innych programów pakietu tina...
problem brzydkich fontów: do ~/.ndrc dodac "source guzik_do_fontow.tcl"

+ literatura o sieciach petriego:
Peterson "Petri Nets" - artykuł przeglądowy
Murata "Petri Nets: Properties, Analysis and Applications" - artykuł przeglądowy (dłuższy)
Reisig "Understanding Petri Nets" - książka
Desel, Esparza "FREE CHOICE PETRI NETS" - książka
https://www.informatik.uni-hamburg.de/TGI/PetriNets/


Zadanie E.10, 1.5pkt, problem filozofów jedzących rybę
Zamodelować przy pomocy PN "problem 5 filozofów" w 2 wersjach:
1. bez zabezpieczenia przed zakleszczeniem
2. z zabezpieczeniem
sprawdzic modele przy przy pomocy oprogramowania TINA;
do sprawozdania wstawic: wydruki analityczne tiny,
pliki .ndr, .ndr zamienione na obrazek (jako zalaczniki do sprawozdania)

Zadanie E.11
Zbudujmy małą, przykładową sieć petriego (4 miejsca, 4 tranzycje) ...
proszę ręcznie zbudowac grafy coverability i reachability,
a następnie proszę porównać swoje konstrukcje z tworzonymi przez prog. TINA.
Proszę zrobić to zadanie w 2 wersjach:
1. dla sieci ograniczonej,
2. dla sieci NIEograniczonej.
Do sprawozdania wstawić grafy c/r tworzone przez TINE,
oraz załączyć obrazki wlasnych grafów
(dlatego trzeba je rysować jakims programem graficznym...).
W razie wątpliwości patrz: literatura, artykuł Murata lub Petersona

Zadanie E.12, 1.5pkt, alg. Petersena
Zamodeluj przy pomocy sieci Petriego algorytm sekcji krytycznej Petersena
(patrz: temat D; wyklady, slajd nr 5).
Sprawdź przy pomocy programu selt (tina) czy zapewnia on wzajemne wykluczanie;
zastanów się co jeszcze można sprawdzić poprzez analizę sieci Petriego.
Przypominam o możliwości użycia strzałki z zaprzeczeniem (może tu się przyda).
Przykład użycia programu selt:
tina np01.ndr np01.ktz
selt np01.ktz -q -b -f '<>([](p1<=3))'
TRUE
Plik .ktz to ts (=transition system), mniej więcej to samo co reachability graph,
jego wierz to wszystkie konfiguracje, kraw (strzałki wychodzące) to aktywne tranzycje.
MH, 05.2020: to przypomina "implementowanie" alg Petersena przy pomocy sieci Petriego...

Zadanie E.13, 1.5pkt, problem prod/kons
Rozwiąż problem A za pomocą sieci Petriego.
Wskazówki:
raczej będzie konieczne użycie strzałki z zaprzeczeniem (tzw. inhibitor);
obejrzyj przykłady prod_kons_siec_?.ndr z folderu, w których
mamy 2 lub 3 węzły + 2 łącza, ale przesyła się dane po 1 bajcie...

Zadanie E.14, 1.5pkt, filozofowie c.d.
Zbuduj model filozofa (z problemu "5 filozofów"),
który najpierw losowo wybiera kolejność podnoszenia widelców
i się tego konsekwentnie trzyma...
(Zauważmy, że impl. problemu 5 filozofów przy pomocy semaforów/widelców
często tak właśnie działa!)

Zadanie E.15, 1.5pkt, problem czytelników i pisarzy
Zamodeluj przy pomocy sieci Petriego problem "czytelników i pisarzy",
gdy rozmiar czytelni wynosi 2 krzesła.
Przetestuj czy działa to prawidłowo dla 2 pisarzy i 2 czytelników.
Upewnij się, że rozwiązanie jest na 100% poprawne za pomocą
polecenia "selt" i wyrażeń logiczynych w logice temporalnej
(selt sprawdza czy w każdej możliwej egzekucji warunek jest spełniony).