Введение в распределённые алгоритмы. Ж. Тель (2009) (1185665), страница 81
Текст из файла (страница 81)
Отсюда следует, что процессы при передаче маркера могут менять окраскус black на white, не нарушая истинности утверждения Р.Правило 5. Сразу после передачи маркера всякий процесс окрашиваетсяв цвет white.При таком режиме перемены окраски можно гарантировать, что после завершения базового вычисления какая-нибудь волна рано или поздно окажетсяуспешной. Приведенные здесь рассуждения воплощены в алгоритме 8.7.nТеорема 8.9. Алгоритм Сафры (алгоритм 8.7) является корректнымалгоритмом обнаружения завершения вычислений с асинхронным обменомсообщениями.Д о к а з а т е л ь с т в о .
Рассматриваемый нами алгоритм устроен так, чтоего инвариантом является предикатР, который определяется формулой Pmt\(PoVP\VP2 VlЧтобы обосновать достаточное условие корректности, следует заметить, чтоалгоритм обнаруживает завершение вычисления только тогда, когда выполняютсяравенства t = 0, statePo = passive, colorPo = white и mcPo + q = 0.
Из этихравенств следует выполнимость условий ~^Рз, - 1Р 2 и ^Р\, а это, в свою очередь,308Гл. 8. Обнаружение завершенияозначает, что выполняется условие РтАРо- С учетом того, что statePo = passiveи mcPo+q = 0 , последнее условие влечет за собой выполнимость предиката term.Чтобы обосновать необходимое условие корректности, заметим, что послезавершения базового вычисления счетчики сообщений будут иметь постоянныезначения и сумма их будет равна 0.
Волна, запущенная из такой конфигурации,завершится так, что будет соблюдено равенство тсРо + q = 0 и при этом всепроцессы будут окрашены в цвет white. Следующая за ней волна непременнобудет успешной.□В отличие от алгоритма Дейкстры—Фейджена—ван Гастерена, сложностьв наихудшем случае алгоритма Сафры не ограничена сверху; маркер может передаваться неограниченное число раз, пока все процессы будут пассивны, нокакое-то сообщение будет долгое время пребывать на этапе пересылки. Так жекак и в случае алгоритма Дейкстры—Фейджена—ван Гастерена, математическоеожидание сложности по числу сообщений составляет величину 0(Т + N) длябазового вычисления, имеющего сложность по времени, равную Т.Алгоритм векторного подсчета. Маттерн в работе [141] предложил алгоритм, сравнимый по эффективности с алгоритмом Сафры, но требующий при этомотдельного счетчика сообщений для каждого процесса-адресата.
В процессе р вкачестве счетчика сообщений используется массив тср[Р]. Когда р отправляетсообщение процессу q, содержимое счетчика процесса р изменяется при помощи оператора mcp[q] := mcp[q] + 1 , а когда р получает сообщение, содержимоесчетчика процесса р изменяется при помощи оператора тср[р] := тср [р] ~ 1 .Вместе с маркером передается также и массив счетчиков, и, когда процесс рвладеет маркером, содержимое массива тср передается с маркером, а сам счетчик сбрасывается в 0 (массив, все компоненты которого равны 0). Завершениевычисления регистрируется, когда массив, переносимый маркером, становитсяравным 0 .Алгоритм векторного подсчета обладает некоторыми преимуществами по сравнению с алгоритмом Сафры, но у него есть и серьезные изъяны.
Одно из достоинств этого алгоритма состоит в том, что завершение вычисления обнаруживается быстрее, а именно спустя один тур после того, как завершится базовоевычисление. Другое положительное качество данного алгоритма состоит в том,что, пока вычисление не завершилось, продвижение маркера задерживается более часто, и это позволяет сократить число обменов контрольными сообщениямив ходе работы алгоритма. В алгоритме Сафры каждый пассивный процесс передает маркер; а вот в алгоритме векторного подсчета такой процесс не будетпроводить передачу маркера, если содержащаяся в маркере информация позволяет заключить, что какое-то сообщение находится на этапе пересылки и будетдоставлено процессу р.Главный недостаток алгоритма векторного подсчета состоит в том, что вместес маркером передается большой объем информации (если быть точным, то поодному целому числу для каждого из процессов), и все это передается в каждом контрольном сообщении.
Этот недостаток может быть не столь серьезным,если число процессов невелико. Другой изъян состоит в том, что для этого ал8.3. Решения на основе волновых алгоритмов309горитма требуется знание отличительных признаков всех остальных процессов.Если вектор представляется массивом, то каждый процесс должен быть заранееосведомлен о всем многообразии отличительных признаков процессов системы;но это требование может быть ослаблено, если вектор представляется в видемножества пар, каждая из которых состоит из отличительного признака и целогочисла. Первоначально каждый процесс должен знать отличительные признакисоседних процессов (чтобы правильно увеличивать показания счетчика), а всепрочие отличительные признаки будут изучены по ходу вычисления.: (a c t i v e , p a s s i v e ) ;c o lo r p: ( w h it e , b la c k ) ;unackp: in teg er init 0 ;Sp: { s t a t e p = a c t i v e }begin send (m es) ; u n a c k p := u n a c k p + 1c o lo r p := b la c k(* Правило В *)епгЩД: Сообщение (m es) от q доставленоbegin receive (m es) ; s t a t e p := a c t i v e ;send (ack) to q(* Правило A *)var s i a i e p;(* Правило A *)процессу р }endIp \ { s t a t e p = a c t i v e }A p:begin s t a t e p := p a s s i v e en d{Подтверждение (ack) доставлено процессу p }begin receive (ack) ; u n a c k p := u n a c k p — 1 en d(* Правило A *)Приступить к обнаружению завершения вычисления;исполняется один раз процессом р о :begin send (tok, w h i t e ) to р ц - i endТ„: (* Процесс p владеет маркером (tok, c) *){ s ta te p = p a s s iv e A unackp = 0 }begin if p = poth en if c = w h i t e Л c o lo r p = w h i t eth en A n n o u n c eelse send (tok, w h i t e ) to р ц - ie ls e if (c o lo rp = w h i t e )th en send (tok, c) to N e x t pe ls e send (tok, b la c k ) to N e x tp ;c o lo r p := w h i t e(* Правило В *)endАлгоритм 8.8.Обнаружение завершения вычисления с использованием подтверждений8.3.3.
Использование подтвержденийВ алгоритме Сафры проводится подсчет отправленных и полученных базовыхсообщений, чтобы установить, что никакие базовые сообщения не пребываютна этапе пересылки. Это требование можно обеспечить, используя подтверждения; сразу несколько авторов предложили снабдить этим механизмом алгоритм310Гл. 8. Обнаружение завершенияДейкстры—Фейджена—ван Гастерена (см., например, работу [152]). Подобнуюмодификацию основного метода мы обсудим лишь вкратце, поскольку полученный в результате алгоритм ни в коей мере не улучшает алгоритм Шави—Франчезаи поэтому уже вышел из употребления.Прежде всего заметим, что утверждение «ни одно сообщение не пребываетна этапе пересылки» равносильно утверждению «для каждого процесса р ни одно сообщение, отправленное р, не пребывает на этапе пересылки».
На каждыйпроцесс возлагается ответственность за отправленные им сообщения, т. е. процесс должен предотвратить вызов процедуры Announce , до тех пор пока он неудостоверится, что все отправленные им базовые сообщения достигли адресата.В рассматриваемом методе обнаружения завершения вычисления для каждогопроцесса р локальное условие quietip) определяется так, чтобы выполняласьимпликацияquietip) =*- {stateр = passive А ни одно сообщение, отправленное процессом р ,не пребывает на этапе пересылки).Тогда будет верно, что (Ур : quiet(p)) ==^ term.Чтобы установить, что ни одно сообщение, отправленное процессом р, не пребывает на этапе пересылки, каждое сообщение сопровождается подтверждениеми каждый процесс ведет учет числа подтверждений, которые должны быть имполучены. Точнее говоря, предикат Ра, который определяется соотношениемУр: (unackp =^(сообщения на этапе пересылки, отправленные процессом р)+ # (подтверждения на этапе пересылки, адресованные р)).должен быть инвариантом, что обеспечивается следующим правилом.Правило А.
При отправлении сообщения процесс р увеличивает значениеunackp; при получении сообщения от процесса q, процесс р отправляет процессуq подтверждение; при получении подтверждения процесс р уменьшает значениеunackp.Указанное выше требование для условия quiet (при выполнении условия quietip)процесс р является пассивным, и ни одно сообщение, отправленное процессом р,не пребывает на этапе пересылки) будет теперь соблюдено, если задать условиеquiet следующим соотношениемquietip) = (statep = passive A unackp = 0).Построение нашего алгоритма обнаружения завершения вычисления проводитсяпоэтапно, подобно тому как был построен алгоритм Дейкстры—Фейджена—ванГастерена.
Вначале рассматривается предикат P q, который задается соотношениемР0 = Vi {N > i > t) : quietip).Предикат P i нужно вводить осмотрительно, поскольку активизация процесса р/процессом pi в случае, когда / > t и i ^ t, не происходит совместно с событиемотправления сообщения процессом pi. Однако если процесс pj активизирован8.3. Решения на основе волновых алгоритмов311(вследствие чего предикат P q будет ложным), то соотношениемРь = Ур : (unackp > 0 ==> colorp = black),при помощи правила В, мы приходимРь = Ур : (unackp > 0 ==> colorp = black),при помощи правила В, мы приходим к заключению о том, что, как только предикат P q становится ложным, будет выполнено условие Р \, и поэтому утверждение(Р0 У Р i) не будет опровергнуто.Правило В. После отправления сообщения всякий процесс окрашиваетсяв цвет black; всякий процесс имеет окраску white только когда для него выполняется условие quiet.В результате мы получим алгоритм 8 .8 , инвариант которого задается формулой Ра Л Р& Л (Р0 У Pi У Р2), гдеРа = V/?: (unackp =^(сообщения, отправленные процессом р)-I- # (подтверждения, адресованные р))Рь = Ур: (unackp > 0 =^> colorр = black)Ро = Vt (N > i > t): quiet(p)Pi = 3i (t > / > 0): colorPi = blackP2 = маркер окрашен в цвет black.Теорема 8.10.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
