Page 75 - 6571

{x == 0} x = x+1; (x == 1}
{y == 0} y = y+1; (y == 1}

Кожен процес містить один оператор присвоєння і два твер-

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

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

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

9.2 Глобальні інваріанти

Ще один, дуже ефективний спосіб уникнення взаємного
втручання полягає у використанні глобального інваріанта для об-
ліку всіх відносин між спільними змінними. Глобальний інварі-

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

змінні. ТодіI називається глобальним інваріантом по відношен-
ню до множини процесів, якщо:
1) I має значення «істина» на початку виконання процесів;

2) I зберігається кожною дією присвоєння.
Умова 1 задовольняється, якщо предикат I має значення «іс-
тина» в початковому стані кожного процесу. Умова 2 задоволь-

няється, якщо для будь-якої дії присвоєння a предикат I має
значення «істина» після виконання a за умови, що предикат I
мав значення «істина» до виконання a. Таким чином, ці дві умо-
ви утворюють приклад використання математичної індукції.

Припустимо, що предикат I є глобальним інваріантом. При-
пустимо, що будь-яке критичне твердження C в обґрунтуванні
кожного процесу P має вигляд I Ù L, де L – предикат відносно
j
локальних змінних. Зокрема, кожна змінна, на яку посилається

предикат L, є або локальною змінною для процесу P , або глоба-
j
льною, в яку записує тільки процес P . Якщо всі критичні твер-
j
74