Page 61 - 4868

59 Ошибка! Стиль не определен.

множини змінних, глобальні інваріанти і синхронізація. Всі вони включають
запис тверджень і дій присвоєння в формі, яка забезпечує істинність
формулам (1).
Нагадаємо, що множина запису процесу – це множина змінних, яким він
присвоює значення (і, можливо, зчитує їх), а множина зчитування процесу –
це множина змінних, які процес зчитує, але не змінює. Множина посилань
процесу – це множина змінних, які зустрічаються у твердженнях, що
доказують коректність даного процесу. Множина посилань процесу часто
(але не завжди) збігається із об’єднанням множин зчитування і запису. По
відношенню до поняття взаємного втручання критичні змінні – це змінні в
твердженнях.
Якщо множина запису одного процесу не перетинається з множиною
посилань іншого процесу і навпаки, то ці два процеси не можуть впливати
один на одного. Формально це відбувається тому, що в аксіомі присвоєння

використовується текстуальна підстановка, яка не впливає на предикат, який
не містить посилань на цільову змінну присвоєння. Локальні змінні в різних
процесах, навіть якщо і мають однакові імена, все одно є різними змінними,
тому перед застосуванням аксіоми присвоєння їх можна перейменувати.
В якості прикладу розглянемо наступну програму.
co x = x+1; // y = y+1; oc

Якщо початкові значення зміннихx та y рівні 0, то згідно аксіоми
присвоєння, теоремами євиступають наступні твердження:

{x == 0} x = x+1; (x == 1}
{y == 0} y = y+1; (y == 1}
Кожен процес містить один оператор присвоєння і два твердження, отже
потрібно довести чотири теореми взаємного невтручання. Кожна з них
тривіально істинна, оскільки два процеси посилаються на різні змінні, тому
підстановки, пов’язані з аксіомою присвоєння, будуть порожніми.
Неперетинні множини записів і посилань утворюють основу для
більшості паралельних ітераційних алгоритмів, таких, наприклад як алгоритм
множення матриць. Ще два приклади – різні гілки дерева можливих ходів в
ігровій програмі можуть досліджуватись паралельно, а множинні транзакції
можуть паралельно переглядати записи у базі даних.

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

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