PWiR lab 2: Spin - wprowadzenie

Spin jest narzędziem do symulacji i formalnej weryfikacji systemów współbieznych i rozproszonych. Językiem wejściowym jest PROMELA. Narzędzie powstało w Bell Labs w roku 1991, gdzie jest rozwijane do chwili obecnej (ostatnia wersja 6.2.3 z października 2012). Siłą Spina są implementacje wielu znanych efektywnych metod analizy systemów współbieżnych. Zasadniczo, narzędzie to zbudowano z myślą o modelowaniu i weryfikacji protokołów komunikacyjnych, natomiast nadaje się ono także wyśmienicie do dydaktyki programowania współbieżnego i rozproszonego. W Spinie nie zaimplementowano natomiast metod weryfikacji symbolicznej, szeroko stosowanych w przemysłowej weryfikacji hardware'u.

Literatura

G. J. Holzmann, “The Spin Model Checker: Primer and Reference Manual”, Addison-Wesley 2004.
M. Ben-Ari, “Principles of the Spin Model Checker”, Springer 2008.
Strona internetowa wykładu Weryfikacja wspomagana komputerowo, 2010/2011 (serdeczne podziękowania dla Bartka Klina za udostępnienie materiałów z laboratorium).
Strona internetowa narzędzia Spin

Pytania

Sławomir Lasota

Cel

zaznajomienie się z podstawowymi konstrukcjami języka Promela
zaznajomienie się z narzędziem spin
proste ćwiczenia ilustrujące przeploty procesów oraz niedeterminizm

Spis treści

Pliki, z których będziemy korzystać
Promela w Emacs'ies
Podstawowe konstrukcje Promeli
Ekstremalne przeploty - weryfikacja przy użyciu asercji
Siła niedeterminizmu (ćwiczenie samodzielne)

Pliki, z których będziemy korzystać

W niniejszym scenariuszu będziemy korzystać z następujących przykładowych programów (do pobrania tutaj):

promela-mode.el: Tryb Emacs'a do edycji Promeli.
step1-init.pml, step2-proctype.pml, ..., step8-chan2.plm: Proste programy (modele) w Promeli.
increment-par.pml: 2 procesy inkrementujące zmienną globalną w przeplocie.
spina: Przykładowy skrypt do wywoływania weryfikatora.
cannibals.pml: Przykładowe rozwiązanie zadania o kanibalach.

Promela w Emacs'ie

umieść w folderze ~/.emacs.d/ plik promela-mode.el

dopisz to pliku ~/.emacs następujące polecenia:

