ref (664672), страница 10

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 10)

Нормирующие функции полагаются га математическое понятие обоснованных множеств. Это множество с порядком <, где нет бесконечных убывающих последовательностей.

Определение 2.15 Частичный порядок (W, <) является обоснованным, если в нем нет бесконечной убывающей последовательности

w₁ > w₂ > w₃ ... .

Примеры обоснованных множеств, которые будут использоваться в этой книге – это натуральные числа с обычным порядком, и n-кортежи натуральных чисел с лексикографическим порядком (см. раздел 4.3). Свойство, что обоснованное множество не имеет бесконечной убывающей последовательности, может использоваться, чтобы показать, что утверждение Р в конечном счете истина. К этому моменту должно быть показано, что существует функция f из C в обоснованное множество W такая, что в каждом переходе значение f убывает или Р становится истиной.

Определение 2.16 Пусть даны система переходов S и утверждение Р. Функция f из С в обоснованное множество W называется нормирующей функцией (по отношению к Р), если для каждого перехода    , f() > f() или Р().

Теорема 2.17 Пусть даны система переходов S и утверждение Р. Если S завершается правильно и нормирующая функция f (w.r.t Р) существует, то Р – истина в некоторой конфигурации каждого исполнения системы S.

Доказательство. Пусть Е = (₀, ₁, ₃, ...) – исполнение системы S. Если Е конечно, его последняя конфигурация является терминальной, и т.к. term  Р всегда истина в системе S, то Р выполняется в этой конфигурации. Если Е бесконечно, пусть E’ будет самым длинным префиксом Е, который не содержит конфигураций, в которых Р истина, и пусть s будет последовательностью (f(₀ ), f(₁), ...) для всех конфигураций _i, которые появляются в Е’. В зависимости от выбора Е’ и свойства f, s может быть убывающей последовательностью, и отсюда, по обоснованности W, s конечна. Это подразумевает также, что Е’ – конечный префикс (₀, ₁, ..., _k ) исполнения Е. В зависимости от выбора Е’, Р(_k+1) выполняется. 

Если приняты свойства справедливости, то можно заключить из более слабых посылок (чем в теореме 2.17), что Р в конце концов станет истиной. Значение нормирующей функции не должно уменьшаться при каждом переходе. Предположение справедливости может быть использовано, чтобы показать, что бесконечные исполнения содержат переходы определенного типа бесконечно часто. Затем будет достаточно показать, что f никогда не увеличивается, а уменьшается с каждым переходом этого типа.

В некоторых случаях мы будем использовать следующий результат, который есть специальный случай теоремы 2.17

Теорема 2.18 Если S завершается правильно и есть число К такое, что каждое исполнение содержит по крайней мере К переходов, то Р истина в некоторой конфигурации каждого исполнения.

Р
ис. 2.1 Пример пространственно-временной диаграммы

2.3 Каузальный порядок событий и логические часы

Взгляд на исполнения как последовательности переходов естественным образом порождает понятие времени в исполнениях. Говорят, что переход а появляется раньше перехода b, если a встречается в последовательности перед b. Для исполнения Е = (₀, ₁, ...) определим ассоциированную последовательность событий Е’=(е₀, е₁, ...), где е_i – это событие, при котором конфигурация изменяется из _i в _i+1. Заметьте, что каждое исполнение определяет уникальную последовательность событий этим путем. Исполнение может быть визуализировано в пространственно-временной диаграмме, рисунок 2.1, которой, представляет пример. В такой диаграмме, горизонтальная линия нарисована для каждого процесса, и каждое событие нарисовано точкой на линии процесса, где оно имеет место. Если сообщение m послано при событии s и получено при событии r, стрелка рисуется от s к r. Говорят, что события s и r соответственные в этом случае.

