Page 77 - 6571

{x == 0 Ùy == 0}
<x = x+1; {x == 1Ùy == 0}; y = y+1;>
{x == 1 Ùy == 1}

Ці дві властивості неподільних дій призводять до виникнення

двох способів використання синхронізації для усунення взаємно-
го впливу: взаємного виключення та умовної синхронізації. Розг-
лянемо наступний фрагмент:

coP : ... a;...
1
// P : ... S ;{C} S ;...
2 1 2
oc

де a – оператор присвоєння в процесі P , а S та S – оператори в
1
2
1
процесі P . Критичне твердження C є передумовою оператора
2
S .
2
Припустимо, що a впливає на C . Перший спосіб позбутися
даного впливу полягає у використанні взаємного виключення, з

метою «приховування» твердження C від оператора a . Для цьо-
го оператори S та S другого процесу можна об’єднати в єдину
1 2
неподільну дію.

<S ; S ;>
1 2
Тепер оператори S та S виконуються неподільним чином, і
1 2
стан змінних стає невидимим для інших процесів.
Інший спосіб уникнути взаємного впливу процесів – викори-
стання умовної синхронізації, з метою посилення передумови

оператора a . Зокрема, можна замінити присвоєння наступною
a
умовною неподільною дією:

<await (!CorB)a;>

де B – предикат, що характеризує множину станів, при яких ви-
конання присвоєння a зробить C істинним. Таким чином, в да-

ному виразі втручання усувається або очікуванням того, що C
стане хибним (тоді оператор S не буде виконаним), або забезпе-
2
ченням того, що виконання a зробить C істинним (що дозволить
виконання оператора S ).
2

Запитання для самоперевірки

76