SO-1st-2.3-w11.tresc-1.0-Slajd24
Poprawność rozwiązania problemu wzajemnego wykluczania
Zasadnicze założenie na potrzeby analizy poprawności rozwiązania problemu wzajemnego wykluczania to skończony czas przebywania procesu w swojej sekcji krytycznej .
Warunkiem bezpieczeństwa jest wzajemne wykluczanie, co oznacza, że nigdy w systemie nie może zaistnieć stan, w którym dwa (lub więcej) procesy byłyby w swojej sekcji krytycznej.
Warunek postępu oznacza, że jeśli nie ma żadnego procesu w sekcji krytycznej, a są procesy w sekcji wejściowej, to jeden z nich w skończonym czasie (po zajściu skończonej liczby zdarzeń w systemie) wejdzie do sekcji krytycznej.
Warunek postępu nie gwarantuje, że konkretny proces wejdzie do sekcji krytycznej. Może się zdarzyć tak, że w momencie przejścia do sekcji wyjściowej, proces opuszczający sekcję krytyczną do sygnał do wejścia procesom oczekującym w sekcji wejściowej, w wyniku którego jakiś proces wejdzie do sekcji krytycznej, a inny (przy zachowaniu warunku bezpieczeństwa) oczywiście nie wejdzie. Przy kolejnym sygnale ze strony procesu wychodzącego z sekcji krytycznej pominięty poprzednio proces ponownie może nie uzyskać prawa wejścia, podczas gdy inny proces wykonujący swoją sekcję wejściową prawo takie dostanie. Sytuacja może się powtarzać w nieskończoność. Postęp jest zachowany bo jakiś proces wchodzi do sekcji krytycznej, ale istnieje proces permanentnie pomijany.
Warunek ograniczonego czekania gwarantuje właśnie, że każdy proces ubiegający się o wejście do sekcji krytycznej w końcu (w skończonym czasie, po skończonej liczbie zdarzeń w systemie) uzyska prawo wejścia do niej. Warto podkreślić, że nie wszystkie algorytmy gwarantuję tę własność.
