Page 101 - 4868
P. 101
99 Ошибка! Стиль не определен.
доступ до бази даних. Необхідно уникати «поганих» станів, у яких значення
обох змінних позитивні або значення змінної 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. Однак у захисті операцій
віднімання немає необхідності, оскільки процес, що звільняє ресурс затримки
не потребує. Після дотримання необхідних для захисту умов отримаємо
наступне крупномодульне рішення, представлене у лістингу 1.23.
Лістинг 1.23 – Крупномодульне рішення задачі про читачів та
письменників
int nr = 0, nw = 0;
process Reader[i = 1 to M] {
while (true) {
...
<await (nw == 0) nr = nr+1; >
зчитати базу даних;
<nr = nr-1; >
}
}
process Writer[i = 1 to N] {