Теормин, страница 5

Когда процесс p, не входящий в состав дерева, становится активным после получения сообщения от процесса q, вершина q становится родительской вершиной для процесса p.

Чтобы обозначить явно отправителя сообщения, всякое базовое сообщение <mes>, отправленное процессом q, будет обозначаться записью cmes_q.

Вершины из дерева T удаляются по двум причинам:

1. Базовое сообщение удаляется после его получения.

2. Чтобы контрольный алгоритм сработал, дерево должно исчезнуть после завершения базового алгоритма. Сообщения — листья дерева T; в каждом процессе есть переменная для подсчета числа вершин-последователей этого процесса в дереве T. Удаление из дерева вершины-последователя процесса p осуществляется в другом процессе q в результате того, что вершина-последователь

   1. либо соответствует сообщению, достигшему процесса q

   2. либо соответствует самому процессу q

Чтобы в процессе p не нарушался учет вершин-последователей, ему отправляется сигнальное сообщение sig_p при удалении вершины-последователя процесса p. Это сообщение замещает удаленную вершину-последователя процесса p, а удаление этой вершины из дерева осуществляется самим процессом p после получения указанного сигнала; при этом p уменьшает значение счетчика последователей на 1.

Теорема 1.

Алгоритм Дейкстры-Шолтена является корректным алгоритмом обнаружения завершения вычисления; в нем используется M обменов контрольными сообщениями.

(доказывается через инвариант)

Алгоритм Шави—Франчеза

Обобщает алгоритм Дейкстры-Шолтена для случая децентрализованных базовых вычислений.

В алгоритме Шави-Франчеза граф вычислений является лесом, каждое дерево которого имеет в качестве корня один из инициаторов базового вычисления.

Для обозначения дерева, корнем которого служит процесс p будем использовать запись T_p.

В алгоритме Шави-Франчеза строится такой граф F = (V_F, E_F), что

1. либо F пуст, либо F представляет собой лес, каждое дерево которого имеет один из инициаторов в качестве корня,

2. множество V_F содержит все активные процессы и все базовые сообщения, пребывающие на этапе пересылки.

Завершение базового вычисления будет обнаружено, когда указанный граф становится пустым.

Проверка того, что все деревья исчезли, проводится при помощи одной-единственной волны.

Лес F строится так, чтобы всякое дерево T_p, ставшее пустым, оставалось пустым и в дальнейшем. Это не препятствует процессу p вновь становиться активным, но если p становится активным после исчезновения его собственного дерева, то он заносится в дерево другого инициатора.

Каждый процесс принимает участие в распространении волны только тогда, когда его дерево исчезает; и если волна приводит к тому, что принимается решение, то вызывается процедура оповещения Announce.

Переменная sc_p используется для подсчета числа последователей вершины p в дереве T.

Булева переменная empty_p принимает значение true тогда и только тогда, когда дерево, в котором содержится вершина p становится пустым.

Примечания.

1. В приведенном описании волновой алгоритм в явном виде не выделен.

2. Волновой алгоритм запускают только инициаторы базовых вычислений

3. Все процессы проводят параллельное выполнение волнового алгоритма, причем отправление сообщений или принятие решения разрешается только тем процессам p, у которых переменная empty_p имеет значение true

4. При осуществлении события decide вызывается процедура Announce.

Теорема 2.

Алгоритм Шави-Франчеза является корректным алгоритмом обнаружения завершения вычисления; в нем используется M + W обменов контрольными сообщениями.

(доказывается через инвариант)

Алгоритм Сафры

Условия применения:

1. Базовый алгоритм децентрализованный.

2. Каналы связи однонаправленные.

3. В сети существует гамильтонов контур, по которому распространяются контрольные сообщения; базовые сообщения могут передаваться по любым каналам.

4. Контрольный алгоритм — централизованный волновой алгоритм в однонаправленном кольце.

Принцип работы:

1. Каждый процесс может иметь некоторый цвет, который задается переменной color; эта переменная может иметь одно из двух значений white или black.

2. Контрольные сообщения (маркеры) также окрашиваются в один из двух цветов white или black.

3. Маркер передается только пассивными процессами.

4. Инициализатор контрольного алгоритма запускает маркер цвета white

5. После приема базового сообщения процесс окрашивается в цвет black

6. Процесс цвета black окрашивает маркер в цвет black

7. После передачи маркера процесс окрашивается в цвет white

8. Если инициализатор принимает маркер цвета white, то он объявляет о завершении базового алгоритма.

9. Каждый процесс p снабжен счетчиком базовых сообщений mc_p, который увеличивается на 1 при отправлении процессом базового сообщения и уменьшается на 1 при приеме базового сообщения.

10. Маркер при прохождении через процессы суммирует показания их счетчиков.

11. Завершение работы базового алгоритма регистрируется, если сумма собранных маркером показаний счетчиков равна 0.

Теорема 3.

Алгоритм Сафры является корректным алгоритмом обнаружения завершения вычисления.

(доказывается через инвариант)

Алгоритм возвращения кредита

Условия применения:

Алгоритм обнаруживает завершение централизованного вычисления при условии, что каждый процесс способен отправить сообщение непосредственно самому инициатору вычисления (т. е., сеть содержит подграф, имеющий форму звезды, в центре которой расположен инициатор).

Принцип работы:

В этом алгоритме каждому сообщению и каждому процессу вручается некоторый кредит; его значением служит вещественное число, расположенное между 0 и 1 (включительно). Алгоритм стремится сохранить инвариантность следующих утверждений.

1. Суммарный кредит, выданный сообщениям и процессам, равен 1.

2. Всякому базовому сообщению вручается положительный кредит.

3. Всякому активному процессу вручается положительный кредит.

