Доказательства правильности классических Paxos и Fast Paxos

Я читаю статью «Быстрых Паксосов» Лесли Лампорта и застреваю с доказательствами правильности как классических Паксосов, так и Быстрых Паксосов.

Для согласованности значение $v$ выбранное координатором на этапе $2a$ в раунде $i$ должно удовлетворять

$CP(v,i):$ Для любого раунда$j < i$ никакое значение, кроме$v$ не было или не могло быть выбрано в раунде$j$ .

Для классического Paxos доказательство (стр. 8) разбито на три случая: $k < j < i$ , $j = k$ и $j < k$ , где $k$ - наибольшее круглое число, в котором какой-то акцептор сообщил координатору по фазе $1b$ сообщение. Я не понял аргументацию для третьего случая:

Случай . По индукции можно предположить, что свойство C P имеет место, когда акцептор a 0 проголосовал за v в раунде k . Это подразумевает, что никакое значение, кроме v, не было и не могло быть выбрано в раунде j .$j < k$$CP$$a_0$$v$$k$$v$$j$

Мой вопрос:

1. Почему мы можем предположить , что свойство проходит при акцепторе 0 проголосовали против в первом раунде к ?$CP$$a_0$$v$$k$

Кажется, что мы используем математическую индукцию, поэтому, какова основа, индуктивная гипотеза и индуктивные шаги?

Для Быстрых Паксосов тот же самый аргумент (Страница 18) продолжается. Это говорит,

Случай . Для любого v в V никакое значение, кроме v, не было и не может быть выбрано в раунде j .$j < k$$v$$V$$v$$j$

Мой вопрос:

2. Как это получается? В частности, почему здесь «Для любого в V »?$v$$V$

На мой взгляд, доказательство правильности случая опирается (рекурсивно) на доказательства случаев k < j < i и j = k . $j < k$$k < j < i$$j = k$

Следовательно, как мы можем завершить случай не доказав сначала полностью j = k (а именно, пропуская подслучае j = k, где V содержит более одного значения)?$j < k$$j = k$$j = k$$V$

Почему мы можем предположить, что свойство CP сохранялось, когда акцептор a0 голосовал за v в раунде k? Кажется, что мы используем математическую индукцию, поэтому, какова основа, индуктивная гипотеза и индуктивные шаги?

Вы смотрите на пример сильной индукции . В простой индукции вы предполагаете, что свойство верно для и доказываете, что оно верно для n = m + 1 . В сильной индукции вы предполагаете, что свойство верно для ∀ n : n < m, и доказываете, что оно верно для n = m + 1 .$n=m$$n=m+1$$\forall n: n<m$$n=m+1$

Основа (я считаю): . То есть нулевой раунд (поскольку раунды начинаются с 1). Это тривиально верно, поэтому, вероятно, это не было указано явно.$j = 0$

Индуктивный шаг : предположим, что ; докажите C P ( v ; j + 1 ), где j < i .$\forall n, n \le j : CP(v; n)$$CP(v; j+1)$$j < i$

Хотите верьте, хотите нет, это всего лишь доказательство . Настоящее доказательство в статье Парламента неполного рабочего дня . (Некоторые считают бумагу загадочной, другие считают ее юмористической.)

Как это получается?

На мой взгляд, доказательство правильности случая опирается (рекурсивно) на доказательства случаев k < j < i и j = k .$j<k$$k<j<i$$j=k$

Следовательно, как мы можем завершить случай не доказав сначала полностью j = k (а именно, пропуская подслучае j = k, где V содержит более одного значения)?$j<k$$j=k$$j=k$$V$

Это опять-таки сильная индукция, поэтому случай опирается на случаи k < j и j = k , но с помощью гипотезы индукции , а именно из предыдущего раунда Паксоса.$j<k$$k<j$$j=k$

Общие советы по доказательствам Лампорта.

Лампорт использует технику иерархических доказательств. Например, структура доказательства на страницах 7-8 выглядит примерно так:

• Предположим, что ; докажите C P ( v ; j + 1 ), где j < i . $\forall n, n \le j : CP(v; n)$$CP(v; j+1)$$j < i$
  1. Наблюдение 1
  2. Наблюдение 2
  3. Наблюдение 3
  4. $k = argmax (...)$
  5. случай k = 0
  6. случай k> 0
     • случай k <j
     • случай k = j
     • случай j <k

Лампорт имеет тенденцию использовать другой тип иерархии. Он докажет более простой алгоритм, а затем докажет, что более сложный алгоритм отображает (или «расширяет» ) более простой алгоритм. Похоже, этого не происходит на странице 18, но на это стоит обратить внимание. (Доказательство на странице 18 представляется модификацией доказательства на страницах 7-8; не является его расширением .)

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

Для доказательства правильности асинхронных систем передачи сообщений необходимо всестороннее представление системы относительно времени . Например, при рассмотрении действий в раунде имейте в виду, что действия для некоторого раунда j < i, возможно, не произошли во времени! , И все же Лампорт утверждает эти потенциально будущие события в прошедшем времени.$i$$j < i$

Системы и доказательства Лампорта, как правило, имеют переменную или набор переменных, которые допускаются только в одном направлении; только увеличивающиеся числа и только добавляющие к наборам. Это широко используется в его доказательствах. Например, на странице 8 Лэмпорт показывает, как он кастрировал будущую способность дать еще один голос:$a$

... Так как при отправке сообщения было установлено значение для i , a впоследствии не мог отдать свой голос ни в одном раунде с номером меньше, чем i ....$rnd[a]$$i$$a$$i$

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

(обновление) : перечислить инварианты; Лампорт использует много инвариантов при разработке и свои доказательства. Они иногда разбросаны по всем доказательствам; иногда они присутствуют только в проверенном машиной доказательстве. Причина каждого инварианта; почему это там? Как это взаимодействует с другими инвариантами? Как каждый шаг в системе сохраняет этот инвариант?

Полное раскрытие : я не читал Fast Paxos, пока меня не попросили ответить на этот вопрос; и только посмотрел на цитируемых страницах. Я инженер, а не математик; Моя работа с Лампортом основана исключительно на необходимости правильно изобретать и обслуживать крупномасштабные распределенные системы.

Мой ответ во многом зависит от моего опыта работы Лампорта. Я прочитал несколько протоколов и доказательств Лампорта; Я профессионально поддерживаю систему на основе Paxos; Я написал и испытал протокол согласования с высокой пропускной способностью и снова профессионально поддерживаю систему, основанную на нем (я пытаюсь заставить свою компанию разрешить мне публиковать статью). Я уже сотрудничал в незначительной работе с Лампорт, в котором я встречался с ним трижды (документ еще находится на рассмотрении экспертной оценки.)