Составители:
CS[i] сначала turn[i] присваивает значение на 1 больше, чем мак-
симальное значение элементов массива turn, а затем ждет, пока
значение turn[i] станет наименьшим среди ненулевых элементов
массива turn.
Этот алгоритм называется алгоритмом поликлиники.
Соответствующий предикат имеет вид
CL :
∀i : 1 ≤ i ≤ n :
(CS[i] в своей критической секции) ⇒ (turn[i] > 0)∧
(turn[i] > 0) ⇒ (∀j : 1 ≤ j ≤ n, j! = i :
turn[j] == 0 ∨ turn[i] < turn[j])
КРУПНОМОДУЛЬНОЕ РЕШЕНИЕ АЛГОРИТМА
ПОЛИКЛИНИКИ
int turn[1 : n] = ([n]0);
## глобальный инвариант — предикат CL
process CS[i = 1 to n] {
while (true) {
< turn[i] = max(turn[1 : n]) + 1; >
# поскольку это неделимая операция, то все получат
# уникальные номера
for [j = 1 to n st j! = i]
< await (turn[j] == 0 or turn[i] < turn[j]);
# или 0 или наша очередь меньше —
# значит, можно “крутнуть” ц ик л:
# если цикл пройдет, то наша очередь меньше всех
[критическая секция];
turn[i] = 0;
[некритическая секция];
}
}
Первое неделимое действие обеспечивает уникальность всех
ненулевых значений массива turn. Второе неделимое действие обес-
57
Страницы
- « первая
- ‹ предыдущая
- …
- 54
- 55
- 56
- 57
- 58
- …
- следующая ›
- последняя »
