Page 40 - 4868

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

властивості живучості.Програма завершується, якщо завершується кожен
цикл або виклик процедури, тобтодовжина кожної історії кінцева. Тотальна
(повна) коректність програми – це властивість, що об’єднує часткову
коректність і завершуваність. Програма повністю коректна, якщо вона
завжди завершується, видаючи при цьому правильний результат.
Взаємне виключення – це приклад властивості безпеки в паралельній
програмі.При «поганому» стані два процеси такої програми одночасно
виконують дії в одній критичній секції.У «хорошому» стані кожен процес
виконується у своїй критичній секції.
Для перевірки того, що дана програма задовольняє бажаним
властивостям звичайний застосовується підхід, якій полягає утестуванні,
або налагодженні. Його можна охарактеризувати фразою «запусти програму
і подивися, що вийде».Це відповідає перебору деяких можливих історій
програми і перевірці їх прийнятності.Недолік такої перевірки полягає в тому,

що кожен тест стосується тільки однієї історії виконання, а обмежене число
тестів навряд чи здатне продемонструвати відсутність поганих історій. Також
в результаті тестування можна виявити тільки наявність помилок, а не
гарантувати їх відсутність.Крім того, паралельні програми дуже складні в
тестуванні та налагодженні, оскільки, по-перше, важко зупинити відразу всі
процеси і перевірити їх стан, і, по-друге, в загальному випадку кожне
виконання програми призводить до нової історії.
Другий підхід – використання операторних міркувань, які можна
назвати «вичерпний аналіз варіантів виконання» (перебираються всі можливі
історії виконання програми).Для цього аналізуються способи чергування
неподільних дій процесів.На жаль, в паралельній програмі число можливих
історій зазвичай дуже велике (тому метод є «виснажливим»).Припустимо, що
паралельна програма містить n процесів і кожен з них виконує послідовність
ізm неподільних дій.Тоді число різних історій програми складе(n m )!/ ( ! )m n
.Для програми з трьох процесів, кожний з яких виконує всього дві неподільні
операції, можливими є 90 різних історій!Чисельник у формулі – це кількість
можливих перестановок з n m дій.Але, оскільки кожен процес виконує
послідовність дій, то для нього можливий тільки один порядок виконання
дій.Знаменник відкидає всі варіанти з неправильним порядком виконання
дій.Ця формула дає кількість, рівну числу способів перемішати n колод по
mкарт у кожній, за умови, що відносний порядок карт в кожній колоді
зберігається.
Третій підхід полягає у застосуванні стверджувальних міркувань
(assertional reasoning).Його можна назвати «абстрактним аналізом».У цьому
методі формули логіки предикатів називаються твердженнями і
використовуються для опису наборів станів – наприклад, всіх станів, у яких
x > 0. Неподільні дії розглядаються як предикатні перетворювачі, оскільки
вони змінюють стан програми, що задовольняє одному предикату, на стан,
який задовольняє іншому.Перевагою даного підходу є компактне
представлення станів і їх перетворень.Але ще важливіше те, що він породжує