Введение в распределённые алгоритмы. Ж. Тель (2009) (не распознанно) (1185664), страница 82
Текст из файла (страница 82)
Этот недостаток может быть не столь серьезным,если число процессов невелико. Другой изъян состоит в том, что для этого ал-8.3. Решения на основе волновых алгоритмов309горитма требуется знание отличительных признаков всех остальных процессов.Если вектор представляется массивом, то каждый процесс должен быть заранееосведомлен о всем многообразии отличительных признаков процессов системы;но это требование может быть ослаблено, если вектор представляется в видемножества пар, каждая из которых состоит из отличительного признака и целогочисла. Первоначально каждый процесс должен знать отличительные признакисоседних процессов (чтобы правильно увеличивать показания счетчика), а всепрочие отличительные признаки будут изучены по ходу вычисления.var statep : (active, passive) ;colorp: (white, black) ;unackp : integer init 0 ;Sp : { statep = active }begin send hmesi ; unackp := unackp + 1 ; (* Правило A *)colorp := black (* Правило B *)endRp{: Сообщение hmesi от q доставлено процессу p }begin receive hmesi ; statep := active ;send hacki to q (* Правило A *)endIp : { statep = active }begin statep := passive endAp : {Подтверждение hacki доставлено процессу p }begin receive hacki ; unackp := unackp − 1 end (* Правило A *)Приступить к обнаружению завершения вычисления;исполняется один раз процессом p0 :begin send htok, whitei to pN−1 endTp : (* Процесс p владеет маркером htok, ci *){ statep = passive ∧ unackp = 0 }begin if p = p0then if c = white ∧ colorp = whitethen Announceelse send htok, whitei to pN−1else if (colorp = white)then send htok, ci to Nextpelse send htok, blacki to Nextp ;colorp := white (* Правило B *)endАлгоритм 8.8.
Обнаружение завершения вычисления с использованием подтверждений8.3.3. Использование подтвержденийВ алгоритме Сафры проводится подсчет отправленных и полученных базовыхсообщений, чтобы установить, что никакие базовые сообщения не пребываютна этапе пересылки. Это требование можно обеспечить, используя подтверждения; сразу несколько авторов предложили снабдить этим механизмом алгоритм310Гл. 8. Обнаружение завершенияДейкстры—Фейджена—ван Гастерена (см., например, работу [152]). Подобнуюмодификацию основного метода мы обсудим лишь вкратце, поскольку полученный в результате алгоритм ни в коей мере не улучшает алгоритм Шави —Франчезаи поэтому уже вышел из употребления.Прежде всего заметим, что утверждение «ни одно сообщение не пребываетна этапе пересылки» равносильно утверждению «для каждого процесса p ни одно сообщение, отправленное p, не пребывает на этапе пересылки».
На каждыйпроцесс возлагается ответственность за отправленные им сообщения, т. е. процесс должен предотвратить вызов процедуры Announce, до тех пор пока он неудостоверится, что все отправленные им базовые сообщения достигли адресата.В рассматриваемом методе обнаружения завершения вычисления для каждогопроцесса p локальное условие quiet(p) определяется так, чтобы выполняласьимпликацияquiet(p) =⇒ (statep = passive ∧ ни одно сообщение, отправленное процессом p,не пребывает на этапе пересылки).Тогда будет верно, что (∀p : quiet(p)) =⇒ term.Чтобы установить, что ни одно сообщение, отправленное процессом p, не пребывает на этапе пересылки, каждое сообщение сопровождается подтверждениеми каждый процесс ведет учет числа подтверждений, которые должны быть имполучены.
Точнее говоря, предикат Pa , который определяется соотношением∀p : (unackp =# (сообщения на этапе пересылки, отправленные процессом p)+ # (подтверждения на этапе пересылки, адресованные p)).должен быть инвариантом, что обеспечивается следующим правилом.Правило A. При отправлении сообщения процесс p увеличивает значениеunackp ; при получении сообщения от процесса q, процесс p отправляет процессуq подтверждение; при получении подтверждения процесс p уменьшает значениеunackp .Указанное выше требование для условия quiet (при выполнении условия quiet(p)процесс p является пассивным, и ни одно сообщение, отправленное процессом p,не пребывает на этапе пересылки) будет теперь соблюдено, если задать условиеquiet следующим соотношениемquiet(p) ≡ (statep = passive ∧ unackp = 0).Построение нашего алгоритма обнаружения завершения вычисления проводитсяпоэтапно, подобно тому как был построен алгоритм Дейкстры —Фейджена—ванГастерена. Вначале рассматривается предикат P 0 , который задается соотношениемP0 ≡ ∀i (N > i > t) : quiet(p).Предикат P1 нужно вводить осмотрительно, поскольку активизация процесса p jпроцессом pi в случае, когда j > t и i 6 t, не происходит совместно с событиемотправления сообщения процессом pi .
Однако если процесс pj активизирован8.3. Решения на основе волновых алгоритмов311(вследствие чего предикат P0 будет ложным), то соотношениемPb ≡ ∀p : (unackp > 0 =⇒ colorp = black),при помощи правила B, мы приходимPb ≡ ∀p : (unackp > 0 =⇒ colorp = black),при помощи правила B, мы приходим к заключению о том, что, как только предикат P0 становится ложным, будет выполнено условие P 1 , и поэтому утверждение(P0 ∨ P1) не будет опровергнуто.Правило B. После отправления сообщения всякий процесс окрашиваетсяв цвет black; всякий процесс имеет окраску white только когда для него выполняется условие quiet.В результате мы получим алгоритм 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 > 0) : colorpi = blackP2 ≡ маркер окрашен в цвет black.Теорема 8.10.
Алгоритм 8.8 является корректным алгоритмом обнаружения завершения вычислений с асинхронным обменом сообщениями.Д о к а з а т е л ь с т в о. Завершение вычисления объявляется в том случае,когда процесс p0 удовлетворяет условию quiet и владеет маркером, окрашеннымв цвет white. Отсюда следует, что условия P2 и P1 не выполняются, и, значит,верна формула Pa ∧ Pb ∧ P0 . Из этой формулы можно заключить, принимая во внимание условие quiet(p0), что все процессы также удовлетворяют условию quiet,и, следовательно, предикат term истинен.Когда завершается базовое вычисление, спустя некоторое время будут получены все подтверждения и все процессы будут удовлетворять условию quiet.Первая же волна, запущенная после того, как условие quiet будет выполнено длявсех процессов, завершится, окрасив все процессы в цвет white, и завершениебазового вычисления будет объявлено по окончании следующей волны.Решение, основанное на ограниченной задержке передачи сообщений.В [187, § 4.1.3] описан один подход к решению задачи обнаружения завершения вычисления (а также целого ряда других задач), в основу которого положено допущение о том, что задержка передачи сообщений ограничена некоторойконстантой (см.
также § 3.3.2). В таком случае всякий процесс остается возбужденным на протяжении интервала времени, длительность которого равна ,после отправления самого последнего сообщения, и при этом процесс остается окрашенным в цвет black, до тех пор пока он возбужден, подобно тому какэто было описано выше для решения задачи с использованием подтверждений.312Гл. 8. Обнаружение завершенияПроцесс p перестает быть возбужденным, если (1) самое последнее отправлениесообщения этот процесс осуществил не менее единиц времени тому назад, и (2)этот процесс является пассивным. Мы предоставляем читателю самостоятельнопровести полное формальное построение алгоритма.8.3.4.
Обнаружение завершения вычислений при помощиволнДо сих пор в этом параграфе мы обсуждали алгоритмы обнаружения завершения вычислений, в которых для передачи контрольных сообщений использовались кольцевые структуры; в основу этих алгоритмов были положены волновые алгоритмы для колец. Аналогичные решения были предложены и для другихтопологий. Так, например, Франчез и Роде в работе [88] , а также Топор в работе [193] разработали алгоритм, в котором для передачи контрольных сообщенийиспользуется остовное дерево. Тян и Ван Ливен (см [181]) построили децентрализованное решение для кольцевых сетей, древесных сетей, а также для сетейпроизвольной топологии.
Внимательное изучение этих решений показывает, чтовсе они очень похожи друг на друга, и отличие проявляется лишь в тех волновыхалгоритмах, на которых основываются эти решения.В данном параграфе мы приведем набросок общего метода построения алгоритма обнаружения завершения вычисления (вместе с его инвариантом), в основу которого положен произвольный, а не специальный (например, кольцевой)волновой алгоритм. Для каждой волны первое событие отправления процессомсообщения по ходу этой волны или принятия им решения мы будем называть посещением волной указанного процесса.
Предполагается, что в случае необходимости процесс может отложить посещение, пока не будут выполнены некоторыелокальные условия. Последующие события, связанные с прохождением той жесамой волны через указанный процесс уже никогда не откладываются.В этом параграфе мы проведем построение алгоритма только для случая синхронного обмена базовыми сообщениями, как это было осуществлено в § 8.3.1.Наше построение можно обобщить на случай асинхронного обмена сообщениями,подобно тому, как это было сделано в §§ 8.3.2 и 8.3.3.Инвариант нашего алгоритма должен позволять обнаруживать завершениевычисления, когда волна принимает решение. Поэтому в качестве первого приближения мы полагаем P = P0 , гдеP0 ≡ все посещенные процессы пассивны.Действительно, коль скоро к моменту принятия решения были посещены все процессы, это требование позволяет обнаружить завершение вычисления в том случае, когда волна принимает решение.
Но требование P 0 , кроме того, соблюдаетсяи в том случае, когда волна запускается (и ни один процесс еще не посещен).Условие P0 сохраняется в ходе работы волнового алгоритма, если принять вовнимание следующее правило.Правило 1. Волна посещает только пассивные процессы.8.3.
Решения на основе волновых алгоритмов313К сожалению, P0 будет опровергнуто, когда процесс, посещенный волной,активизируется другим процессом, который волна еще не посетила. Поэтомукаждый процесс снабжается окраской и требование P замещается ослабленнымусловием (P0 ∨ P1), гдеP1 ≡ имеется процесс цвета black, который еще не был посещен.Ослабленный инвариант сохраняется при выполнении следующего правила.Правило 2. Процесс, отправивший базовое сообщение, приобретает окраскуblack.Но даже и это условие может быть опровергнуто по ходу движения волны,если она посетила единственный ранее не посещенный процесс цвета black.