Введение в распределённые алгоритмы. Ж. Тель (2009) (не распознанно) (1185664), страница 81
Текст из файла (страница 81)
В качестве первого приближения положим P = P m ∧ P0 , где предикат P08.3. Решения на основе волновых алгоритмов305задается следующим образом:P0 ≡ ∀i (N > i > t) : statepi = passive ∧ q =XN>i>tmcpi .И действительно, P0 обращается в истину, когда t = N − 1 и q = 0, причемв случае t = 0 из условия P следует утверждение(∀i > 0 : statepi = passive) ∧ (mcp0 + q = B).Поэтому p0 может обнаружить завершение базового вычисления, если будут выполнены равенства statep0 = passive и mcp0 + q = 0.Утверждение P0 выполняется, когда процесс p0 запускает волну, передаваямаркер процессу pN−1 с пометкой q = 0. При передаче маркера утверждение P 0будет оставаться верным в том случае, когда в передаче маркера участвуют только пассивные процессы, и при этом к пометке маркера добавляется показаниесчетчика сообщений.
Таким образом, мы вводим следующее правило.Правило 1. Только пассивный процесс может работать с маркером, и еслипроцесс передает маркер, то он добавляет к пометке маркера q значение своегосчетчика сообщений.При таком режиме работы условие P сохраняется как при передаче маркера,так и при выполнении внутренних действий. К сожалению, P не сохраняется приполучении сообщения таким процессом pi , для которого i > t.
Опровержениепредиката P0 происходит, как только будет получено некоторое сообщение, т. е.это возможно только при условии B > 0. Поскольку до получения этого сообщения утверждение P0 было верно, это означает, что в таком случае должновыполняться условие P1 , которое задается следующим соотношением:Xmcpi + q > 0.P1 ≡i6tУтверждение P1 остается справедливым и после получения сообщения процессом pi , номер i которого удовлетворяет неравенству i > t; следовательно, болееслабое утверждение P, которое определяется формулой P m ∧ (P0 ∨ P1), сохраняетсвою справедливость и в случае получения сообщения процессом p i , i > t.Уточненное таким образом условие P тем не менее позволяет процессу p 0обнаружить завершение базового вычисления по тем же самым признакам: приt = 0 утверждение P1 верно лишь при mcp0 + q > 0, а это означает, с учетомравенства mcp0 + q = 0 (проверку которого требуется провести для обнаружения завершения вычисления), что имеет место ¬P 1 .
Передача маркера, равно каки отправление базового сообщения, сохраняет предикат P 1 . К сожалению, условие P1 может быть опровергнуто при получении некоторого сообщения процессомpi , номер i которого удовлетворяет неравенству i 6 t. Как и в § 8.3.1, такую ситуацию можно исправить, снабдив каждый процесс окраской и введя следующееправило.Правило 2. Процесс-получатель окрашивается в цвет black.306Гл. 8.
Обнаружение завершенияvar statep : (active, passive) ;colorp: (white, black) ;mcp: integer init 0 ;Sp : { statep = active }begin send hmesi ;mcp := mcp + 1 (* Rule M *)endRp : { Сообщение hmesi доставлено процессу p }begin receive hmesi ; statep := active ;mcp := mcp − 1 ; (* Правило M *)colorp := black (* Правило 2 *)endIp : { statep = active }begin statep := passive endПриступить к обнаружению завершения вычисления,выполняется один раз процессом p0 :begin send htok, white, 0i to pN−1 endTp : (* Процесс p обрабатывает маркер htok, c, qi*){ statep = passive } (* Правило 1 *)begin if p = p0then if (c = white) ∧ (colorp = white) ∧ (mcp + q = 0)then Announceelse send htok, white, 0i to pN−1 (* Правило 4 *)else if (colorp = white) (* Правила 1 и 3 *)then send htok, c, q + mcp i to Nextpelse send htok, black, q + mcp i to Nextp ;colorp := white (* Правило 5 *)endАлгоритм 8.7.
Алгоритм СафрыПосле этого заменим прежнее условие P на новое, которое будет представленоформулой Pm ∧ (P0 ∨ P1 ∨ P2), гдеP2 ≡ ∃j (t > j > 0) : colorpj = black.Каждое получение сообщения, влекущее за собой опровержение утверждения P 1 ,делает истинным P2 , и поэтому ни одно базовое действие не приводит к опровержению утверждения P.
Поскольку верна импликация (P ∧ color p0 = white ∧ t == 0) =⇒ ¬P2 , новое утверждение оставляет возможность обнаружить завершение вычисления. Это можно сделать, проверив, окрашен ли процесс p 0 в цветwhite (будучи при этом пассивным), когда он обладает маркером.Ослабленный вариант утверждения P нельзя опровергнуть в результате выполнения базовых действий; но и его можно опровергнуть, если принять во внимание передачу маркера, например, когда процесс p t , передающий маркер, — этоединственный процесс цвета black. Спасти ситуацию может дальнейшее ослабление утверждения P.
Мы вновь будем полагать, что маркер также имеет окраску8.3. Решения на основе волновых алгоритмов307(white или black), а само утверждение P ослабим, приведя его к виду P m ∧ (P0 ∨P1 ∨P2 ∨P3),гдеP3 ≡ the token is black.При передаче маркера предикат P3 остается истинным, если процессы цветаblack передают маркер, также имеющий окраску black.Правило 3. Когда процесс цвета black передает маркер, маркер приобретаетокраску black.Поскольку верна импликация «маркер окрашен в цвет white» =⇒ ¬P3 ,процесс p0 тем не менее способен обнаружить завершение вычисления. Для этогонужно проверить, верно ли, что этот процесс получил маркер цвета white (будучипри этом пассивным и окрашенным в цвет white).Действительно, теперь можно убедиться, что утверждение P сохраняет справедливость при выполнении внутренних действий, обмене базовыми сообщениями и при передаче маркера.
Прохождение волны не приводит к успеху, еслипри возвращении маркера процессу p0 оказывается, что этот маркер окрашен вцвет black, p0 окрашен в цвет black или mcp0 + q 6= 0. Если одна волна быланеудачной, то нужно запустить новую.Правило 4. Когда прохождение волны заканчивается неудачно, процесс p 0запускает новую волну.Очередная волна, впрочем, может оказаться столь же неудачной, как и еепредшественница, если процесс цвета black не будет иметь возможности сменитьсвою окраску на white. И в самом деле, процессы, окрашенные в цвет black, припередаче маркера придают ему ту же окраску, вследствие чего новая волна такжепотерпит неудачу.Обратим внимание на то, что, переменив окраску на white, процесс p i неопровергнет тем самым утверждение P, если i > t, а само утверждение P всегда остается истинным, когда p0 запускает волну, передавая маркер процессуpN−1 .
Отсюда следует, что процессы при передаче маркера могут менять окраскус black на white, не нарушая истинности утверждения P.Правило 5. Сразу после передачи маркера всякий процесс окрашиваетсяв цвет white.При таком режиме перемены окраски можно гарантировать, что после завершения базового вычисления какая-нибудь волна рано или поздно окажетсяуспешной. Приведенные здесь рассуждения воплощены в алгоритме 8.7.Теорема 8.9. Алгоритм Сафры (алгоритм 8.7) является корректнымалгоритмом обнаружения завершения вычислений с асинхронным обменомсообщениями.Д о к а з а т е л ь с т в о. Рассматриваемый нами алгоритм устроен так, чтоего инвариантом является предикат P, который определяется формулой P m ∧ (P0 ∨P1 ∨P2 ∨PЧтобы обосновать достаточное условие корректности, следует заметить, чтоалгоритм обнаруживает завершение вычисления только тогда, когда выполняютсяравенства t = 0, statep0 = passive, colorp0 = white и mcp0 + q = 0.
Из этихравенств следует выполнимость условий ¬P3 , ¬P2 и ¬P1 , а это, в свою очередь,308Гл. 8. Обнаружение завершенияозначает, что выполняется условие Pm ∧ P0 . С учетом того, что statep0 = passiveи mcp0 + q = 0, последнее условие влечет за собой выполнимость предиката term.Чтобы обосновать необходимое условие корректности, заметим, что послезавершения базового вычисления счетчики сообщений будут иметь постоянныезначения и сумма их будет равна 0.
Волна, запущенная из такой конфигурации,завершится так, что будет соблюдено равенство mc p0 + q = 0 и при этом всепроцессы будут окрашены в цвет white. Следующая за ней волна непременнобудет успешной.В отличие от алгоритма Дейкстры—Фейджена—ван Гастерена, сложностьв наихудшем случае алгоритма Сафры не ограничена сверху; маркер может передаваться неограниченное число раз, пока все процессы будут пассивны, нокакое-то сообщение будет долгое время пребывать на этапе пересылки. Так жекак и в случае алгоритма Дейкстры—Фейджена—ван Гастерена, математическоеожидание сложности по числу сообщений составляет величину Θ (T + N) длябазового вычисления, имеющего сложность по времени, равную T.Алгоритм векторного подсчета. Маттерн в работе [141] предложил алгоритм, сравнимый по эффективности с алгоритмом Сафры, но требующий при этомотдельного счетчика сообщений для каждого процесса-адресата.
В процессе p вкачестве счетчика сообщений используется массив mc p [P] . Когда p отправляетсообщение процессу q, содержимое счетчика процесса p изменяется при помощи оператора mcp [q] := mcp [q] + 1, а когда p получает сообщение, содержимоесчетчика процесса p изменяется при помощи оператора mc p [p] := mcp [p] − 1.Вместе с маркером передается также и массив счетчиков, и, когда процесс pвладеет маркером, содержимое массива mcp передается с маркером, а сам счетчик сбрасывается в ~0 (массив, все компоненты которого равны 0). Завершениевычисления регистрируется, когда массив, переносимый маркером, становитсяравным ~0.Алгоритм векторного подсчета обладает некоторыми преимуществами по сравнению с алгоритмом Сафры, но у него есть и серьезные изъяны.
Одно из достоинств этого алгоритма состоит в том, что завершение вычисления обнаруживается быстрее, а именно спустя один тур после того, как завершится базовоевычисление. Другое положительное качество данного алгоритма состоит в том,что, пока вычисление не завершилось, продвижение маркера задерживается более часто, и это позволяет сократить число обменов контрольными сообщениямив ходе работы алгоритма. В алгоритме Сафры каждый пассивный процесс передает маркер; а вот в алгоритме векторного подсчета такой процесс не будетпроводить передачу маркера, если содержащаяся в маркере информация позволяет заключить, что какое-то сообщение находится на этапе пересылки и будетдоставлено процессу p.Главный недостаток алгоритма векторного подсчета состоит в том, что вместес маркером передается большой объем информации (если быть точным, то поодному целому числу для каждого из процессов), и все это передается в каждом контрольном сообщении.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