Как мы увидим в подразделе 2.3.1, события распределенного исполнения могут иногда быть взаимно обменены без воздействия на последующие конфигурации исполнения. Поэтому понятие времени как абсолютного порядка на событиях исполнения не приемлемо для распределенных исполнений, и вместо этого представляется понятие каузальной зависимости. Эквивалентность исполнений при переупорядочивании событий изучается в подразделе 2.3.2. Мы обсуждаем в подразделе 2.3.3 как могут быть определены часы для измерения каузальной зависимости (а не времени), и представляем логические часы Лампорта, важный пример таких часов.

2.3.1 Независимость и зависимость событий

Уже было замечено, что переходы распределенной системы влияют, и подвержены влиянию, только на часть конфигураций. Это ведет к тому наблюдению, что два последовательных события, влияя на разделенные части конфигурации, независимы и могут также появляться в обратном порядке. Для систем с асинхронной передачей сообщений, это выражается в следующей теореме.

Теорема 2.19 Пусть  будет конфигурацией распределенной системы (с асинхронной передачей сообщений) и пусть е_р и е_q будут событиями различных процессов р и q, применимых в . Тогда е_р применимо в е_q(), е_q применимо в е_р(), и е_р(е_q()) = е_q(е_р()).

Доказательство. Чтобы избежать анализа случаев, которые есть посылка, получение, или внутренние события, мы представим каждое событие однородной нотацией (с, х, у, d). Здесь с и d обозначают состояние процесса до и после события, х – набор сообщений, полученных во время события, и у – набор сообщений, посланных во течение события. Таким образом, внутренне событие (с, d) обозначается как (c,,,d), событие отправки (с, m, d) обозначается как (с, , {m}, d), и событие приема (с, m, d) – (c, {m}, , d). В этой нотации, событие е = (с, x, y, d) процесса p применимо в конфигурации  = (С_p1, ..., C_p, ..., С_рN, M), если с_р = с и x  M. В этом случае

е() = (С_p1, ..., d, ..., (M \ x)  у).

Теперь предположим е_р = (b_p, x_р, у_р, d_p) и е_q = (b_q, x_q, у_q, d_q) применимы в

• = (..., с_р, ..., с_q, ..., M),

то есть с_р = b_p, c_q = b_q, x_p  M, и x_q  M. Важное наблюдение состоит в том, что х_р и x_q разделены, сообщение в x_p (если есть такое) имеет назначением р, в то время как сообщение в х_q (если есть такое) имеет назначением q.

Запишем _р = е_р(), и запомним что

_р = (..., d_p, ..., c_q, ..., (M \ x_p )  у_р ).

Так как x_q  M и x_q  х_р = , следует, что х_q  (M \ x_p  у_р ), и отсюда е_q применимо в _р. Запишем _pq = e_q(_р), и запомним, что

_рq = (..., d_p, ..., d_q, ..., ((M \ x_p  у_р ) \ x_q )  у_q ).

С помощью симметричного аргумента может быть показано, что е_р применимо в _q = e_q(). Запишем _qp = e_p(_q), и запомним, что

_qp = (..., d_p, ..., d_q, ..., ((M \ x_q  у_q ) \ x_p )  у_p ).

Так как M – мультимножество сообщений, x_p  M, и x_q  M,

((M \ x_p  у_р ) \ х_q  у_q ) = ((M \ x_q  у_q ) \ x_p  у_р ),

и отсюда _pq = _qp . 

Пусть е_р и е_q будут двумя событиями, которые появляются последовательно в исполнении, т.е. исполнение содержит подпоследовательность

..., , е_р(), е_q(е_р()), ...

для некоторых . Посылка теоремы 2.19 применима к этим событиям за исключением следующих двух случаев.

1. p = q; или

2. е_р – событие отправки, и е_q - соответствующее событие получения.

