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$ ze zbioru $p\in \bigcup _{s\in I}{Path}_s$.