else send ( tok, black ) to Nextp ;
colorp := white (*Правило 5 *)
end
Алгоритм 8.6 dukstra-feuen-van gasteren алгоритм.
Теорема 8.8 Dijkstra-Feijen- Фургон Gasteren алгоритм (Алгоритм 8.6) - правильный алгоритм обнаружения завершения для основных вычислений, использующих синхронное прохождение сообщений.
Доказательство. Предикат P º (P0 Ú P1 Ú P2 ) и алгоритм были разработаны таким образом, что P является инвариантом алгоритма. Завершение считается обнаруженным когда пассивный, белый p0 обрабатывает белый маркер. Действительно, при этом из цвета маркера следует, что ØP2 ,из цвета процесса p0 и из t = 0 следует ØP1 , а из P0 и состояния p0 следует term. Следовательно алгоритм безопасен.
Чтобы доказать живость, предположим, что основное вычисление закончилось. После этого, все процессы отправляют маркеры без задержки, сразу после того, как их получают. Когда маркер заканчивает первый полный обход, начатый после завершения, все процессы окрашены в белый цвет и после того, как маркер заканчивает следующий обход, обнаруживается завершение. o
Теперь мы попытаемся оценить число управляющих сообщений, используемых алгоритмом. Основное вычисление, используемое в доказательстве Теоремы 8.2 заставляет алгоритм использовать по крайней мере один обход маркера для каждых двух основных сообщений; следовательно сложность алгоритма в худшем случае - ½ N.M управляющих сообщений; см. Упражнение 8.5.
Алгоритм может использовать значительно меньшее количество сообщений в "среднем" основном вычислении. Предположим, что основное вычисление имеет сложность по времени T. Т.к. маркер всегда отправляется последовательно, не неблагоразумно предположить, что маркер отправляется приблизительно T раз прежде, чем заканчивается основное вычисление. (Даже эта оценка может быть слишком пессимистичной, т.к. отправление маркеров приостановлено в активных процессах.) Т.к. маркер отправляется менее чем 3N раза после завершения, алгоритм в этом случае использует T + 3N управляющих сообщений. Сложность основного вычисления - по крайней мере T (а именно, сложность по времени), но если вычисление содержит достаточный параллелизм, сложность сообщения может достигать Ω(N.T ).Если параллелизм позволяет каждому процессу посылать постоянное число сообщений в единицу времени, сложность по сообщениям основного вычисления - N.T.a, то есть Ω(N.T ) . Число управляющих сообщений, который является 0 (N + T), тогда намного лучше чем можно ожидать от сложности обнаружения завершения в худшем случае.
8.3.2 Подсчет Основных Сообщений: Алгоритм Сафра
Синхронность прохождения сообщений, принятая для основного вычисления в алгоритме Dijkstra-Feijen-Van Gasteren - серьезное ограничение для его общего применения. Несколько авторов обобщили этот алгоритм для вычислений с асинхронным прохождением сообщений (cf. Алгоритм 8.1). В данном подразделе будет обсуждено решение Сафра [Dij87]; в нем сложность в среднем случае сопоставима с сложностью алгоритма Dijkstra-Feijen-Van Gasteren.
Определим для каждой конфигурации число сообщений находящихсы в процессе передачи как B. Тогда term эквивалентен
("p : statep = passive) Ù B = 0.
Снова инвариант P будет составлен так, что завершение можно будет определить из P, t = 0, и другой информации из p0. Инвариант должен сохраняться, когда p0 начинает волну, то есть, когда t = N - 1.
Чтобы информация о B была доступна в процессах (распределенным способом), процесс p снабжается счетчеком сообщений mcp , и процессы поддерживают Pm как инвариант, где
Pm º B= SpÎP mcp .
Инвариант Pm получен, когда первоначально mcp = 0 для каждого p, и процессы подчиняются следующему правилу.
Правило М. Когда процесс p посылает сообщение, счетчик сообщений увеличивается на 1; когда процесс p получает сообщение, счетчик сообщений уменьшается на 1.
Инвариант должен позволять p0 решать,что содержит term, когда он получает маркер (t = 0). Т.к. term теперь также включает ограничение на значение B, маркер будет использоваться для передачи целого числа q для вычисления суммы счетчиков сообщений процессов, которые его отправили. Попробуем установить P = Pm Ù P0 , где
P0 º ("i (N > i > t) : statePi = passive) Ù ( q = SN>i>t mcPi ) .
Действительно, P0 истинен, когда t = N -1 и q = 0, и если t = 0 тогда из P следует, что
("i > 0 : statePi = passive) Ù (mcP0+ q = B),
так что p0 может определить завершение если state P0 = passive и mcP0 + q = 0.
Утверждение P0 устанавливается, когда p0 начинает волну, посылая маркер в pN -1 с q = 0. Отправление маркера сохраняет P0, только если отправляют маркер пассивные процессы и добавляют значение их счетчека сообщений; поэтому мы принимаем следующее правило.
Правило 1. Процесс обрабатывает маркер только когда он пассивен, и когда процесс посылает маркер он прибавляет значение своего счетчика сообщений к q.
При этом, P сохраняется при отправлении маркера и также при внутренних действиях; к сожалению, P не сохраняется при получении сообщения процессом p, с i > t. При получении сообщения P0 принимает значение ложь, то есть, это применимо только когда B> 0. Т.к. Почтовый сохраняется перед тем как принимает значение ложь,сохраняется P1, где
P1 º (Si £ t mcPi + q )>0.
Утверждение P1 остается истинным при получении сообщения процессом pi с i > t ; следовательно, более слабое утверждение P, определенное как Pm Ù (P0 Ú P1) сохраняется при получениисообщения процессом pi с i > t.
var statep : {active, passive) ;
colorp : (white, black) ;
mcp : integer init 0 ;
Sp: { statep = active }
begin send ( mes ) ;
mcp := mcp + 1 (* Правило M *)
Rp: { Сообщение (mes) прибывает в p }
begin receive (mes) ; statep := active ;
mcp := mcp - 1; (*Правило M *)
colorp := black (*Правило 2 *)
Ip: { statep = active }
begin statep := passive end
Начало определения, выполняется один раз процессом p0:
begin send (tok, white, 0) to pN - 1 end
Tp: (* Процесс p обрабатывает маркер (tok,c,q ) *)
{ statep = passive } (*Правило I *)
begin if p = p0
then if (c = white) Ù (colorp = white) Ù(mcp + q = 0)
Страницы: 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90
