Specyfikowanie i weryfikacja własności programów współbieżnych. CTL

Poprawność programów współbieżnych

Do tej pory nie zajmowaliśmy się w sposób formalny poprawnością programów współbieżnych. Wspomnieliśmy jedynie, że rozważa się dwie formy poprawności: bezpieczeństwo (albo inaczej zapewnianie) oraz żywotność.

Obecnie zaprezentujemy jedno z wielu możliwych podejść do weryfikacji programów współbieżnych. Pokażemy, w jaki sposób można specyfikować własności bezpieczeństwa i żywotności w logice temporalnej o nazwie Computational Tree Logic. Ponieważ jest to logika rozstrzygalna pokażemy też w jaki sposób, poprzez badanie modeli (ang. model chcecking) można weryfikować poprawność programów współbieżnych.

Własność bezpieczeństwa

Przypomnijmy, że własność bezpieczeństwa wyraża fakt, że nigdy nie dojdzie do sytuacji niepożądanej: nigdy dwa procesy nie będą jednocześnie w sekcji krytycznej, producent nie nadpisze danych w buforze itp. Własność bezpieczeństwa jest własnością statyczną w tym sensie, że pojawia się w specyfikacji problemu.

Własność żywotności

Własność żywotności to własność dynamiczna. Ogólnie można powiedzieć, że warunek żywotności wyraża następujący fakt: Jeśli proces chce wykonać pewną akcję, to w skończonym czasie mu się to uda. Przykładem własności żywotności jest żądanie, aby proces, który chce wejść do sekcji krytycznej w końcu mógł do niej wejść. Podobnie czytelnik, który chce rozpocząć czytanie powinien w skończonym czasie wejść do czytelni.

Przejawem braku żywotności jest zakleszczenie albo zagłodzenie. Zjawiska te polegają na tym, że proces (lub procesy) nie mogą wykonać żadnej pożytecznej pracy. Jeśli jest to zjawisko globalne mówimy o zakleszczeniu, jeśli brak żywotności dotyczy pojedynczego procesu (pojedynczych procesów) mówimy o zagłodzeniu.

Abstrakcyjny model procesu

Dla potrzeb tej części wykładu wprowadźmy abstrakcyjny model procesu.

Definicja

Proces modelujemy jako trójkę: \((S, R, I)\), gdzie:

\(S\) jest skończonym zbiorem stanów
\(dom (R) = S\)
\(I \subseteq S\)

Przeplot

Mając powyższy model procesu można formalnie zdefiniować ciąg wykonawczy procesu:

Niech \(P = (S, R, I)\) będzie procesem. Określmy następujące zbiory:

zbiór ścieżek: \(Path= \{ p: N\rightarrow S\, |\, \forall_{i\in\nat}\; (p(i), p(i+1))\in R \}\)
zbiór ścieżek rozpoczynających się w zadanym stanie \({Path}_s = \{ p\in\textit{Path}\, |\, p(0) = s \}\)

Wówczas ciągiem wykonawczym procesu nazwiemy dowolną ścieżkę \(p\in\bigcup_{s\in I}\,{Path}_s\).

Zauważmy, że zbiór wszystkich ciągów wykonawczych danego procesu jest drzewem.

Computational Tree Logic (CTL)

Computational Tree Logic jest zdaniową logiką temporalną. Można w niej wyrażać nie tylko proste fakty typu własność p zachodzi w pewnym stanie, ale także stwierdzenia zawierające kwantyfikatory dotyczące czasu: kiedyś w przyszłości, zawsze w przyszłości oraz kwantyfikatory dotyczące możliwości: na pewno, może się zdarzyć. Zauważmy, że własności, które chcemy formułować jako warunki poprawności zawierają takie właśnie kwantyfikatory: na pewno nigdy w przyszłości dwa procesy nie będą w sekcji krytycznej.

Składnia

Aby zdefiniować logikę powinniśmy określić co najmniej jej składnię i semantykę. Zaczniemy od definicji składni. Formuły w CTL dzielą się na dwie kategorie: formuły stanowe i formuły ścieżkowe. Ich definicja jest wzajemnie rekurencyjna.

Niech \(V=\{v_1, v_2,\ldots\}\) będzie przeliczalnym zbiorem zmiennych zdaniowych.

Zbiór formuł stanowych \(\textit{FS}\) to najmniejszy zbiór, taki że:
- \(V\subseteq \textit{FS}\)
- \(\perp\in\textit{FS}\)
- jeśli \((\phi \rightarrow \psi)\in \textit{FS}\)
- jeśli \((A\alpha), (E\alpha)\in\textit{FS}\)
Zbiór formuł ścieżkowych \(\textit{FP}\) to najmniejszy zbiór, taki że:
- jeśli \((\phi U\psi)\in \textit{FP}\)
- jeśli \((G\phi), (F\phi), (X\phi)\in\textit{FS}\)

Spójniki \(\neg, \wedge, \vee, \leftrightarrow\) definiuje się na formułach stanowych za pomocą \(\rightarrow\)

Struktura Kripkego

Prawdziwość formuł w logice CTL będziemy wyliczać w strukturach Kripkego. Intuicyjnie, struktura Kripkego to proces wzbogacony o wartościowanie zmiennych zdaniowych w każdym stanie. Innymi słowy: z każdym stanem procesu związujemy zbiór faktów (zmiennych zdaniowych), które w tym stanie są prawdziwe. Ponieważ proces wykonuje się (zmienia stany zgodnie z relacją przejścia) to prawdziwość zmiennych zdaniowych zmienia się w czasie.

