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

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
• $R$ jest relacją przejścia: $R\subseteq S\times S$, przy czym zakładamy dodatkowo $dom(R)=S$
• $I$ jest zbiorem stanów początkowych: $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: 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} : ${Path}_s=\{p\in \text{<mrow data-mjx-texclass="ORD">Path</mrow>}|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.

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,\dots \}$ będzie przeliczalnym zbiorem zmiennych zdaniowych.

1. Zbiór formuł stanowych $\text{<mrow data-mjx-texclass="ORD">FS</mrow>}$ to najmniejszy zbiór, taki że:
   • $V\subseteq \text{<mrow data-mjx-texclass="ORD">FS</mrow>}$
   • $\perp \in \text{<mrow data-mjx-texclass="ORD">FS</mrow>}$
   • jeśli $\varphi ,\psi \in \text{<mrow data-mjx-texclass="ORD">FS</mrow>}$, to także $(\varphi \to \psi )\in \text{<mrow data-mjx-texclass="ORD">FS</mrow>}$
   • jeśli Parser nie mógł rozpoznać (błąd składni): {\displaystyle \alpha\in\textit{FP}$, to także <math>(A\alpha), (E\alpha)\in\textit{FS}}