Page 62 - 4868

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

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

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

будь-яке критичне твердженняC в обґрунтуванні кожного процесу P має
j
вигляд I  L , де L – предикат відносно локальних змінних. Зокрема, кожна
змінна, на яку посилається предикат L , є або локальною змінною для процесу
P , або глобальною, в яку записує тільки процес P .Якщо всі критичні
j j
твердження можна представити у формі I  L , то доведення правильності
процесів будуть вільні від взаємного втручання. Справа в тому, що:
1) предикат I інваріантний щодо кожної дії присвоєнняa ;2) жодна дія
присвоєння в одному процесі не може вплинути на локальний предикат L в
іншому процесі, оскільки ліва частина присвоєння a відрізняється від
змінних в предикаті L .
Якщо всі твердження використовують глобальний інваріант і локальний
предикат так, як це описано вище, то вимога взаємного невтручання (1)
виконується для кожної пари дій присвоєння та критичних тверджень. Крім
того, необхідно перевірити тільки трійки в кожному процесі, щоб впевнитися
в тому, що кожне критичне твердження має вищеописаний вигляд, а
предикат I є глобальним інваріантом. При цьому немає жодної необхідності
переглядати твердження або оператори в інших процесах. Фактично з масиву
ідентичних процесів досить перевірити тільки один. У будь-якому випадку
необхідно перевірити лише лінійне число операторів і тверджень у порівнянні
із перевіркою експоненціальної кількості історій програми.

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

наступну неподільну дію:
<x = x+1; y = y+1;>

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