Vlastnosti programu
- vlastnost programu je dána tvrzením o jeho historii
- program tuto vlastnost má, pokud je pravdivé pro každou historii
- vlastnost bezpečnosti - tvrzení o nežádoucím stavu, musí být nepravdivé v každém stavu historie
- vlastnost živosti - program se dostane do žádoucího stavu
Kritická sekce
- část programu, kde se pracuje se sdílenými zdroji
- platí zde několik pravidel
- vzájemné vyloučení - maximálně 1 proces je v kritické sekci - bezpečnost
- absence uváznutí - pokud se 2 procesy snaží vstoupit do kritické sekce, alespoň 1 uspěje - životnost
- absence zbytečného čekání - pokud se proces snaží vstoupit do kritické sekce a další v ní nejsou nebo již skončili, tak musí uspět - bezpečnost
- zaručení vstupu - pokud se proces snaží vstoupit do kritické sekce, jednou musí uspět - životnost
Dekkerův algortimus
- řeší problém vzájemného vyloučení
- používá se pro 2 procesy
- nevyžaduje atomické operace
- není zdaleka tak efektivní, protože neustále testuje podmínku (nevyužívá uspání)
- proměnné pro to, kdo chce vstoupit do kritické sekce
bool wantA, bool wantB
- proměnná určující kdo má přednost
int turn
Petersonův algortimus (tie-breaker)
- vychází z Dekkerova algoritmu
- proměnná
last indikuje, kdo poslední začal vykonávat vstup
- akce
await not in2 or last = 2 nemusí být atomické
- zobecnění je opět kompikované (obvykle 2 procesy)
