Составители:
посылает его в сеть и следит, не возникнет ли конфликт с дру-
гими сообщениями от других контроллеров. Если конфликтов не
наблюдается, то считается, что сообщение послано удачно; в про-
тивном случае посылка повторяется через случайный промежуток
времени. Такой протокол называется “двоичным экспоненциальным
протоколом отхода”.
Замечание 3. Если S состоит из одного оператора skip, то про-
токол упрощается; в частности, если условие B удовлетворяет усло-
вию “не больше одного”, то оператор < await (B); > реализуется в
виде while (!B) skip;.
§6 Алгоритм разрыва узла
Вспомним крупномодульное решение задачи о критической секции.
1) bool in1 = false, in2 = false;
2) ## INY : ¬(in1 ∧ in2) — глобальный инвариант
3) process CS1 {
4) while (true) {
5) < await (!in2) in1 = true; > # вход
6) [критическая секция];
7) in1 = false; # выход
8) [некритическая секция];
9) }
10) }
11) process CS2 {
12) while (true) {
13) < await (!in1) in2 = true; > # вход
14) [критическая секция];
15) in2 = false; # выход
16) [некритическая секция];
17) }
18) }
52
Страницы
- « первая
- ‹ предыдущая
- …
- 49
- 50
- 51
- 52
- 53
- …
- следующая ›
- последняя »
