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

распознавание (процессами непосредственно) того, что распределенное

вычисление завершено. Эта проблема изучается в Главе 8. Нижняя граница

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

подробно. Глава включает некоторые классические алгоритмы (например.,

Dijkstra, Feijen, и Van Gasteren и Dijkstra и Scholten) и снова конструкция

дана для получения алгоритмов для этой проблемы из волновых алгоритмов.

Глава 9 изучает вычислительную мощность систем, где процессы не

различаются уникальными идентификаторами. Как показал Angluin, что в этом

случае много вычислений не могут быть выполнены детерминированным

алгоритмом. Глава представляет вероятностные алгоритмы, и мы исследуем

какие проблемы, могут быть решены этими алгоритмами.

Глава 10 объясняет, как процессы системы могут вычислять глобальное

"изображение", снимок состояния системы. Такой кадр полезен для определения

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

вычисление прогрессировало.

В Главе 11 эффект доступности понятия глобального времени будет

изучаться. Несколько степеней синхронизма будут определены, и будет

показано, что полностью асинхронные системы могут моделировать полностью

синхронные довольно тривиальными алгоритмами. Таким образом замечено, что

предположения относительно синхронизма не влияют на совокупность функций,

которые являются вычислимыми распределенной системой. Будет впоследствии

показываться, однако, что имеется влияние на сложность связи многих

проблем: чем лучше синхронизм сети, тем ниже сложность алгоритмов для этих

проблем.

Часть 3: Отказоустойчивость. В практических распределенных системах

возможность сбоя в компоненте не может игнорироваться, и следовательно

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

неудачу. Этот предмет будет обрабатываться в последней части книги;

короткое введение в предмет дано в Главе 12. Отказоустойчивость асинхронных

систем изучается в Главе 13. Результат Fischer и других обеспечен;

показывается, что детерминированные асинхронные алгоритмы не могут

справляться с даже очень скромным типом сбоя, аварийным отказом одиночного

процесса. Будет также показано, что с более слабыми типами неисправностей

можно иметь дело, и что некоторые задачи являются разрешимыми несмотря на

сбой типа аварийного отказа. Алгоритмы Bracha и Toueg будут обеспечены:

оказывается, напротив, рандомизированные асинхронные системы, способны

справиться с приемлемо большим количеством сбоев. Таким образом замечено,

что имеет место для надежных систем (см. Главу 9), рандомизированные

алгоритмы предлагают большее количество возможностей чем детерминированные

алгоритмы.

В Главе 14 отказоустойчивость синхронных алгоритмов будет изучаться.

Алгоритмы Lamport и другие показали, что детерминированные синхронные

алгоритмы могут допустить нетривиальные сбои. Таким образом замечено, что,

в отличие от случая надежных систем (см Главу 11), синхронные системы

предлагают большее количество возможностей чем асинхронные системы. Даже

большее число неисправностей может допускаться, если процессы способны

"подписаться" на связь к другим процессам. Следовательно, выполнение

синхронизма в ненадежной системе больше усложнено, чем в надежном случае. И

последний раздел Главы 14 будет посвящен этой проблеме.

Другой подход к надежности, а именно через само-стабилизацию

алгоритмов, сопровождается в Главе 15. Алгоритм стабилизируется, если,

независимо от начальной конфигурации, он сходится в конечном счете к

предназначенному поведению. Некоторая теория относительно стабилизации

алгоритмов будет разработана, и ряд алгоритмов стабилизации будет

обеспечен. Эти алгоритмы включают протоколы для нескольких алгоритмов графа

типа вычисления дерева поиска в глубину (как в Разделе 6.4) и вычисления

таблиц маршрутизации (как в Главе 4). Также, стабилизационные алгоритмы для

передачи данных (как в Главе 3) были предложены. Это может означать, что

все компьютерные сети могут быть выполнены, c использованием

стабилизационых алгоритмов.

Приложения. Приложение A объясняет нотацию, используемую в этой книге,

чтобы представить распределенные алгоритмы. Приложение В обеспечивает

некоторые фоновые основы из теории графов и терминологии графов. Книга

заканчивается списком ссылок и индексом терминов.

2 Модель

В изучении распределенных алгоритмов часто используется несколько

различных моделей распределенной обработки информации. Выбор определенной

модели обычно зависит того какая проблема распределенных вычислений

изучается и какой тип алгоритма или невозможность доказательства

