Page 46 - 6571

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

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

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

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

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

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

Властивістю програми називається атрибут, який є істинним
при будь-якій можливій історії програми і, отже, при всіх її вико-
наннях. Існує два типи властивостей: безпека і живучість. Влас-
тивість безпеки полягає в тому, що програма ніколи не потрапляє

в «поганий» стан (при якому деякі змінні можуть мати небажані
значення). Властивість живучості означає, що програма зрештою
завжди потрапляє в «хороший» стан, тобто стан, в якому всі

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

ється). Якщо програмі не вдається завершити виконання, то вона
може ніколи не видати правильний результат, але не існує такої
історії, при якій програма завершується з неправильним резуль-

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

тальна (повна) коректність програми – це властивість, що

45