(add-to-list 'load-path "~/.emacs.d/")

(autoload 'promela-mode "promela-mode" "PROMELA mode" nil t)
        (setq auto-mode-alist
              (append
               (list (cons "\\.promela$"  'promela-mode)
                     (cons "\\.spin$"     'promela-mode)
                     (cons "\\.pml$"      'promela-mode)
                     )
               auto-mode-alist))

syntax-check: C-c/C-s

Podstawowe konstrukcje Promeli

Kolejno obejrzyj następujące pliki od step1-init.pml do step8-chan2.pml. Dla każdego z nich spróbuj przewidzieć efekt uruchomienia, a następnie uruchom poleceniem:

> spin nazwa_pliku

Wykonaj polecenia i odpowiedz na pytania.

step1-init.pml

Hello world. Proces init.

step2-proctype.pml

Pierwszy program współbieżny. Instrukcja run.

step3-params.pml

Procesy z parametrami. Jak spin wybiera wcięcia dla wypisywanych tekstów? (Wskazówka: wyświetl za pomocą printf identyfikator procesu, z predefiniowanej zmiennej _pid.) Opcja spin -T znosi wcięcia.

step4-guards.pml

Zmienne, warunki logiczne jako komendy, blokowanie.

step5-if.pml

Instrukcja warunkowa. Uwaga na niedeterminizm! Lukier syntaktyczny: -> = ;.

step6-do.pml

Pętle.

step6-do-niedet.pml

Niedeterminizm w do.

step7-chan.pml

Kanały komunikacyjne. Różnica między kanałami buforowanymi i niebuforowanymi. Co się stanie, jeśli zamienimy pojemność kanału [1] na [0], czyli jeśli zamienimy kanał buforowany na niebuforowany?

step8-chan2.pml

Sprawdzanie elementów w kanałach.

Promela man pages

Ekstremalne przeploty - weryfikacja przy użyciu asercji

Obejrzyj zawartość pliku increment-par.pml. Jakie wartości końcowe może przyjmować zmienna n? Jaka jest najmniejsza teoretycznie możliwa wartość?

Informacje o symulacji: opcje -p, -g, -l, -w, np.
```
> spin -p -g -w increment-par.pml
```
Interaktywna symulacja: spin -i
Dodaj asercję assert(n <= 20) i wykonaj kolejno polecenia:
```
> spin -a increment-par.pml                   (generuje weryfikator pan.c)
> gcc -O2 -o pan pan.c
> ./pan
```
Szczegółowe objaśnienie formatu wyjściowego weryfikatora znajduje się tutaj.
Sprawdź eksperymentalnie jaka jest najmniejsza możliwa wartość końcowa zmiennej n używając asercji. Np. wyspecyfikowanie assert(n >= 10) spowoduje, że jeśli jest możliwa wartość mniejsza niż 10, to Spin wygeneruje ślad porażki (kontrprzykład) i zapisze go do pliku increment-par.pml.trail.
Śledzenie śladu porażki: opcje spin -t lub spin -k nazwa_pliku

Przykładowy skrypt do wywołania weryfikatora (w pliku spina):

spin -a $1
if [ $? -eq 0 ];
then
  rm $1.trail
  # safety i reach sa dla optymalizacji czasu; bfs szuka jak najkrótszych kontrprzykładów
   gcc -DSAFETY -DREACH -DBFS -o pan pan.c
   ./pan -E -I
   if [ -e $1.trail ];
   then
      spin -t -p $1
   fi
fi

Ciekawostka: zmień w pliku increment-par.pml nazwę zmiennej reg na register i powtórz....

Jak zmieni się wynik, jeśli inkrementacja zmiennej n będzie atomowa? Atomowość uzyskujemy pomijając zmienna reg, czyli n++ zamiast

      reg = n + 1;
      n = reg;

Atomowość można także wymusić w Promeli za pomocą konstrukcji atomic { ... }:

   atomic {
      reg = n + 1;
      n = reg;
   }

Inna konstrukcja, która jest bardziej efektywna ale można ją stosować tylko w niektórych przypadkach:

   d_step {
      reg = n + 1;
      n = reg;
   }

Parametry wywołań:

Parametry wywołania spin'a, zob. też spin --help
Dyrektywy przydatne przy kompilacji weryfikatora
Parametry wywołania weryfikatora

Siła niedeterminizmu (ćwiczenie samodzielne)

Rozwiąż samodzielnie następujące zadanie używając niedeterminizmu.

M misjonarzy i K kanibali ma przeprawić się przez rzekę. Do dyspozycji mają łódkę, którą może płynąć co najwyżej L osóby na raz. Jeśli na którymś brzegu kanibale uzyskają przewagę, to zjedzą misjonarzy. Czy istnieje sposób przeprawienia wszystkich na drugi brzeg tak, aby misjonarze przeżyli? Oczywiście łódka sama nie popłynie!

Wskazówki:

Wykorzystaj niedeterminizm: łódka może odpływać, gdy nie jest pusta, każdy misjonarz i kanibal może zawsze próbować wsiadać do łódki, która znajduje się na tym samym brzegu.
Pamiętaj o warunkach brzegowych: kanibale zjadają misjonarzy nie zawsze wtedy, gdy jest ich więcej na danym brzegu :-)
Zastosuj assert tak, aby kontrprzykład wygenerowany przez spina był rozwiązaniem zadania.
Użyj opcji ./pan -E aby spin nie sprawdzał poprawności zakończenia procesów (end states) -- interesują nas wyłącznie asercje:
```
> spin -a cannibals.pml
> gcc -DSAFETY -o pan pan.c 
> ./pan -E
> spin -t -p cannibals.pml
```
Przetestuj dla M = K = 3, L = 2
Użyj przeszukiwania BFS albo opcji ./pan -E -i aby znaleźć krótszy kontrprzykład
W ilu najmniej krokach wszyscy przeprawią się na drugi brzeg? (Użyj konstrukcji atomic.)
Jeśli nie potrafisz użyć asercji, to użyj formuły LTL'a, np. <> solution, gdzie solution mówi, że wszyscy misjonarze i kanibale przeprawili się przez rzekę. Wtedy weryfikator ./pan powinien być wywołany z opcją -a (acceptance cycles):
```
> spin -a -f "<>solution" cannibals.pml
> gcc -o pan pan.c 
> ./pan -a -E
> spin -t -p cannibals.pml
```

Ostatnia modyfikacja: 24/02/2013