Readers?Writers Problem
daný program (user), v ktorom sú dve premenné nr, nw také, ze pre nejakú konštantu N platí
invariant 0 ? nr ? N ? 0 ? nw ? N (1)
hodnoty nr, nw sa menia len v nasledujúcich druhoch priradení v programe user:
nr := nr + 1 {started read}
nr := nr ? 1 {end read}
nw := nw + 1 {started write}
nw := nw ? 1 {end write}
(v týchto priradeniach môzu byt aj iné premenné) a program user môze mat aj iné priradenia
Úloha: modifikovat priradenia programu user tak, aby platilo:
invariant nw ? 1 ? (nr = 0 ? nw = 0) (2)
nr, nw znamenajú pocet cítajúcich a zapisujúcich procesov (do súboru) v danom case
pocet procesorov je obmedzený na N (invariant 1)
hocikolko vela môze cítat, ale zápis sa nemôze vykonat súcasne s iným zápisom alebo cítaním