Процессы, имеющие положительный кредит и не подпадающие под перечисленные законы (т. е. пассивные процессы), возвращают кредит инициатору. Инициатор поступает подобно банку и собирает все кредиты, которые ему отправляют, в переменной ret (возвращённые кредита).

Когда инициатор владеет всеми кредитами, то он сообщает о завершении базового алгоритма.

Теорема 4.

Алгоритм возвращения кредита является корректным алгоритмом обнаружения завершения вычислений.

(доказательство через инвариант)

Алгоритм Раны

Для решения задачи обнаружения завершения вычисления можно использовать штемпели времени. Предполагается, что все процессы снабжены часами; для этой цели пригодны как аппаратные таймеры, так и логические часы Лампорта.

В основу алгоритма положен локальный предикат quiet(p), определенный для каждого процесса p так, что:

quiet(p)  state_p = passive && никакое базовое сообщение, отправленное p не пребывает на этапе пересылки,

откуда следует импликация (Для любого p quiet(p)) => term

Условие quiet определяется следующим соотношением: quiet(p) := (state_p = passive || unack_p = 0).

Цель алгоритма — проверить, верно ли, что в определенный момент времени t все процессы удовлетворяют условию quiet.

Процесс p, перейдя в состояние quiet, сохраняет в памяти тот момент времени qt_p, когда произошло это событие, и запускает волну, чтобы проверить, все ли процессы уже перешли в состояние quiet к моменту времени qt_p

Если это так, то завершение вычисления считается обнаруженным. В противном случае существует процесс, который перейдет в состояние quiet позже, и он запустит новую волну.

Теорема 5.

Алгоритм Раны является корректным алгоритмом обнаружения завершения вычислений.

(доказательство через инвариант)

1. Задача сохранения моментального состояния. Алгоритм Чанди-Лампорта Алгоритм Лаи-Янга. Применение алгоритмов сохранения моментального состояния.

Конфигурация системы — это набор конфигураций составляющих ее процессов плюс содержание каналов связи.

Необходимо уметь сохранять конфигурации согласованно.

Множество реализуемых конфигураций не является инвариантом отношения эквивалентности, и поэтому оно не определяется вычислением однозначно. Таким образом, мы будем считать разумным всякий результат работы алгоритма, если он приводит к построению какой-либо конфигурации, которая окажется возможной для заданного вычисления (т. е. может случится в некоторой реализации этого вычисления).

Для чего необходимо сохранение моментального состояния системы (snapshot)

1. Проверка свойств после в режиме offline над snapshot-ом

Свойство P конфигураций называется устойчивым, если справедливо соотношение P(Конф.1) && (Конф.1 -> Конф.2) => P(Конф.2)

1. Использование snapshot вместо начальных конфигураций.

2. Использование snapshot для отладки распределённой программы.

Допущение:

1. Слабая справедливость вычислений.

2. Сеть – сильно связна

Распределённая система C.

Множество процессов P.

Множество событий вычисления Ev.

На множестве событий процесса p вводится причинно-следственный порядок <<_p

Очевидным образом вводятся значения словосочетаний «моментальное локальное состояние процесса p», «предмоментальное событие», «постмоментальное событие».

Моментальное состояние системы состоит из

1. Моментальные состояния всех процессов

2. Моментальные состояния всех каналов (могут быть случаи, когда сообщение находится на этапе пересылки, а могут быть случаи, когда один из процессов уже зарегистрировал получение сообщения, а другой из процессов не зарегистрировал отправки этого сообщения)

Осуществимое моментальное состояние: если для всех пар соседних процессов p и q, rsvd_pq подмножество sent_pq

Сечением называется совокупность событий вычисления, замкнутая влево относительно отношения локальной причинно-следственной зависимости.

Сечение L2 считается более поздним, чем сечение L1, если верно включение L1 вложено в L2.

Сечение называется согласованным, если оно замкнуто влево относительно отношения причинно-следственной зависимости.

Моментальное состояние S* называется значимым в вычислении C, если существует такая реализация E ∈ C, что Y* является конфигурацией E.

Теорема 1.

Пусть S* — моментальное состояние системы и L — сечение, порожденное S*. Тогда равносильны следующие три утверждения:

1. S* осуществимо;

2. L согласовано;

3. S* значимо.

(доказывается 1 => 2 => 3 => 1)

Алгоритм Чанди-Лампорта

По теореме 1 достаточно скоординировать локальные моментальные состояния, чтобы выполнялись следующие два свойства:

1. выбранные в каждом процессе локальные моментальные состояния должны быть реализованы.

2. получение постмоментального сообщения не может составлять предмоментальное событие.

Сообщения самого вычисления – базовые сообщения.

Сообщения алгоритма построения моментального состояния – контрольные сообщения.

Допущения:

1. Сильно связная сеть

2. Каналы могут быть однонапавленными

3. Каналы сохраняют очерёдность собщений

Идея алгоритма:

В алгоритме Ченди—Лэмпорта процессы сообщают друг другу о построении моментальных состояний путем отправления специальных сообщений (маркеров) (mkr) по каждому каналу.

Каждый процесс, запечатлевая свое локальное состояние, отправляет маркер в точности один раз по каждому примыкающему к нему каналу; маркеры рассматриваются как контрольные сообщения.

Получение сообщения (mkr) каким-либо процессом, который еще не запечатлел свое моментальное состояние, приводит к тому, что этот процесс запечатлевает свое моментальное состояние и также отправляет маркер (mkr), который выполняется параллельно с вычислением C.

Лемма

Если хотя бы один процесс запустит алгоритм Чанди-Лампорта, то спустя конечный промежуток времени все процессы запечатлеют свое локальное моментальное состояние.