представлена. В этой книге, хотя она и покрывает большой диапазон

распределенных алгоритмов и теории о них, сделана попытка работать с одной,

общей моделью, описанной в этой главе насколько это возможно.

Для того чтобы признать выводы невозможности (доказательство не

существования алгоритма для определенной задачи), модель должна быть очень

точной. Вывод невозможности это утверждение о всех возможных алгоритмах,

разрешенных в системе, отсюда модель должна быть достаточно точной, чтобы

описать релевантные свойства для всех допускаемых алгоритмов. Кроме того,

вычислительная модель это более чем детальное описание конкретной

компьютерной системы или языка программирования. Существует множество

различных компьютерных систем, и мы хотим, чтобы модель была применима к

классу схожих систем, имеющих общие основные свойства, которые делают их

«распределенными». И наконец, модель должна быть приемлемо компактной,

потому что хотелось бы, чтобы в доказательствах учитывались все аспекты

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

кратко релевантные аспекты класса компьютерных систем.

Распределенные вычисления обычно понимаются как набор дискретных

событий, где каждое событие это атомарное изменение в конфигурации

(состояния всей системы). В разделе 2.1 это понятие включено в определение

систем перехода, приводящих к понятию достижимых конфигураций и

конструктивному определению множества исполнений, порождаемых алгоритмом.

Что делает систему «распределенной»? То, что на каждый переход влияет, и он

в свою очередь оказывает влияние только на часть конфигурации, в основном

на локальное состояние одного процесса. (Или на локальные состояния

подмножества взаимодействующих процессов.)

Разделы 2.2 и 2.3 рассматривают следствия и свойства модели, описанной

в разделе 2.1. Раздел 2.2 имеет дело с вопросом о том, как могут быть

доказаны желаемые свойства данного распределенного алгоритма. В разделе 2.3

обсуждается очень важное понятие, а именно: каузальное отношение между

событиями в исполнении. Это отношение вызывает отношение эквивалентности,

определенное на исполнениях; вычисление это класс эквивалентности,

порожденный этим отношением. Определены часы, и представлены логические

часы как первый распределенный алгоритм, обсуждаемый в этой книге. И

наконец, в разделе 2.4 будут обсуждаться дальнейшие допущения и нотация, не

включенные в основную модель.

2.1 Системы перехода и алгоритмы

Система, чьи состояния изменяются дискретными шагами (переходами или

событиями) может быть обычно удобно описана с помощью понятия системы

переходов. В изучении распределенных алгоритмов это применимо к

распределенной системе как целиком, так и к индивидуальным процессам,

которые сотрудничают в рамках алгоритма. Поэтому системы перехода это очень

важное понятие в изучении распределенных алгоритмов и оно определяется в

подразделе 2.1.1.

В распределенных системах переходы влияют только на часть конфигурации

(системного глобального состояния). Каждая конфигурация сама по себе это

кортеж, и каждое состояние связано с некоторыми компонентами только из

этого кортежа. Компоненты конфигурации включают состояния каждого

индивидуального процесса. Для точного описания конфигураций должны

подразделяться различные виды распределенных систем, в зависимости от типа

коммуникаций между процессами.

Процессы в распределенной системе сообщаются либо с помощью доступа с

разделяемым переменным либо при помощи передачи сообщений. Мы примем более

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

процессы сообщаются при помощи обмена сообщениями. Распределенные системы,

где сообщение производится посредством разделяемых переменных, будут

обсуждаться в главе 15. Читатель, интересующийся сообщением посредством

разделяемых переменных, может проконсультироваться в поворотной статье

Дейкстры [Dij68] или Овицкий и Грайс [OG76].

Сообщения в распределенных системах могут передаваться либо синхронно,

либо асинхронно. Основной упор в этой книге делается на алгоритмы для

систем, где сообщения передаются асинхронно. Во многих случаях синхронная

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

передачи сообщений, как это было продемонстрировано Чаррон-Бост и др.

[CBMT92]. Подраздел 2.1.2 описывает модель асинхронной передачи сообщений

точно; в подразделе 2.1.3 модель адаптируется к системам, использующим

синхронную передачу сообщений. В подразделе 2.1.4 кратко обсуждается

справедливость.

2.1.1 Системы переходов

Система переходов состоит из множества всех возможных состояний

системы, переходов («ходов»), которые система совершает в этом множестве, и

