Справедливость (англ. fairness). При исследовании поведения распределенных систем часто возникает необходимость ограничиться рассмотрением только так называемых справедливых выполнений (англ. fair executions). Условия слабой справедливости позволяют исключить из рассмотрения такие выполнения, в которых некоторые события оказываются постоянно допустимыми для бесконечного числа идущих подряд глобальных состояний, но при этом ни разу не происходят в виде переходов из этих состояний из-за того, что выполнение продолжается всякий раз за счет других допустимых событий. Условия сильной справедливости позволяют исключить из рассмотрения такие выполнения, в которых некоторые события оказываются бесконечно часто допустимыми для глобальных состояний в выполнении, но при этом ни разу не происходят в виде переходов из этих состояний из-за того, что выполнение продолжается всякий раз за счет других допустимых событий. Другими словами, выполнение считается слабо справедливым, если ни одно событие не может оставаться постоянно допустимым без того, чтобы, в конце концов, не произойти в виде перехода. Выполнение считается сильно справедливым, если ни одно событие не может оказываться допустимым бесконечно часто без того, чтобы, в конце концов, не произойти в виде перехода.
Безопасность (англ. safety) и живучесть (англ. liveness). При разработке распределенного алгоритма, решающего ту или иную задачу, необходимо показать, что полученный алгоритм действительно представляет собой корректное решение поставленной задачи. Существует два фундаментальных типа свойств, проверяемых для подтверждения корректности распределенного алгоритма: безопасность и живучесть.
Неформально можно сказать, что алгоритм удовлетворяет свойству безопасности, если "что-то плохое никогда не случается". Другими словами, условие безопасности требует, чтобы определенное утверждение оставалось истинным в каждом достижимом глобальном состоянии в любом выполнении. Для иллюстрации этого требования можно привести пример системы управления сигналами светофоров; тогда требование безопасности будет выражаться в том, что при любом распределении
сигналов светофоров одновременное движение по пересекающимся направлениям на перекрестке должно быть запрещено.
Однако из того, что в системе не может произойти ничего плохого, совсем не следует, что в ней может случиться что-то хорошее. Так, программные системы, которые ничего не делают, всегда удовлетворяют требованиям безопасности: в них ничего не происходит, и, как следствие, ничего плохого тоже не случается. Или, например, для системы управления сигналами светофоров требование безопасности можно выполнить путем разрешения проезда только в одном направлении и полного запрещения движения в другом.
Таким образом требования безопасности должны сопровождаться требованиями прогресса вычислительной системы в нужном направлении. Такие требования называются живучестью. Неформально можно сказать, что алгоритм удовлетворяет свойству живучести, если "что-то хорошее рано или поздно случится". Другими словами, условие живучести требует, чтобы определенное утверждение становилось истинным хотя бы в одном достижимом глобальном состоянии в любом выполнении. Для нашего примера системы управления сигналами светофоров это свойство должно выражаться в обеспечении возможности, рано или поздно, проехать по любому направлению на перекрестке.
Do'stlaringiz bilan baham: |