Provas de correção dos Paxos clássicos e Paxos rápidos

Estou lendo o artigo "Fast Paxos" de Leslie Lamport e fico preso às provas de correção dos clássicos Paxos e Fast Paxos.

Por consistência, o valor escolhido pelo coordenador na fase 2 a na rodada i deve satisfazer$v$$2a$$i$

Para qualquer rodada j < i , nenhum valor diferente de v foi ou pode ainda ser escolhido na rodada j .$CP(v,i):$$j < i$$v$$j$

Para Paxos clássico , a prova (página 8) é dividida em três casos: , j = k , e j < k , onde k é o maior número rodada em que alguns aceitador foi relatado para o coordenador de fase 1 b mensagem. Não entendi o argumento do terceiro caso:$k < j < i$$j = k$$j < k$$k$$1b$

Caso . Podemos assumir, por indução, que a propriedade C P mantinha quando o aceitador a 0 votou em v na rodada k . Isso implica que nenhum valor diferente de v foi ou ainda pode ser escolhido na rodada j .$j < k$$CP$$a_0$$v$$k$$v$$j$

Minha pergunta é:

1. Por que podemos assumir que a propriedade mantida quando o aceitador a 0 votou em v na rodada k ?$CP$$a_0$$v$$k$

Parece que estamos usando indução matemática, portanto, quais são as bases, hipóteses indutivas e etapas indutivas?

Para o Fast Paxos , o mesmo argumento (Página 18) continua. Diz,

Caso . Para qualquer v em V , nenhum valor diferente de v foi ou ainda pode ser escolhido na rodada j .$j < k$$v$$V$$v$$j$

Minha pergunta é:

2. Como isso é obtido? Em particular, por que "Para qualquer em V " está aqui?$v$$V$

Na minha opinião, a prova de correcção do caso depende (de forma recursiva) sobre aqueles de casos de k < j < i e j = k . $j < k$$k < j < i$$j = k$

Portanto, como podemos concluir o caso sem provar primeiro j = k completamente (ou seja, faltando a subcaixa de j = k onde V contém mais de um valor)?$j < k$$j = k$$j = k$$V$

Por que podemos assumir que a propriedade CP mantida quando o aceitador a0 votou em v na rodada k? Parece que estamos usando indução matemática, portanto, quais são as bases, hipóteses indutivas e etapas indutivas?

Você está vendo um exemplo de forte indução . Na indução simples, você assume que a propriedade vale para e prova que ela vale para n = m + 1 . Na indução forte, você assume que a propriedade vale para ∀ n : n < m e prova que ela vale para n = m + $n=m$$n=m+1$$\forall n: n<m$$n=m+1$ .

Base (acredito): . Ou seja, a rodada nula (já que as rodadas começam em 1). Isso é trivialmente verdade, e é provavelmente por isso que não foi afirmado explicitamente.$j = 0$

Etapa indutiva : Suponha ; provar C P ( v ; j + 1 ) onde j < i .$\forall n, n \le j : CP(v; n)$$CP(v; j+1)$$j < i$

Acredite ou não, este é apenas um esboço de prova . A prova real está no documento do Parlamento em Tempo Parcial . (Alguns consideram o papel enigmático, outros o consideram engraçado.)

Como isso é obtido?

Na minha opinião, a prova de correcção do caso depende (de forma recursiva) sobre aqueles de casos de k < j < i e j = k .$j<k$$k<j<i$$j=k$

Portanto, como podemos concluir o caso sem provar primeiro j = k completamente (ou seja, faltando a subcaixa de j = k onde V contém mais de um valor)?$j<k$$j=k$$j=k$$V$

Isso é novamente forte indução, portanto o caso se baseia nos casos de k < j e j = k , mas através da hipótese de indução , a saber, da rodada anterior de Paxos.$j<k$$k<j$$j=k$

Dicas gerais para as provas de Lamport.

Lamport usa uma técnica de provas hierárquicas. Por exemplo, a estrutura da prova nas páginas 7-8 é mais ou menos assim:

• Suponha ; provar C P ( v ; j + 1 ) onde$\forall n, n \le j : CP(v; n)$$CP(v; j+1)$ . $j < i$
  1. Observação 1
  2. Observação 2
  3. Observação 3
  4. $k = argmax (...)$
  5. caso k = 0
  6. caso k> 0
     • caso k <j
     • caso k = j
     • caso j <k

Lamport tende a usar outro tipo de hierarquia. Ele provará um algoritmo mais simples e depois provará que um algoritmo mais complexo mapeia (ou "estende" ) o algoritmo mais simples. Isso não parece estar acontecendo na página 18, mas é algo a se observar. (A prova na página 18 parece ser uma modificação da prova nas páginas 7-8; não uma extensão dela.)

Lamport depende fortemente de forte indução ; ele também tende a pensar em termos de conjuntos em vez de números. Portanto, você pode obter conjuntos vazios onde outros teriam zeros ou nulos; ou estabelecer sindicatos onde outros teriam acréscimo.

A comprovação da correção dos sistemas de passagem de mensagens assíncronas precisa de uma visão onisciente do sistema em relação ao tempo . Por exemplo, ao considerar ações na rodada , lembre-se de que as ações de uma rodada j < i podem não ter ocorrido temporalmente!$i$$j < i$ . E, no entanto, Lamport afirma esses eventos potencialmente futuros no passado.

Os sistemas e provas de Lamports tendem a ter uma variável ou conjunto de variáveis ​​que só podem seguir uma direção; apenas incrementando números e adicionando apenas a conjuntos. Isso é usado extensivamente em suas provas. Por exemplo, na página 8, Lamport mostra como ele neutralizou a capacidade futura de dar outro voto:$a$

... Como definiu para i ao enviar uma mensagem, a não poderia posteriormente ter votado em nenhuma rodada numerada menos que i ....$rnd[a]$$i$$a$$i$

Definitivamente, é um esticador de cérebro provar esses tipos de sistemas.

(atualização) : Liste os invariantes; Lamport usa muitos invariantes ao desenvolver e suas provas. Às vezes, eles estão espalhados pelas provas; Às vezes, eles estão presentes apenas na prova verificada pela máquina. Razão sobre cada invariante; porque esta ai? Como ele interage com os outros invariantes? Como cada etapa do sistema mantém essa invariante?

Divulgação completa : eu não tinha lido o Fast Paxos até que me pediram para responder a essa pergunta; e apenas olhou para as páginas citadas. Sou engenheiro e não matemático; meu contato com o trabalho de Lamport se baseia puramente na necessidade de inventar e manter corretamente sistemas distribuídos em larga escala.

Minha resposta depende muito da minha experiência com o trabalho de Lamport. Eu li vários protocolos e provas de Lamport; Eu mantenho profissionalmente um sistema baseado em paxos; Escrevi e provei um protocolo de consenso de alto rendimento e, novamente, mantenho profissionalmente um sistema baseado nele (estou tentando fazer minha empresa me permitir publicar um artigo). I têm colaborado em um papel insignificante com Lamport, em que me encontrei com ele três vezes (o papel ainda está pendente de revisão por pares).