Slajd10

Niezmienniki semaforów

Semafor spełnia poniższe niezmienniki:

* s >= o

ł S = SO + #Sygnały - #Oczekiwania

gdzie:

so - wartość początkowa semafora s,

#Sygnały - liczba wykonanych operacji signai (S), #Oczekiwania - liczba zakończonych operacji Walt (S).

Niezmiennik - własność prawdziwa w każdym stanie każdego możliwego ciągu wykonań.

Programowanie współbieżne z zastosowaniem semaforów. .. 10