Programowanie współbieżne i rozproszone/PWR Wykład 11

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

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ę: , gdzie:

  • jest skończonym zbiorem stanów
  • jest relacją przejścia: , przy czym zakładamy dodatkowo
  • jest zbiorem stanów początkowych:


Przeplot

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

Niech będzie procesem. Określmy następujące zbiory:

  • zbiór ścieżek: Parser nie mógł rozpoznać (nieznana funkcja „\nat”): {\displaystyle 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 Parser nie mógł rozpoznać (nieznana funkcja „\inS”): {\displaystyle s\inS} :

Wówczas ciągiem wykonawczym procesu nazwiemy dowolną ścieżkę .

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 będzie przeliczalnym zbiorem zmiennych zdaniowych.

  1. Zbiór formuł stanowych to najmniejszy zbiór, taki że:
    • jeśli , to także
    • jeśli , to także
  2. Zbiór formuł ścieżkowych to najmniejszy zbiór, taki że:
    • jeśli , to
    • jeśli , to

Spójniki definiuje się na formułach stanowych za pomocą oraz

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 , gdzie

  • jest procesem
  • Funkcja Parser nie mógł rozpoznać (nieznana funkcja „\Power”): {\displaystyle \delta: S \rightarrow \Power V} przyporządkowuje każdemu stanowi zbiór f zmiennych zdaniowych prawdziwych w tym stanie.

Funkcję 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 będzie strukturą Kripkego, a dowolnym stanem.

  1. Definiujemy relację dla formuły stanowej :
    • dla mamy wtw, gdy
    • nieprawda, że zachodzi
    • wtw, gdy (jeśli to )
    • wtw, gdy dla wszystkich zachodzi
    • Parser nie mógł rozpoznać (nieznana funkcja „\E”): {\displaystyle K, s \vDash \E\alpha} wtw, gdy dla pewnej ścieżki zachodzi
  2. Definiujemy dla formuły ścieżkowej :
    • wtw, gdy Parser nie mógł rozpoznać (nieznana funkcja „\nat”): {\displaystyle \forall_{i\in\nat} K, p(i) \vDash \phi}
    • wtw, gdy Parser nie mógł rozpoznać (nieznana funkcja „\nat”): {\displaystyle \exists_{i\in\nat} K, p(i) \vDash \phi}
    • wtw, gdy

Powiemy, że struktura Kripkego jest modelem dla formuły stanowej wtw, gdy dla każdego zachodzi .

Przykłady formuł i ich znaczenie

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

  • --- jest niezmiennikiem, zachodzi w każdym stanie każdej ścieżki, bezpieczeństwo
  • --- być może kiedyś zajdzie
  • --- kiedyś na pewno będzie
  • --- być może zawsze będzie
  • --- zachodzi nieskończenie wiele razy
  • --- żywotność egzystencjalna, zaczynając od dowolnego stanu osiągalnego możemy kiedyś osiągnąć
  • --- jeśli znajdziemy się w stanie spełniającym , to na pewno kiedyś dojdziemy do stanu spełniającego , żywotnosc

Weryfikacja modelowa

Dana jest struktura Kripkego oraz formuła stanowa . Sprawdzić, czy .

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:

  1. Zidentyfikuj kluczowe stany procesów, które składają się na program współbieżny.
  2. Utwórz strukturę Kripkego modelującą przeplot ciągów wykonawczych tych procesów.
  3. Wyraź własności żywotności i bezpieczeństwa w postaci formuł logiki CTL.
  4. 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