Automatyczna weryfikacja algorytmów asynch czyli "model checking", narzędzie Spin|Promela¶
weryfikujemy algorytmy ASYNCHRONICZNE (lub systemy, urządzenia, ...)
"message passing", "shared memory", ...
sprawdzamy czy pewien WARUNEK jest spełniony dla KAŻDEJ możliwej egzekucji algorytmu
(konfiguracja początkowa + ciąg zdarzeń obliczeniowych)
WARUNEK jest wyrażony w logice temporalnej (LTL= Linear TL); np:
"<>[] X" w każdej egzekucji, od pewnego momentu spełniony jest warunek X,
"[] X" w każdej egzekucji, zawsze jest spełniony X
"model checking", a nie "program checking"
chodzi o "model" algorytmu (uproszczony!)
istnieją różne podejcia do tego problemu:
- Spin/Promela - C podobny j. programowania/modelowania (to tutaj omawiamy !)
- Sieci Petriego - model buduje się graficznie, z "miejsc" i "tranzycji"
język Promela¶
http://spinroot.com/
http://spinroot.com/spin/Man/promela.html
"Promela" to uproszczony j. C wyposażony w dodatkowe konstr/idee:
typy zmiennych: tylko całkowite (bit, bool, byte, short, int) oraz tablice;
trzeba używać OSZCZĘDNIE !
w zasadzie NIE MA tu procedur !?
(bo chodzi o modelowanie, nie programowanie)
// tworzy N współbieżnie działających procesów:
active [N] proctype mojProces() {
// kod procesu
}
// kanały (do "message passing")
chan mojKanal = [max_liczba_kom] of {lista_typów}
// każdy komunikat to ciąg liczb, plus ew. typ "mtype" (=enum)
// oraz instrukcje do wysyłania/odbierania komunikatów:
mojKanal ! wart1, wart2, ...; // wysyłanie, może blokować
mojKanal ? zm1, zm2, ...; // odczyt, może blokować
// wyrażenie LTL z etykietą w kodzie programu
ltl L1 {<>[] (a==6)}
// od pewnej chwili jest spełniony warunek a==6; a - zm. globalna
ltl L2 {[] (a1==a2)}
// zawsze jest spełniony warunek a1==a2
// non-determinizm (modelowanie, nie programowanie (?))
if
:: wyr1 -> instr1a; instr1b; ...; // wykonują się jeśli warunek "wyr1" spełniony
:: wyr2 -> instr2a; instr2b; ...;
:: instr3; ...; // może być bez warunku
:: else -> instr; ...; // jeśli żaden wyrX nie jest spełniony (bez instr3 (?))
fi
// pętla; najlepiej jeśli zawsze 1 z wyrX jest spełniony
do
:: wyr1 -> instr1a; instr1b; ...; // wyjście z pętli przez "break"!
:: wyr2 -> instr2a; instr2b; ...;
:: else -> instr; ...;
od
// "dziwne" konstrukcje:
wyr -> instr_a; instr_b; ...; // BLOKUJE, jeśli wyr NIE jest spełniony
wyr; instr_a; instr_b; ...; // ... to samo (!)
zm = (war -> wart1 : wart2); // trochę inaczej niż w Cprogram spin¶
"spin" potrafi uruchomić program w Promeli (non-det jest losowy):
spin mojprog1.pml"spin" potrafi także wygenerować program w j. C,
który bada wszystkie możliwe egzekucje,
i sprawdza czy warunek LTL jest spełniony ...
to jest właśnie weryfikacja ...
UWAGA na eksplozję kombinatoryczną - to jest główne niebezpieczeństwo !!!
przypomnienie pojęć:
każdy proces ma skończoną liczbę stanów;
konfiguracja to stany wszystkich procesów
oraz wartości zm. globalnych, w tym zawartość kanałów;
możemy przejść z danej konfiguracji do innej
poprzez zdarzenie obliczeniowe;
zdarzenie obliczeniowe to wykonanie pojedynczej instrukcji
programu w Promeli (w przypadku instr non-det trzeba podać "opcję" ...)
nakładka graficzna na program "spin": ispin.tcl;
ważne opcje: "Verification", "Simulate / Reply";
jeśli podczas weryfikacji prog np01.pml wystąpi błąd,
to jest tworzony plik np01.pml.trail
który można potem "prześledzić" ...
// Przykład:
// 5 procesów zwiększających zm. globalną "a" o 1, 3x...
byte a= 0; // wydaje się, że po jakimś czasie powinno być a==15
active [5] proctype P() {
byte tmp, i;
i=0;
do
:: i>=3 -> break;
:: else -> tmp=a; tmp++; a=tmp;
// tak robią "a++" prymitywne procesory (na rejestrach typu AX itp)
i++;
od
}
ltl L1 {<>[] (a==15)}
ltl L2 {! <>[] (a==4)}
ltl L3 {! <>[] (a==2)}
/*
L1 - klasyczne sprawdzenie, że algorytm nie działa...
L2 - jest po to aby pokazać, że na końcu może być a==4
L3 - nie dziala, wlacza sie OOM killer !!
*/praktyka spin/promela¶
http://spinroot.com/
http://spinroot.com/spin/Man/promela.html Language Reference
http://spinroot.com/spin/Man/Manual.html Basic Spin Manual
http://spinroot.com/spin/Man/index.html Spin Online Reference
SpinIntro.pdf: slajdy opisujące zasadę działania spin-a (bardzo przystępnie!)
inne potrzebne materiały/programy są w folderze
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)
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; # badamy tylko zakleszczenie
obserwować wydruki programu pan...literatura o spin/promela:
Holzmann "The Model Checker SPIN"
Ben-Ari "Principles of the Spin Model Checker"
Zadania¶
Zadanie 70 (1.5pkt) LE w Promeli
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!
Spróbuj także sprowokować sytuację, w której alg LE nie działa (np. niewłaściwe ID).
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 tzw. problemu producenta/konsumenta,
z ograniczonym buforem. 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 71 (1.5pkt) "Problem A" w Promeli
Rozwiąż problem A za pomocą narzędzia Spin/Promela.
Zbadaj co się zmieni jeśli oba węzły zamiast liczby 6 używają 7,
Wskazówki:
Możesz wykorzystać przykład prod_kons_siec_4b.pml z folderu wyżej;
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:
- użyć cmd "spin -t plik.pml" aby zobaczyć zmienne na końcu symulacji,
- 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 72 (1.5pkt) prod i kons, sem ogólne
Zbadaj poprawność rozwiązania problemu producenta i konsumenta ze skończonym buforem,
w którym używa się semaforów ogólnych...
Skąd wziąć semafory ogólne w Promeli?
to jest semafor binarny:
inline wait(sem) { atomic { sem; sem=false } }
inline signal(sem) { sem=true }
//gdzie sem to zmiena typu bool.spróbuj w podobny sposób zdef semafor ogólny.
Materiały o współbieżności i semaforach, patrz tutaj
Zadanie 73 (1.5pkt) czyt i pisarze, sem ogólne
Zbadaj poprawność rozwiązania problemu czytelników i pisarzy,
gdy rozmiar czytelni jest znany.
Materiały o współbieżności i semaforach, patrz tutaj
Zadanie 74 (1.5pkt) funkcja barierowa, aktywne czekanie
W modelu asynch ze wspólną pamięcią (wielowątkowość), w języku Promela,
zdefiniuj funkcję barierową przypominającą "fiber yield" z symulatora.
Przetestuj czy funkcja działa poprawnie dla kilku wątków
wykonujących nieskończoną pętlę z rundami i z licznikiem rund.
Przetestuj poprawność rozwiązania przy pomocy prog spin...
Zadanie 75 (1.5pkt) funkcja barierowa, bez aktywnego czekania
To samo co w poprzednim zadaniu, ale bez aktywnego czekania
(tzn. że trzeba koniecznie użyć narzędzi typu semafory...).