Введение в распределённые алгоритмы. Ж. Тель (2009) (1185665), страница 18
Текст из файла (страница 18)
В соответствии с этим переходы в системе разделяются надва типа: переходы первого типа связаны с изменением внутренних состоянийпроцесса, а переходы второго типа связаны с комбинированным осуществлениемсобытий отправления-приема сообщения двумя процессами.2.1. Системы переходов и алгоритмы59Определение 2.7. Пусть задано семейство процессов р\, . .. , pN.
Тогда будем говорить, что система переходов S = (С, — Т) порождена распределенным алгоритмом для семейства процессов р\, ...,р ы при их синхроннойвзаимосвязи, если выполнены соотношения:1) С = {(cPi, . . . , cPN) : Ур е Р : ср Е Zp}',2) —>•= (Upep —>р) U (Up><76p:p^q —>pq), где• ~^Pi представляет собой множество пар(Cpi, . . .
, cPi, . .. , cPN), . . . , (cPl, . .. , cpi, . . . , cPN),для которых справедливо включение (cPi, ср.)е \~1р.',• —представляет собой множество пар(• • • >сРп ■■■, cPj, ...),cpi, . . . , Ср., . . .),для которых существует такое сообщение т € М , что имеют местовключения(cPi, т, c'Pi)e НР1 и (сР1, т, c'Pj)e Нр 3) X = {(сPl, . .. , cPN) (Vр € Р : Ср € /р)}•В некоторых распределенных системах допускается смешанная форма взаимосвязи; процессы в таких системах имеют примитивы для совершения обменовсообщениями как в синхронном, так и в асинхронном режиме.
Располагая темидвумя моделями, которые были определены выше, нетрудно построить модельи для этого типа распределенных систем. Конфигурации для таких систем определяются состояниями процессов и совокупностью сообщений, пребывающих наэтапе (асинхронной) пересылки. Переходы системы включают в себя все типыпереходов, представленные в определениях 2.6 и 2.7.Синхронизация и ее влияние на алгоритмы.
Как уже было отмечено, прирешении многих задач синхронный обмен сообщениями можно рассматриватькак особый случай асинхронного обмена сообщениями. Множество выполненийв случае синхроного обмена сообщениями ограничивается лишь теми выполнениями, в которых за событием отправления сообщения непосредственно следуетсоответствующее ему событие приема сообщения (см. [48]). Поэтому мы считаем асинхронный обмен сообщениями более общим видом модели, нежели синхронный обмен сообщениями, и в дальнейшем мы будем заниматься разработкойалгоритмов преимущественно для этого более общего случая.Тем не менее, нужно проявить определенную аккуратность, если алгоритм,разработанный в расчете на асинхронный обмен сообщениями, выполняется в системе с синхронным обменом сообщениями.
Сокращение недетерминизма в коммуникационной подсистеме должно быть уравновешено возрастанием недетерминизма в процессах системы, ибо в противном случае это может привести квозникновению взаимной блокировки.В качестве иллюстрации мы рассмотрим простой пример, в котором два процесса посылают друг другу некоторую информацию. В асинхронном случае каждый процесс может вначале отправить сообщение, а затем получить сообщение60Гл. 2.
Модельот другого процесса. На отрезке времени между отправлением и получением сообщения коммуникационная подсистема выступает в роли буфера, в который поступают сообщения. В синхронном случае такая буферизация невозможна, и еслиоба процесса должны отправить свои сообщения, прежде чем они приступят ких приему, никаких переходов не может произойти.
В синхронном случае один изпроцессов обязан принять сообщение от другого процесса, перед тем как отправить свое сообщение. Очевидно, что если оба процесса должны провести приемсообщения прежде, чем отправить свои собственные сообщения, то никаких переходов произойти не может.Обмен двумя сообщениями в синхронных системах может совершиться только в том случае, если выполнено одно из следующих двух условий.1. Заранее определено, который из двух процессов будет отправлять сообщение первым и который из них будет вначале заниматься приемом сообщения.Предопределить такой выбор заранее во многих случаях бывает невозможно,поскольку для этого требуется, чтобы эти два процесса выполняли разные локальные алгоритмы.2. Процессам предоставлена возможность недетерминированного выбора: либо вначале отправить сообщение, а затем заняться приемом сообщения, либовначале совершить прием сообщения, а уже затем приступить к отправлениюсообщения.
При каждом выполнении коммуникационной подсистемой будет выбран один из возможных порядков действия для каждого процесса, т. е. симметрия будет нарушена коммуникационной подсистемой.Когда мы даем описание какого-либо алгоритма, рассчитанного на асинхронныйобмен сообщениями, и утверждаем, что этот алгоритм может быть использовани в системах с синхронным обменом сообщениями, мы тем самым неявно предполагаем, что для этого в алгоритме нужно ввести указанный недетерминизм, и этовсегда возможно.2.1.4. СправедливостьИногда при исследовании поведения систем возникает необходимость ограничиться рассмотрением только так называемых справедливых выполнений.
Условия справедливости позволяют исключить из рассмотрения такие выполнения,в которых некоторые события оказываются допустимыми всегда (или бесконечночасто), но при этом ни разу не осуществляются в виде переходов (из-за того чтовыполнение продолжается всякий раз за счет осуществления других событий).Определение 2.8. Выполнение считается слабо справедливым, если никакое событие не может оказаться допустимым в каждой из бесконечного числаподряд идущих конфигураций, не осуществившись при этом ни разу в этом выполнении. Выполнение считается сильно справедливым, если никакое событие,не может оказаться допустимым в бесконечном множестве конфигураций, не осуществившись при этом ни разу в этом выполнении0 Приведенное здесь определение слабой и сильной справедливости не является достаточно строгим.
Более корректное определение этих понятий таково:2.2. Как обосновывать свойства систем переходов61Условия справедливости можно включить в явном виде в состав определения формальной модели, как это было сделано в работе Манны и Пнуели [138].Большинство алгоритмов, с которыми нам предстоит иметь дело в настоящейкниге, не зависят от этих условий; поэтому мы предпочли не включать их в состав модели, а вместо этого будем явно оговаривать эти условия всякий раз, когдаони используются в том или ином алгоритме или задаче. Вопрос о целесообразности включения допущений справедливости в состав модели распределеннойсистемы вызвал немало споров. Сложилось убеждение, что на допущения справедливости не следует рассчитывать; вместо этого сами алгоритмы должны бытьустроены так, чтобы они не зависели от этих допущений.
Обсуждение некоторыхзамысловатых аспектов, связанных с допущениями справедливости, можно найтив работе [89].2.2. Как обосновывать свойства систем переходовЕсли имеется распределенный алгоритм для некоторой задачи, то необходимоубедиться в том, что данный алгоритм правильно решает эту задачу. Исходя изсамой задачи можно определить, какими свойствами должен обладать требуемыйалгоритм ее решения; после этого нужно показать, что предложенное решениеобладает этими свойствами. Проблема верификации распределенных алгоритмовпривлекла большое внимание, и существует много работ, в которых обсуждаются формальные методы верификации (см, например, [46, 89, 115, 138]). В этомпараграфе мы обсудим ряд простых, но при этом наиболее часто используемыхметодов обоснования корректности распределенных алгоритмов.
Эти методы основываются только на определении понятия системы переходов.Многие свойства распределенных алгоритмов, нуждающиеся в проверке, относятся к одному из двух типов: условие безопасности и условие живости .Условие безопасности требует, чтобы каждая достижимая конфигурация в любом выполнении системы обладала определенным свойством. Условие живоститребует, чтобы хотя бы одна достижимая конфигурация в любом выполнениисистемы обладала определенным свойством. Формальное изучение вопроса о том,как устроены свойства безопасности и живости, было предпринято в работе Альперна и Шнейдера [6]. Они установили, что каждая возможная спецификация(свойство множества выполнений) может быть представлена в виде конъюнкциисвойств безопасности и живости.Эти условия могут возникнуть также и в более слабой форме; например, может потребоваться, чтобы они соблюдались с некоторой заданной вероятностьюна множестве всех возможных выполнений.
Другие условия, которым должны1) . каждое выполнение, оканчивающееся заключительной конфигурацией, является справедливым(как в слабом, так и в сильном смысле);2) . бесконечное выполнение Е = (yo , Yi, Y2 > • ■•) считается слабо справедливым, если не существует такого натурального числа п, п > 0, и такого события е, что для любого i, i ф я, событие едопустимо в конфигурации у;, но при этом y ^ i У е(у;);3 ) . бесконечное выполнение Е = ( y o , yi, У г , • • •) считается сильно справедливым, если не существует такого натурального числа п, п > 0, и такого события е, что для любого i, i ф я, событие едопустимо в некоторой конфигурации ур, где / ^ i, но при этом y;+i ф е(ур. — Прим, перев.62Гл. 2. Модельудовлетворять алгоритмы, могут выражать требования о том, чтобы в этих алгоритмах использовались только сведения определенного рода (см.
§2.4.4), чтобыалгоритмы были устойчивы к сбоям в отдельных процессах (см. гл. 13), чтобыпроцессы были неотличимы (см. гл. 9), и т. п.Методы верификации,описанные в этом параграфе, основываются на истинности у т в е р ж д е н и й о конфигурациях, достижимых по ходу выполнения.
Такогорода методы называются а с с е р т и в н ы м и 2) методами верификации. Под утверждением понимается одноместное отношение на множестве конфигураций, т. е.предикат, который является истинным на множестве одних конфигураций и ложным на множестве других.2.2.1. Свойства безопасностиСвойством безопасности алгоритма является всякое свойство, которое можно сформулировать в виде следующего предложения: «Для любого выполненияалгоритма утверждение Р истинно в каждой конфигурации выполнения». Болеекратко это свойство можно сформулировать так: «Утверждение Р всегда истинно».
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
