Page 60 - 4868

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

Таким чином, критичне твердження C є інваріантним щодо дії
присвоєння a .
В якості прикладу розглянемо останню з наведених вище програм.
Передумова першого процесу є критичним твердженням. На нього не
впливає оператор присвоєння в другому процесі, оскільки істинна наступна

трійка:
{(x == 0  x == 2)  (x == 0 x == 1)}
x = x+2;
{x == 0 x == 2}

Перший предикат спрощується до x == 0, тому після додавання 2 до
змінної x значення змінної x буде або 0, або 2. Дана трійка висловлює
наступний факт: якщо другий процес виконується перед першим, то на
початку виконання першого процесу змінна x буде мати значення 2. У даній
програмі є ще три критичних твердження: постумова першого процесу та
перед- і постумова другого процесу. Усі інші докази взаємного невтручання
аналогічні наведеному.

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

1. Що розуміють під терміном «логіка програмування»?
2. Із яких правил складається будь-яка формальна логічна система?
3. Коли логіка програмування є несуперечливою щодо інтерпретації?
4. Коли логіка програмування є повною щодо інтерпретації?
5. Як називаються формули у логіці програмування?
6. З чого складається «трійка» у логіці програмування?
7. Які чотири найбільш важливих правила виведення у логіці
програмування Ви знаєте?
8. Що таке інваріант циклу у паралельній програмі?
9. У якому випадку говорять, що один процес втручається в (впливає на)
інший?
10. В чому полягає принцип взаємного невтручання?

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

9.1. Неперетинні множини змінних
Процеси в паралельній програмі виконуються спільно для отримання
загального результату. Ключова вимога для отримання правильного
результату полягає в тому, що процеси не повинні впливати один на одного.
Множина процесів вільна від взаємного впливу, якщо в одному процесі
немає дій присвоєння, які втручаються в критичні твердження іншого
процесу.
Розглянемо три основні методи усунення взаємного впливу, які можна
використовувати для розробки коректних паралельних програм: неперетинні