quiet(p) Þ (statep = passive Ù никакие основный сообщения, посланные процессом р не находятся в процессе передачи)
удовлетворен. Тогда ("p : quiet(p)) Þ term.
Чтобы устанавить, что никакое сообщение, посланное p не находится в процессе передачи, каждое сообщение подтверждается, и каждый процесс поддерживает счетчик числа подтверждений, которые он должен еще получить. Формально, утверждение Pa определяется как
Pa = " p : (unackp = # (передается сообщение,посланное p) + # (передается подтверждение для p))
и поддерживается инвариант в соответствии с следующим правилом.
var statep : (active, passive) ;
colorp : (white, black) ;
unackp : integer init 0 ;
Sp: { statep = active }
begin send (mes) ; unackp:= unackp + 1 : (* Правило A *)
colorp := black (*Правило B *)
end
Rp: { сообщение ( mes ) из q прибыло в p }
begin receive (mes) ; statep := active ;
send (ack) to q (*Правило A*)
Ip: { statep = active }
begin statep := passive end
Ap: { подтверждение (ack) прибыло в p }
begin receive (ack) ; unackp := unackp – 1 end (* Rule A *)
Начало определения, исполняется один раз процессом p0:
begin send ( tok, white ) to pN -1 end
Tp: (* Процесс p обрабатывает маркер (tok,c) *)
{ statep = passive Ù unackp = 0 }
begin if p = p0
then if c = white Ù colorp = white
then Announce
else send (tok, white ) to pN -1
else if (colorp = white)
then send ( tok, c ) to Nextp
else send ( tok, black ) to Nextp ;
colorp := white (*Правило B *)
Алгоритм 8.8 обнаружения завершения, использующие подтверждения.
Правило A. При посылке сообщения, p увеличивает unackp, при получение сообщения от q, p посылает подтверждение q ; при получении подтверждения, p уменьшает на 1 unackp.
Требования для quiet (а именно, что из quiet(p) следует, что p пассивен и никакое основное сообщение, посланное p не находится в процессе передачи) будут удовлетворены, если quiet определить как
quiet(p) º (statep= passive Ù unackp = 0).
Начало алгоритма обнаружения похоже на начало алгоритма Dijkstra-Feijea-Van Gasteren. Начинаем с рассмотрения утверждение P0 ,определенного как
P0 º " i (N > i> t) : quiet(p).
Представление P1 нужно выбирать осторожно, потому что активация процесса pj с j> t процессом pi с i £ t не имеет место в том же самом событии,что и посылка сообщения процессом pi. Это имеет место, однако, что, когда pj активизирован (таким образом, что P0 ложь ), unackPi > 0. Следовательно, если утверждение Pb определенное как
Pb º " p : (unackp > 0 Þ colorp = black),
Поддерживается наблюдением
Правило B. Когда процесс посылает сообщение, он становится черным; процесс становится белым только, когда он quiet.
Заключение снова подтветждает, что когда P0 обращается в ложь, P1 сохраняется, следовательно (P0 Ú P1) не обращается в ложь.
Результируещий алгоритм дается как Алгоритм 8.8, и инварианта - Pa Ú Pb Ú (P0 Ù P1 ÙP2 ) , где
Pa º" p : (unackp =: #(передается сообщение посланное p)
+ #(передается подтверждение для p))
Pb º" p : (unackp > 0 Þ colorp = black)
P0 º" i (N > i> t) : quiet(p)
P1 º$ i (t ³ i ³ O): colorPi , = black
P2 º маркер черный.
Теорема 8.10 Алгоритма 8.8 - правильный алгоритм обнаружения завершения для вычислений с асинхронным прохождением сообщений.
Доказательство. Завершение объявляется, когда p0 quiet и обрабатывает белый маркер. Из этих условий следует, что ØP2 и ØP1, а следовательно Pa Ù Pb ÙP0 сохраняются. Вместе с quiet(p0) (p0) это означает, что все процессы quiet, следовательно сохраняется term.
Когда основное вычисление заканчивается, через некоторое время получены все подтверждения, и все процессы становятся quiet. Когда заканчивается первая волна, которая начинается, когда все процессы quiet, все процессыокрашены в белый цвет, и завершение объявляется в конце следующей волны. o
Решение, основанное на ограниченной задержке сообщений. В [Tel91b, Раздел 4.1,3] классе решений обнаружения завершения (и других проблем) описывается решение основанное на предположении, что задержка сообщений ограничена
постоянной m. (См. также Раздел 3.2). В этих решениях, процесс не является quiet промежуток времяни m после отправления последнего сообщения, также процесс остается черным, пока он не quiet, как описано в решении основанном на использовании подтверждений. Процесс p становится quiet если (1) прошло по крайней мере m времяни после того как прцесс p посылал последний раз сообщения и р пассивен. Полный формальный вывод алгоритма предоствлен читателю.
8.3.4 Обнаружение завершения с помощью волн
Страницы: 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90
