Page 80 - 6571

кутових дужок випливає задоволення умови 2. Інші три власти-
вості будуть задовольнятися при безумовній справедливій страте-
гії планування, оскільки вона гарантує, що процес, який намага-
ється виконати неподільну дію, яка відповідає його критичній се-

кції, зрештою це зробить, незалежно від дій інших процесів. Од-
нак при такому «рішенні» виникає проблема реалізації оператора
неподільності (кутові дужки).

Всі чотири зазначені властивості важливі, проте найбільш
суттєвим є взаємне виключення. Для опису властивості взаємного
виключення необхідно визначити, чи знаходиться процес у своїй
критичній секції. Щоб спростити запис, побудуємо рішення для

двох процесів, CS1 та CS2, яке легко узагальнюється для n проце-
сів.

Нехай in1 та in2 – логічні змінні з встановленим початко-
вим значенням «хиба». Коли процес CS1 (CS2) знаходиться у сво-
їй критичній секції, змінній in1 (in2) присвоюється значення

«істина». Поганий стан, якого необхідно уникати, виникає у ви-
падку, якщо змінні in1 та in2 одночасно мають значення «істи-
на». Таким чином, потрібно, щоб для будь-якого стану виконува-

лося заперечення умови поганого стану.
MUTEX:Ø(in1 Ùin2)

Предикат MUTEX – це глобальний інваріант. Він повинен за-
довольнятися в початковому стані і після кожної операції присво-
єння значень змінним in1 та in2. Зокрема, перед тим, як процес
CS1 увійде в критичну секцію, присвоївши тим самим змінній

in1 значення «істина», він повинен переконатися, що змінна in2
має значення «хиба». Дану дію можна реалізувати за допомогою

наступної умовної неподільної операції.
<await (!in2) in1 = true;>

Оскільки процеси симетричні відносно один-одного, то у

вхідному протоколі процесу CS2 використовується аналогічна
умовна неподільна операція.
Рішення даної задачі показано в лістингу 3. Дана програма

задовольняє умові взаємного виключення. Взаємного блокування
не виникає, оскільки якби кожен процес був заблокований в сво-
єму протоколі входу, то обидві змінні in1 та in2, мали б значен-

ня «істина», а це суперечить тому, що в даній точці коду обидві

79