Реферат: Распределенные алгоритмы

Действительно, 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 *)

       end

Rp: { Сообщение (mes) прибывает в p }

       begin receive (mes) ; statep := active ;

                 mcp := mcp - 1;   (*Правило M *)

                 colorp := black  (*Правило 2 *)

       end

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)

                                 then Announce

                                 else send (tok, white,0) to pN -1   (*Правило 4 *)

                    else if (colorp = white)  (*Правила I and 3 *)

                                 then send ( tok, c, q + mcp ) to Nextp

                                 else send ( tok, black, q + mcp ) to Nextp ;

                colorp := white  (*Правило 5 *)

       end

Алгоритм алгоритма 8.7 safra's.

Это измененное утверждение все еще позволяет обнаружить завершение процессу p0 при тех же самых условиях, потому что, если t = 0, P1 читает mcP0 + q > 0, таким образом если mcP0 + q = 0 (это уже требовалось для обнаружения), ØP1 сохраняется. Отправление маркера сохраняет P1, и тоже самое происходит при посылке основного сообщения. К сожалению, P1 может принималь значение ложь при получении сообщения процессом  pi с i £ t. Как и в Подразделе 8.3.1, эта ситуация исправляется  назначение цвета каждому процессу по следующему правилу:

Правило 2. Процесс получающий сообщение становится черным и P заменяется на Pm Ù (P0 Ú P1 Ú P2 ), где

P2 º  $ j (t ³ j ³ 0) : colorp = black.

При каждом получении соощения, при котором P1 принимает значение ложь, P2 принимает значение истинна, так что P не принимает значение ложь при любом основном действии. Так как (P Ù colorP0 = white Ù t = 0) Þ ØP2 , все еще возможно обнаружить завершение с новым утверждением, а именно, проверяя является ли p0 белым (и пассивным) когда он обрабатывает маркер.

Ослабление P было успешно предотвращает изменение значения Р после основных событий; но более слабое утверждение может принять значение ложь при отправлении маркера, а именно, если процесс t - единственный черный процесс и он посылает маркер. Ситуация исправляется дальнейшим ослаблением P. Маркеру также назначается цвет (белый или черный) , и P ослабляется до Pm Ù (P0 Ú P1 Ú P2 ÚP3),  где

P3   º маркер черный.

Отправление маркера сохраняет P3, если черные процессы отправляют черный маркер.

Правило 3. Когда черный процесс посылает маркер, маркер  становится черным.

Т.к. (маркер белый) Þ ØP3  завершение может все еще обнаруживаться процессом p0, а именно, проверкой получает ли он белый маркер (и белый ли он сам и пассивный).

Действительно, теперь можно быть уверенным, что внутренние действия, основные коммуникации и отправление маркеров сохраняют P. Волна заканчивается неудачно,  когда маркер возвращается в p0, если он черный, p0 черный, или mcP0 + q ¹ 0. Если волна заканчивается неудачно, должна быть начата новая волна.

Правило 4. Когда волна заканчивается неудачно, p0 начинает новую волну.

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

Страницы: 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, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105