Page 126 - 6571

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

процесів кожного із типів та обмеження значень лічильників.
Наприклад, нехай nr та nw – змінні з невід’ємними цілими
значеннями, що зберігають відповідно число процесів-читачів і

процесів-письменників, які отримали доступ до бази даних.
Необхідно уникати «поганих» станів, у яких значення обох
змінних позитивні або значення змінної nw більше 1:

BAD: (nr > 0Ù nw > 0) Ú nw > 1

Доповнююча множина «хороших» станів описується запере-
ченням наведеного вище предиката спрощеного до наступного

виразу:

RW: (nr == 0 Ú nw == 0) Ù nw <= 1

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

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

<nr = nr+1; >
зчитати базу даних;
<nr = nr-1; >

А схема процесу-письменника:

<nw = nw+1; >
записати в базу даних;
<nw = nw-1; >

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

глобальним інваріантом. У процесах-читачах потрібно захистити
операцію приросту змінної nr умовою (nw == 0), оскільки при

збільшенні змінної nr значенням nw повинен бути 0. Процеси-
письменники повинні задовольняти умові
(nr == 0 and nw == 0), оскільки при збільшенні nw бажаним є
нульове значення як для змінної nr, так і для змінної nw. Однак у

125