В самом деле, теорема явно утверждает, что p и q должны быть различными, и если е_q получает сообщение, посланное в е_р, событие отправки не применимо в начальной конфигурации события e_p, как требуется. Таким образом, если одно из этих двух утверждений истина, события не могут появляться в обратном порядке, иначе они могут встречаться в обратном порядке и кроме того иметь результат в одной конфигурации. Запомните, что с глобальной точки зрения переходы не могут быть обменены, потому что (в нотации теоремы 2.19) переход из _р в _pq отличается от перехода из  в _q. Однако, с точки зрения процесса эти события неразличимы.

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

Определение 2.20 Пусть Е – исполнение. Отношение , называемое каузальным порядком, на событиях исполнения есть самое малое отношение, которое удовлетворяет

1. Если е и f – различные события одного процесса и е появляется перед f, то е  f.

2. Если s – событие отправки и r – соответствующее событие получения, то s  r.

3. Отношение  транзитивно.

Мы пишем а = b, чтобы обозначить (а  b  а = b). Так как = есть частичный порядок, могут существовать события а и b, для которых ни а = b ни b = а не выполняется. Говорят такие события конкурирующие, в нотации а || b. На рисунке 2.1, b || f, d || i, и т.д.

Каузальный порядок был впервые определен Лампортом [Lam78] и играет важную роль в рассуждениях, относящихся к распределенным алгоритмам. Определение  подразумевает существование каузальной цепочки между каузально связанными событиями. Этим мы подразумеваем, что а  b включает существование последовательности а = е₀ , е₁ , ..., е_к = b такой, что каждая пара последовательных событий в цепочке удовлетворяет либо (1), либо (2) в определении 2.20. Каузальная цепочка может быть даже выбрана так, что каждая пара, удовлетворяющая (1), есть последовательная пара событий в процессе, где они встречаются, т.е., нет событий между ними. На рисунке 2.1 каузальная цепочка между событием а и событием l есть последовательность а, f, g, h, j, k, l.

2.3.2 Эквивалентность исполнений: вычисления

В этом подразделе показывается, что события исполнения могут быть переупорядочены в любом порядке, согласующимся с каузальным порядком, без воздействия на результат исполнения. Это переупорядочивание событий вызывает другую последовательность конфигураций, но это исполнение будет рассматриваться как эквивалент исходного исполнения.

Пусть f = (f₀ , f₁ , f₂ ,...) будет последовательностью событий. Эта последовательность - последовательность событий относящихся к исполнению F = (₀, ₁, ₂, ...), если для каждого i, f_i применимо в _i и f_i (_i) = _i+1. В этом случае F называется включенным исполнением последовательности f. Мы хотели бы, чтобы F уникально определялась последовательностью f, но это не всегда так. Если для некоторого процесса p нет события в p, включенного в f, то состояние процесса p может быть произвольным начальным состоянием. Однако, если f содержит по крайней мере одно событие из р, то первое событие в р, скажем (с, х, у, d), определяет, что начальное состояние процесса р будет с. Поэтому, если f содержит по крайней мере одно событие в каждом процессе, ₀ уникально определено, и это определяет целое исполнение уникально.

Теперь пусть Е = (₀, ₁, ₂, ... ) будет исполнением с ассоциированной последовательностью событий Е’ = (е₀ , е₁ , е₂ , ...) и положим, что f –перестановка из Е’. Это означает, что существует перестановка  натуральных чисел (или множества {0, ..., k-1}, если Е – конечное исполнение с k событиями) таких, что f_i = е_(i). Перестановка (f₀ , f₁ , f₂ , ...) событий из Е согласующаяся с каузальным порядком, если f_i = f_j подразумевает i  j, т.е., если нет события, которому предшествует в последовательности событие, которому оно само каузально предшествует.

Теорема 2.21 Пусть f = (f₀ , f₁ , f₂ , ...) – перестановка событий из Е, которая согласуется с каузальным порядком исполнения Е. Тогда f определяет уникальное исполнение F, начинающееся в начальной конфигурации из Е. F имеет столько же событий сколько и Е, и если Е конечно, то последняя конфигурация из F такая же как и последняя конфигурация из Е.

Характеристики

Список файлов реферата