Programowanie współbieżne i rozproszone/PWR Wykład 11: Różnice pomiędzy wersjami
Nie podano opisu zmian |
|||
| Linia 1: | Linia 1: | ||
== Poprawność programów współbieżnych == | == 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 === | === 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 === | ||
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 == | == Abstrakcyjny model procesu == | ||
Dla potrzeb tej części wykładu wprowadźmy abstrakcyjny model procesu. | |||
=== Definicja === | === Definicja === | ||
Proces modelujemy jako trójkę: <math>(S, R, I)</math>, gdzie: | |||
* <math>S</math> jest skończonym zbiorem stanów | |||
* <math>R</math> jest relacją przejścia: <math>R \subseteq S \times S</math>, przy czym zakładamy dodatkowo <math>dom (R) = S</math> | |||
* <math>I</math> jest zbiorem stanów początkowych: <math>I \subseteq S</math> | |||
=== Przeplot === | === Przeplot === | ||
Wersja z 13:48, 3 paź 2006
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:
