Page 76 - 6571

дження можна представити у формі I Ù L, то доведення правиль-
ності процесів будуть вільні від взаємного втручання. Справа в
тому, що: 1) предикат I інваріантний щодо кожної дії присвоєння
a ; 2) жодна дія присвоєння в одному процесі не може вплинути

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

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

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

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

ної кількості історій програми.

9.3 Синхронізація процесів

Послідовність операторів всередині оператора await для ін-

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

операторів зумовити втручання. Наприклад, розглянемо наступну
неподільну дію:

<x = x+1; y = y+1;>

Жодне присвоєння саме по собі не може викликати втручан-
ня, оскільки жодний інший процес не може побачити стан, при

якому змінна x уже була збільшена на 1, а змінна y ще ні. Причи-
ною втручання може стати тільки пара присвоєнь.
Внутрішні стани сегментів програми всередині кутових ду-
жок також неподільні. Отже, жодне твердження про внутрішній

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

75