Доказательство. Алгоритм был разработан так, что предикат P, определенный как Pm Ù (P0 Ú P1 Ú P2 ÚP3) - инвариант алгоритма.
Чтобы показать безопасность, заметим, что завершение обнаружевается при t = 0, stateP0 = passive, colorP0 = white, и mcP0 + q = 0.Из этих условий Ø P3, Ø P2, и Ø P1, следовательно Pm Ù P0, из чего вместе с stateP0 = passive и mcP0 + q = 0 следует term.
Чтобы показать живость, заметим, что после завершения основного вычисления счетчики сообщений не изменяют свои значения и их сумма, равняется 0. Волна, начатая в такой конфигурациизаканчивается с mcP0 +q = 0 и все процессы окрашены в белый цвет, что гарантирует, что следующая волна будет успешной. -
В отличие от алгоритма Dijkstra-Feijen-Van Gasteren, алгоритм Сафра не имеет ограниченной сложности для худшего случая; маркер может быть пропущен неограниченное число раз, в то время как все процессы - пассивные, но некоторые основные сообщения находятся в процессе передачи в течение длительный периода времени. Что касается алгоритма Dijkstra-Feijen-Van Gasteren, для основного вычисления со сложностью времени T можно ожидать выполнения Q(T + N) сообщений.
Векторно-расчетный алгоритм. Mattern [Mat87] предложил алгоритм, сопоставимый с алгоритмом Сафра, но который поддерживает отдельный счетчик сообщений для каждого адресата. Для процесса p счетчик сообщений - массив mcp[P]. Когда p посылает сообщение q, p изменяет счетчик mcp [q] := mcp [q]+l и когда p получает сообщение, он изменяет счетчик mcp [p] := mcp [p] - 1. Маркер также содержит массив счетчиков, и когда p обрабатывает маркер, к mcp добавляется в маркер и обнуляется (массив в начале содержит нули). Завершение обнаружено, когда маркер равняется 0.
Алгоритм векторного-подсчета имеет некоторые преимущества по сравнению с алгоритмом Сафра, но также и страдает от некоторых серьезных неудобств. Одно из преимуществ алгоритма состоит в том, что завершение обнаруживается быстрее, а именно за один обход маркера после возникновения завершения. Второе преимущество состоит в том, что пока вычисление не закончилось, маркер приостанавливается чаще, что может уменьшить число управляющих сообщений, используемых алгоритмом. В алгоритме Сафра, каждый пассивный процесс передает маркер; в алгоритме векторного подсчета такой процесс p не будет отправлять маркер если из информации, содержащейся в маркере следует, что сообщение находиться на пути к p.
Главное неудобство алгоритма векторного подсчета состоит в том, что маркер содержит большое количество информации (а именно, целое число для каждого процесса), которую нужно передавать в каждом управляющем сообщении. Это неудобство не обременительно, если число процессов не велико. Другое неудобство состоит в том, что требуется знание идентификаторов других процессов. Если вектор представлен как массив, каждый процесс должен заранее знать идентификаторы всех процессов, но это требование может быть смягчено, если вектор представлен как множество пар целого числа и идентификатора. Первоначально каждый процесс должен знать по крайней мере идентификаторы соседей (чтобы правильно увеличивать счетчик), а другие идентификаторы будут изучены в течение вычисления.
8.3.3 Использование Подтверждений
Алгоритм Сафра подсчитывает основные сообщения, которые посланы и получены, чтобы знать есть ли основные сообщения, находящиесы в процессе передачи. Также возможно гарантировать это используя подтверждения; несколько авторов предложили такое усовершенствование алгоритма Dijkstra-Feijen-Van Gasteren, см., например, Naimi [Nai88]. Это разновидность принципа обсуждается лишь кратко, потому что результирующий алгоритм не во всех смыслах является усовершенствованием алгоритма Shavit-Francez, и поэтому устарел.
Сначала, заметим, что никакое сообщение не находится в процессе передачи эквивалентено для всех p никакое сообщение, посланное p не находится в процессе передачи. Каждый процесс ответственен за сообщения, которые он послало, то есть, он должен позабититься о том, чтобы алгоритм объявления не был вызван, пока не будет уверенности в том, что все основные сообщения, посланные им получены. Метод обнаружения определяет для каждого процесса p локальное условие quiet(p) таким образом, что
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*)
end
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 *)
end
Алгоритм 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, все процессыокрашены в белый цвет, и завершение объявляется в конце следующей волны. -
Решение, основанное на ограниченной задержке сообщений. В [Tel91b, Раздел 4.1,3] классе решений обнаружения завершения (и других проблем) описывается решение основанное на предположении, что задержка сообщений ограничена
постоянной m. (См. также Раздел 3.2). В этих решениях, процесс не является quiet промежуток времяни m после отправления последнего сообщения, также процесс остается черным, пока он не quiet, как описано в решении основанном на использовании подтверждений. Процесс p становится quiet если (1) прошло по крайней мере m времяни после того как прцесс p посылал последний раз сообщения и р пассивен. Полный формальный вывод алгоритма предоствлен читателю.