подмножества состояний, в которых системе позволено стартовать. Чтобы

избежать беспорядка между состояниями отдельного процесса и состояниями

алгоритма целиком («глобальных состояний»), последние теперь будут

называться конфигурациями.

Определение 2.1 Система переходов есть тройка S = (C, (, I), где С это

множество конфигураций, ( это бинарное отношение перехода на C, и I это

подмножество С начальных конфигураций.

Отношение перехода это подмножество С х С. Вместо ((, () ( ( будет

использоваться более удобная нотация ( ( (.

Определение 2.2 Пусть S = (C, (, I) это система переходов. Исполнение S

это есть максимальная последовательность E = ((0, (1, (2,…), где (0 ( I, и

для всех i ( 0, (i ( (i+1.

Терминальная конфигурация это конфигурация (, для которой не существует

( такой, что ( ( (. Нужно помнить, что последовательность E = ((0, (1,

(2,…) с (i ( (i+1 для всех i максимальна, если она либо бесконечна, либо

заканчивается в терминальной конфигурации.

Определение 2.3 Конфигурация ( достижима из (, нотация ( ( (, если

существует последовательность ( = (0, (1, (2, …, (k = ( c (i ( (i+1 для

всех 0 ( i < k. Конфигурация ( достижима, если она достижима из начального

состояния.

2.1.2 Системы с асинхронной передачей сообщений

Распределенная система состоит из набора процессов и коммуникационной

подсистемы. Каждый процесс является системой переходов сам по себе с той

лишь оговоркой, что он может взаимодействовать с коммуникационной

подсистемой. Чтобы избежать путаницы между атрибутами распределенной

системы как целого и атрибутов индивидуальных процессов, мы используем

следующее соглашение. Термины «переход» и «конфигурация» используются для

атрибутов системы целиком, и (их эквиваленты) термины «событие» и

«состояние» используются для атрибутов процессов. Чтобы взаимодействовать с

коммуникационной системой процесс имеет не только обычные события

(упоминаемые как внутренние события), но также события отправки и события

получения, при которых сообщения воспроизводятся и потребляются. Пусть M

будет множеством возможных сообщений, и обозначим набор мультимножеств с

элементами из M через M(M).

Определение 2.4 Локальный алгоритм процесса есть пятерка (Z, I, (i, (s,

(r), где Z это множество состояний, I это подмножество Z начальных

состояний, (i это отношение на Z x Z, и (s и (r это отношения на Z x M x

Z. Бинарное отношение ( на Z определяется как

c ( d ( (c, d) ( (i ( (m ( M((c, m, d) ( (s ( (r ).

Отношения (i , (s , (r соответствуют переходам состояния, соотносящихся

с внутренними сообщениями, сообщениями отправки и сообщениями получения,

соответственно. Впоследствии мы будем обозначать процессы через p, q, r,

p1, p2 и т.д., и обозначать множество процессов системы P. Определение 2.4

служит как теоретическая модель для процессов; конечно, алгоритмы в этой

книге не описываются только перечислением их состояний и событий, но также

средствами удобного псевдокода (см. приложение А). Исполнения процесса есть

исполнения системы переходов (Z, (, I). Нас, однако, будут интересовать

исполнения системы целиком, и в таком исполнении исполнения процессов

координируются через коммуникационную систему. Чтобы описать координацию,

мы определим распределенную систему как систему переходов, где множество

конфигураций, отношение перехода, и начальные состояния строятся из

соответствующих компонентов процессов.

Определение 2.5 Распределенный алгоритм для набора P = {p1, …, pN}

процессов это набор локальных алгоритмов, одного для каждого процесса в P.

Поведение распределенного алгоритма описывается системой переходов, как

это объясняется далее. Конфигурация состоит из состояния каждого процесса и

набора сообщений в процессе передачи; переходы это события процессов,

которые влияют не только на состояние процесса, но также оказывают влияние

(или подвергаются таковому) на набор сообщений; начальные конфигурации это

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

сообщений пуст.

Определение 2.6 Система переходов, порожденная распределенным

алгоритмом для процессов p1, …, pN при асинхронной коммуникации, (где

локальный алгоритм для процесса pi это есть (Z, I, (i, (s, (r)), это S =

(C, (, I), где

(1) C = {(cP1, …, cPN, M) : ((p ( P : cp ( Zp) и M ( M(M)}.

(2) ( = ((p(P (p), где (p это переходы соответствующие изменениям

состояния процесса p; (Pi это множество пар

(cP1, …, cPi, …, cPN, M1), (cP1, …, c’Pi, …, cPN, M2),

для которых выполняется одно из следующих трех условий:

. (cPi , c’Pi ) ( (iPi и M1 = M2;

. для некоторого m ( M, (cPi , m, c’Pi ) ( (sPi и M2 = M1 ( {m};

. для некоторого m ( M, (cPi , m, c’Pi ) ( (rPi и M1 = M2 ( {m}.

(3) I = {(cP1, …, cPN, M) : ((p ( P : cp ( Ip) ( M = (}.

Исполнение распределенного алгоритма это исполнение его, породившее

систему переходов. События исполнения выполняются явно с помощью следующей

нотации. Пары (c, d) ( (ip называются (возможными) внутренними событиями

процесса p, и тройки в (sp и (rp называются событиями отправки и событиями

получения процесса.

. Внутреннее событие е заданное как е = (c, d) процесса p называется

применимым в конфигурации ( = (cP1, …, cP, …, cPN, M), если cp = c.

В этом случае, e(() определяется как конфигурация (cP1, …, d, …,

cPN, M).

. Событие отправки e, заданное как e = (c, m, d) процесса p называется

применимым в конфигурации ( = (cP1, …, cP, …, cPN, M), если cp = c.

В этом случае, e(() определяется как конфигурация (cP1, …, d, …,

cPN, M ( {m}).

. Событие получения e, заданное как e = (c, m, d) процесса p

называется применимым в конфигурации ( = (cP1, …, cP, …, cPN, M),

если cp = c и m ( M. В этом случае, e(() определяется как

конфигурация (cP1, …, d, …, cPN, M \ {m}).

Предполагается, что для каждого сообщения существует уникальный

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

назначением сообщения.

2.1.3 Системы с синхронной передачей сообщений

Говорят, что передача сообщений синхронная, если событие отправки и

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

отдельный переход системы. То есть, процессу не разрешается посылать

сообщение, если назначение сообщения не готово принять сообщение.

Следовательно, переходы системы делятся на два типа: одни соответствуют

изменениям внутренних состояний, другие соответствуют скомбинированным

коммуникационным событиям двух процессов.

Определение 2.7 Система переходов, порожденная распределенным

алгоритмом для процессов p1, …, pN при синхронной коммуникации, это S =

(C, (, I), где

(1) C = {(cP1, …, cPN) : (p ( P : cp ( Zp}.

(2) ( = ((p(P (p) ( ((p,q(P:p(q (pq), где

. (Pi это множество пар

(cP1, …, cPi, …, cPN), (cP1, …, c’Pi, …, cPN),

для которых (cPi , c’Pi ) ( (iPi ;

. (PiPj это множество пар

(…, cPi, …, cPj , …), (…, c’Pi, …, c’Pj , …),

для которых существует сообщение m ( M такое, что

(cPi , m, c’Pi ) ( (sPi и (cPj , m, c’Pj ) ( (rPj .

(3) I = {(cP1, …, cPN) : ((p ( P : cp ( Ip)}.

Некоторые распределенные системы допускают гибридные формы

коммуникации; процессы в них имеют коммуникационные примитивы для передачи

сообщений как в синхронном так и в асинхронном стиле. Имея две модели,

определенные выше, нетрудно разработать формальную модель для этого типа

распределенных систем. Конфигурации такой системы включают состояния

процессов и набор сообщений в процессе передачи (а именно, асинхронных

сообщений). Переходы включают все типы переходов представленных в

определениях 2.6 и 2.7.

Синхронизм и его влияние на алгоритмы. Уже было замечено, что во многих

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

случай асинхронной передачи сообщений. Набор исполнений ограничен в случае

синхронной передачи сообщений исполнениями, где за каждым событием отправки

немедленно следует соответствующее событие приема [CBMT92]. Мы поэтому

рассматриваем асинхронную передачу сообщений как более общую модель, и

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

Однако, нужно быть внимательным, когда алгоритм, разработанный для

асинхронной передачи сообщений исполняется в системе с синхронной передачей

сообщений. Пониженный недетерминизм в коммуникационной системе должен быть

сбалансирован повышенным недетерминизмом в процессах, в противном случае

результатом всего этого может стать тупик.

Мы проиллюстрируем это элементарным примером, в котором два процесса

посылают друг другу некоторую информацию. В асинхронном случае, каждый

процесс может сначала послать сообщение и впоследствии получает сообщение

от другого процесса. Сообщения временно накапливаются в коммуникационной

подсистеме между их отправкой и посылкой. В синхронном случае, такого

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

сообщения перед тем как они могут получить сообщение, то никакой передачи

вообще не будет. В синхронном случае, один из процессов должен получить

сообщение перед тем как другой процесс отправит свое собственное сообщение.

Нет нужды говорить, что, если оба процесса должны получить сообщение перед

отправкой их собственных сообщений, опять же не будет никакой передачи.

Обмен двумя сообщениями будет иметь место в синхронном случае, только

если одно из двух нижеследующих условий выполняется.

1) Заранее определено, какой из двух процессов будет отправлять первым,

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

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

различных локальных алгоритмов в процессах.

2) Процессы имеют право недетерминированного выбора либо отправлять

сначала, потом принимать, либо получать сначала, потом – посылать. В

каждом исполнении один из возможных порядков исполнения будет выбран

для каждого процесса, т.е. симметрия нарушается коммуникационной

системой.

Когда мы представляем алгоритм для асинхронной передачи сообщений и

утверждаем, что алгоритм может также использоваться при синхронной передаче

сообщений, добавление этого недетерминизма, который всегда возможен,

предполагается неявно.

2.1.4 Справедливость

В некоторых случаях необходимо ограничить поведение системы так

называемыми справедливыми исполнениями. Условия справедливости вводят

исполнения, где события всегда (или бесконечно часто) применимы, но никогда

не встречаются как переход (потому что исполнение продолжается с помощью

других применимых событий).

Определение 2.8 Исполнение справедливо в слабом смысле, если нет

события применимого в бесконечно многих последовательных конфигурациях без

появления в исполнении. Исполнение справедливо в сильном смысле, если нет

события применимого в бесконечно многих конфигурациях без появления в

исполнении.

Возможно включить условия справедливости в формальную модель явно, как

это сделано Манна и Пнули [MP88]. Большинство алгоритмов, с которыми мы

имеем дело в этой книге, не полагаются на эти условия; поэтому мы решили не

включать их в модель, а устанавливать эти условия явно, когда они

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

спор, приемлемо ли включать предположение справедливости в модели

распределенных систем. Было выдвинуто утверждение, что предположение

справедливости не должны производиться, более того алгоритмы не должны

разрабатываться с учетом этих предположений. Дискуссия по некоторым

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

найдена в [Fra86].

2.2 Доказательство свойств систем перехода

Рассматривая распределенный алгоритм для некоторой проблемы, необходимо

продемонстрировать, что алгоритм есть корректное решение этой проблемы.

Проблема указывает, какие свойства требуемый алгоритм должен иметь; должно

быть показано, что решение обладает этими свойства. Вопрос проверки

распределенных алгоритмов получил значительное внимание и есть большое

количество статей, обсуждающих формальные методы проверки; см. [CM88,

Fra86, Kel76, MP88]. В этом разделе обсуждаются некоторые простые, но часто

используемые методы для демонстрации правильности распределенных

алгоритмов. Эти методы полагаются только на определение системы переходов.

Многие из требуемых свойств распределенных алгоритмов попадают в один

из двух типов: требования безопасности и требования живости. Требования

безопасности накладывают ограничение, что определенное свойство должно

выполняться для каждого исполнения системы в каждой конфигурации,

достигаемой в этом исполнении. Требования живости определяют, что

определенное свойство должно выполняться для каждого исполнения системы в

некоторых конфигурациях, достигаемых в этом исполнении. Эти требования

могут также встречаться в ослабленной форме, например, они могут

удовлетворяться с некоторой фиксированной вероятностью над множеством

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

ограничения, которые основываются только на использовании некоторого

данного знания (см. подраздел 2.4.4), что они гибки по отношен ию к

нарушениям в некоторых процессах (см. часть 3), что процессы равны (см.

главу 9), и т.д.

Методы проверки, описанные в этом разделе, базируются на истинности

утверждений в конфигурациях, достигаемых в исполнении. Такие методы

называются методами проверки утверждений. Утверждение это унарное отношение

на множестве конфигураций, то есть, предикат, который принимает значение

истина на одном подмножестве конфигураций и ложь – на другом.

2.2.1 Свойства безопасности

Свойство безопасности алгоритма это свойство в форме «Утверждение P

истина в каждой конфигурации каждого исполнения алгоритма». Неформально это

формулируется как «Утверждение Р всегда истина». Основной метод для того,

чтобы показать, что утверждение Р всегда истина, это продемонстрировать,

что Р инвариант согласно следующим определениям. Нотация P((), где ( это

конфигурация, есть булево выражение, чье значение истина, если Р

выполняется в (, и ложь в противном случае.

Определения зависят от данной системы переходов S = (C, (, I). Далее,

мы будем писать {P} ( {Q}, чтобы обозначить, что для каждого перехода ( ( (

(системы S), если Р(() то Q((). Таким образом {P} ( {Q} означает, что, если

Р выполняется перед любым переходом, то Q выполняется после этого перехода.

Определение 2.9 Утверждение Р инвариант системы S, если

1) для всех ( ( I, и

2) {P} ( {P}.

Определение говорит, что инвариант выполняется в каждой начальной

конфигурации, и сохраняется при каждом переходе. Из этого следует, что он

сохраняется в каждой достигаемой конфигурации, как и формулируется в

следующем теореме.

Теорема 2.10 Если Р это инвариант системы S, то Р выполняется для

каждой конфигурации каждого исполнения системы S.

Доказательство. Пусть Е = ((0, (1, (2, ...) исполнение системы S. Будет

показано по индукции, что Р((i) выполняется для каждого i. Во-первых, Р((0)

выполняется, потому что (0 ( I и по первому предложению определения 2.9. Во-

вторых, предположим P((i ) выполняется и (i ( (i+1 есть переход, который

встречается в E. По второму предложению определения 2.9 P((i+1)

выполняется, что и завершает доказательство. (

И наоборот, утверждение, которое выполняется в каждой конфигурации

каждого исполнения, есть инвариант (см. упражнение 2.2). Отсюда не каждое

свойство безопасности может быть доказано применением теоремы 2.10. В этом

случае, однако, каждое утверждение, которое всегда истинно, включено в

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

утверждение всегда истинно. (Нужно помнить, однако, что часто очень трудно

найти подходящий инвариант Q, к которому можно применить теорему.)

Теорема 2.11 Пусть Q будет инвариантом системы S и положим Q ( P (для

каждого ( ( С). Тогда Р выполняется в каждой конфигурации каждого

исполнения системы S.

Доказательство. По теореме 2.10, Q выполняется в каждой конфигурации, и

так как Q включает P, то P выполняется в каждой конфигурации также. (

Иногда полезно доказать сначала слабый инвариант, и впоследствии

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

сделать инвариант более сильным демонстрируется в следующем определении и

теореме.

Определение 2.12 Пусть S будет системой переходов и P, Q будут

утверждениями. Р называется Q-производным, если

1) для всех ( ( I, Q(() ( Р((); и

2) {Q ( Р} ( {Q ( Р}.

Теорема 2.13 Если Q есть инвариант и Р – Q-производное, то Q ( P есть

инвариант.

Доказательство. Согласно определению 2.9, должно быть показано, что

1) для всех ( ( I, Q(() ( Р((); и

2) {Q ( Р} ( {Q ( Р}.

Т.к. Q это инвариант, Q(() выполняется для всех ( ( I, и т.к. для всех

( ( I, Q(() ( Р((), P(() выполняется для всех ( ( I. Следовательно, Q(() (

P(() выполняется для всех ( ( I.

Предположим ( ( ( и Q(() ( Р((). Т.к. Q это инвариант, Q(()

выполняется, и т.к. {Q ( P} ( {Q ( Р}, Q(() ( Р((), откуда Р(() вытекает.

Следовательно, Q(() ( Р(() выполняется. (

Примеры доказательства безопасности, основывающиеся на материале

данного раздела, представлены в разделе 3.1.

2.2.2 Свойства живости

Свойство живости алгоритма это свойство в форме «Утверждение Р истина в

некоторой конфигурации каждого исполнения алгоритма». Неформально это

формулируется как «Утверждение Р в конечном счете истина». Основные методы,

используемые, чтобы показать, что Р в конце концов истина – это нормирующие

функции и беступиковость (или правильное завершение). Более простой метод

может быть использован для алгоритмов, в которых разрешаются только

исполнения с фиксированной, конечной длиной.

Пусть S будет системой переходов и Р – предикат. Определим term как

предикат, который истина во всех терминальных конфигурациях и ложь во всех

нетерминальных конфигурациях. Мы сначала предположим ситуации, где

исполнение достигает терминальной конфигурации. Обычно нежелательно, чтобы

такая конфигурация достигалась, в то время, как «цель» Р не была

достигнута. Говорят, что в этом случае имеет место тупик. С другой стороны,

завершение позволено, если цель была достигнута, в этом случае говорят о

правильном завершении.

Определение 2.14 Система S завершается правильно (или без тупиков),

если предикат (term ( Р) всегда истинен в системе S.

Нормирующие функции полагаются га математическое понятие обоснованных

множеств. Это множество с порядком w2 > w3 ... .

Примеры обоснованных множеств, которые будут использоваться в этой

книге – это натуральные числа с обычным порядком, и n-кортежи натуральных

чисел с лексикографическим порядком (см. раздел 4.3). Свойство, что

обоснованное множество не имеет бесконечной убывающей последовательности,

может использоваться, чтобы показать, что утверждение Р в конечном счете

истина. К этому моменту должно быть показано, что существует функция f из

C в обоснованное множество W такая, что в каждом переходе значение f

убывает или Р становится истиной.

Определение 2.16 Пусть даны система переходов S и утверждение Р.

Функция f из С в обоснованное множество W называется нормирующей функцией

(по отношению к Р), если для каждого перехода ( ( ( , f(() > f(() или

Р(().

Теорема 2.17 Пусть даны система переходов S и утверждение Р. Если S

завершается правильно и нормирующая функция f (w.r.t Р) существует, то Р –

истина в некоторой конфигурации каждого исполнения системы S.

Доказательство. Пусть Е = ((0, (1, (3, ...) – исполнение системы S.

Если Е конечно, его последняя конфигурация является терминальной, и т.к.

term ( Р всегда истина в системе S, то Р выполняется в этой конфигурации.

Если Е бесконечно, пусть E’ будет самым длинным префиксом Е, который не

содержит конфигураций, в которых Р истина, и пусть s будет

последовательностью (f((0 ), f((1), ...) для всех конфигураций (i, которые

появляются в Е’. В зависимости от выбора Е’ и свойства f, s может быть

убывающей последовательностью, и отсюда, по обоснованности W, s конечна.

Это подразумевает также, что Е’ – конечный префикс ((0, (1, ..., (k )

исполнения Е. В зависимости от выбора Е’, Р((k+1) выполняется. (

Если приняты свойства справедливости, то можно заключить из более

слабых посылок (чем в теореме 2.17), что Р в конце концов станет истиной.

Значение нормирующей функции не должно уменьшаться при каждом переходе.

Предположение справедливости может быть использовано, чтобы показать, что

бесконечные исполнения содержат переходы определенного типа бесконечно

часто. Затем будет достаточно показать, что f никогда не увеличивается, а

уменьшается с каждым переходом этого типа.

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

есть специальный случай теоремы 2.17

Теорема 2.18 Если S завершается правильно и есть число К такое, что

каждое исполнение содержит по крайней мере К переходов, то Р истина в

некоторой конфигурации каждого исполнения.

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

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

Взгляд на исполнения как последовательности переходов естественным

образом порождает понятие времени в исполнениях. Говорят, что переход а

появляется раньше перехода b, если a встречается в последовательности перед

b. Для исполнения Е = ((0, (1, ...) определим ассоциированную

последовательность событий Е’=(е0, е1, ...), где е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, ..., Cp, ..., СрN, M), если ср = с и x ( M. В этом случае

е(() = (Сp1, ..., d, ..., (M \ x) ( у).

Теперь предположим ер = (bp, xр, ур, dp) и еq = (bq, xq, уq, dq)

применимы в

. = (..., ср, ..., сq, ..., M),

то есть ср = bp, cq = bq, xp ( M, и xq ( M. Важное наблюдение состоит в

том, что хр и xq разделены, сообщение в xp (если есть такое) имеет

назначением р, в то время как сообщение в хq (если есть такое) имеет

назначением q.

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

(р = (..., dp, ..., cq, ..., (M \ xp ) ( ур ).

Так как xq ( M и xq ( хр = (, следует, что хq ( (M \ xp ( ур ), и

Страницы: 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18