Struktura Kripkego to czwórka uporządkowana \((S, R, I, \delta)\), gdzie

\((S, R, I)\) jest procesem
Funkcja \(\delta: S \rightarrow \Power V\) przyporządkowuje każdemu stanowi zbiór f zmiennych zdaniowych prawdziwych w tym stanie.

Funkcję \(\delta\) można uważać za wartościowanie zmiennych zdaniowych, ale wartościowanie to zależy od stanu, w którym znajduje się proces.

Semantyka

Mając strukturę Kripkego i formułę CTL możemy rozstrzygać, czy jest ona prawdziwa w tej strukturze. Najpierw jednak musimy zdefiniować prawdziwość formuły stanowej w określonym zadanym stanie oraz prawdziwość formuły ścieżkowej dla zadanej ścieżki.

Niech \(s\in S\) dowolnym stanem.

Definiujemy relację \(\phi\):
- dla \(v\in\delta(s)\)
- nieprawda, że zachodzi \(K, s \vDash \perp\)
- \(K, s \vDash \psi\))
- \(K, p \vDash \alpha\)
- \(K, p \vDash \alpha\)
Definiujemy \(\alpha\):
- \(\forall_{i\in\nat} K, p(i) \vDash \phi\)
- \(\exists_{i\in\nat} K, p(i) \vDash \phi\)
- \(K, p(1) \vDash \phi\)

Powiemy, że struktura Kripkego \(K, s \vDash \phi\).

Przykłady formuł i ich znaczenie

A oto przykładowe formuły i ich sens:

\(\phi\) jest niezmiennikiem, zachodzi w każdym stanie każdej ścieżki, bezpieczeństwo
\(\phi\)
\(\phi\)
\(\phi\)
\(\phi\) zachodzi nieskończenie wiele razy
\(\phi\)
\(\psi\), żywotnosc

Weryfikacja modelowa

Dana jest struktura Kripkego \(\phi\). Sprawdzić, czy \(K \vDash \phi\).

Można pokazać, że zadanie to sprowadza się do wielokrotnego przeszukiwania grafu reprezentującego proces. Zatem problem sprawdzenia, czy dana struktura Kripkego jest modelem dla zadanej formuły jest rozstrzygalny. Można to wykorzystać proponując następujący sposób weryfikacji programów współbieżnych:

Zidentyfikuj kluczowe stany procesów, które składają się na program współbieżny.
Utwórz strukturę Kripkego modelującą przeplot ciągów wykonawczych tych procesów.
Wyraź własności żywotności i bezpieczeństwa w postaci formuł logiki CTL.
Sprawdź, czy struktura Kripkego utworzona w punkcie 2 jest modelem dla tych formuł.

Zadanie to można przeprowadzić za pomocą narzędzi wspomagających takich jak na przykład SMV. A oto formalizacja algorytmu Petersona z pierwszego wykładu w postaci kodu w SMV.

Weryfikacja poprawności algorytmu Petersena

MODULE main
VAR
  chce1 : boolean;
  chce2 : boolean;
  kto : {1, 2};
  proc1 : process proc1(chce1,chce2,kto);
  proc2 : process proc2(chce1,chce2,kto);

ASSIGN
  init(chce1) := 0;
  init(chce2) := 0;

SPEC
  AG (! (proc1.stan = sekcja & proc2.stan = sekcja))

MODULE proc1 (chce1,chce2,kto) 
VAR
  stan : {wlasne,chce,zmkto,while1,while2,sekcja,wyjscie}; 
ASSIGN
  init(stan) := wlasne;
  next(stan) := 
   case 
     stan = wlasne :  {wlasne, chce};
     stan = chce : zmkto;
     stan = zmkto : while1; 
     stan = while1 & !chce2 : sekcja;
     stan = while1 & chce2 : while2;
     stan = while2 & kto!=1 : sekcja;
     stan = while2 & kto=1 : while1;
     stan = sekcja : {sekcja, wyjscie};
     stan = wyjscie : wlasne;
     1: stan;
   esac;
 next(chce1) := 
   case
     stan = chce : 1;
     stan = wyjscie : 0;
     1 : chce1;
   esac;
 next (kto) := 
   case 
     stan = zmkto : 1;
     1 : kto;
   esac;
SPEC
  AG (stan = chce -> AF stan = sekcja)

FAIRNESS
  running

FAIRNESS
  stan != sekcja

MODULE proc2 (chce1,chce2,kto)
VAR
  stan : {wlasne,chce,zmkto,while1,while2,sekcja,wyjscie};
ASSIGN
 init(stan) := wlasne;
 next(stan) := 
   case 
     stan = wlasne :  {wlasne, chce};
     stan = chce : zmkto;
     stan = zmkto : while1; 
     stan = while1 & !chce1 : sekcja;
     stan = while1 & chce1 : while2;
     stan = while2 & kto!=2 : sekcja;
     stan = while2 & kto=2 : while1;
     stan = sekcja : {sekcja, wyjscie};
     stan = wyjscie : wlasne;
     1: stan;
   esac;
 next(chce2) := 
   case
     stan = chce : 1;
     stan = wyjscie : 0;
     1 : chce2;
   esac;
 next (kto) := 
   case 
     stan = zmkto : 2;
     1 : kto;
   esac;

SPEC
  AG (stan = chce -> AF stan = sekcja)

FAIRNESS
  running

FAIRNESS
  stan != sekcja

Informatyka MIMUW