Page 74 - 6571

ЛЕКЦІЯ 9

ТЕХНІКА УСУНЕННЯ ВЗАЄМНОГО ВТРУЧАННЯ

9.1 Неперетинні множини змінних

Процеси в паралельній програмі виконуються спільно для

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

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

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

них, яким він присвоює значення (і, можливо, зчитує їх), а мно-
жина зчитування процесу – це множина змінних, які процес зчи-
тує, але не змінює. Множина посилань процесу – це множина

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

По відношенню до поняття взаємного втручання критичні змінні
– це змінні в твердженнях.
Якщо множина запису одного процесу не перетинається з

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

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

менувати.
В якості прикладу розглянемо наступну програму.

co x = x+1; // y = y+1; oc

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

73