Pruebas de corrección de Paxos clásico y Paxos rápido

Estoy leyendo el documento "Fast Paxos" de Leslie Lamport y me quedo atascado con las pruebas de corrección de Paxos clásico y Fast Paxos.

Por consistencia, el valor recogió por el coordinador en fase en la ronda debería satisfacer2 a $v$$2a$$i$

$CP(v,i):$ para cualquier ronda , ningún valor que no sea ha sido o podría ser elegido en la ronda .v $j < i$$v$$j$

Para Paxos clásico , la prueba (Página 8) se divide en tres casos: , , y , donde es el número redondo más grande en el que algún aceptante ha informado al coordinador por mensaje de fase . No entendí el argumento para el tercer caso:j = k j < k k 1 $k < j < i$$j = k$$j < k$$k$$1b$

Caso . Podemos suponer por inducción que la propiedad mantenida cuando el aceptador votó por en la ronda . Esto implica que ningún valor distinto de ha sido o podría ser elegido en la ronda .$j < k$a 0 v k v $CP$$a_0$$v$$k$$v$$j$

Mi pregunta es:

1. ¿Por qué podemos suponer que la propiedad mantenida cuando el aceptador votó por en la ronda ?a 0 v $CP$$a_0$$v$$k$

Parece que estamos usando la inducción matemática, por lo tanto, ¿cuáles son las bases, la hipótesis inductiva y los pasos inductivos?

Para Fast Paxos , continúa el mismo argumento (Página 18). Dice,

Caso . Para cualquier en , ningún valor que no sea ha sido o podría ser elegido en la ronda .v V v $j < k$$v$$V$$v$$j$

Mi pregunta es:

2. ¿Cómo se obtiene esto? En particular, ¿por qué está aquí "Para cualquier en "?$v$$V$

En mi opinión, la prueba de corrección del caso basa (recursivamente) en los casos de y . k < j < i j = $j < k$$k < j < i$$j = k$

Por lo tanto, ¿cómo podemos concluir el caso sin probar primero completo (es decir, omitiendo el subcase de donde contiene más de un valor)?j = k j = k $j < k$$j = k$$j = k$$V$

¿Por qué podemos suponer que la propiedad CP mantenida cuando el aceptador a0 votó por v en la ronda k? Parece que estamos usando la inducción matemática, por lo tanto, ¿cuáles son las bases, la hipótesis inductiva y los pasos inductivos?

Estás viendo una instancia de inducción fuerte . En la inducción simple, usted asume que la propiedad es válida para demuestra que es válida para . En una inducción fuerte, asume que la propiedad es válida para demuestra que es válida para .n = m + 1 ∀ n : n < m n = m + $n=m$$n=m+1$$\forall n: n<m$$n=m+1$

Base (creo): . Es decir, la ronda nula (ya que las rondas comienzan en 1). Esto es trivialmente cierto, lo que probablemente sea la razón por la que no se declaró explícitamente.$j = 0$

Paso inductivo : Suponga ; probar donde .C P ( v ; j + 1 ) j < $\forall n, n \le j : CP(v; n)$$CP(v; j+1)$$j < i$

Lo creas o no, esto es solo un boceto de prueba . La prueba real está en el documento del Parlamento a tiempo parcial . (Algunos consideran el papel críptico, otros lo consideran humorístico).

¿Cómo se obtiene esto?

En mi opinión, la prueba de corrección del caso basa (recursivamente) en los casos de y .k < j < i j = $j<k$$k<j<i$$j=k$

Por lo tanto, ¿cómo podemos concluir el caso sin probar primero completo (es decir, omitiendo el subcase de donde contiene más de un valor)?j = k j = k $j<k$$j=k$$j=k$$V$

Esto es nuevamente una inducción fuerte, por lo que el caso se basa en los casos de y , pero a través de la hipótesis de inducción , es decir, de la ronda anterior de Paxos.k < j j = $j<k$$k<j$$j=k$

Consejos generales para las pruebas de Lamport.

Lamport utiliza una técnica de pruebas jerárquicas. Por ejemplo, la estructura de la prueba en las páginas 7-8 se parece a esto:

• Suponga ; probar donde . C P ( v ; j + 1 ) j < $\forall n, n \le j : CP(v; n)$$CP(v; j+1)$$j < i$
  1. Observación 1
  2. Observación 2
  3. Observación 3
  4. $k = argmax (...)$
  5. caso k = 0
  6. caso k> 0
     • caso k <j
     • caso k = j
     • caso j <k

Lamport tiende a usar otro tipo de jerarquía. Él probará un algoritmo más simple, y luego probará que un algoritmo más complejo se mapea (o "extiende" ) al algoritmo más simple. Esto no parece estar sucediendo en la página 18, pero es algo a tener en cuenta. (La prueba en la página 18 parece ser una modificación de la prueba a las páginas 7-8; no una extensión de la misma).

Lamport depende en gran medida de una fuerte inducción ; También tiende a pensar en términos de conjuntos en lugar de números. Entonces puede obtener conjuntos vacíos donde otros tendrían ceros o nulos; o establecer sindicatos donde otros tendrían más.

Probar la corrección de los sistemas de paso de mensajes asíncronos necesita una visión omnisciente del sistema con respecto al tiempo . Por ejemplo, al considerar acciones en la ronda , ¡tenga en cuenta que las acciones para alguna ronda pueden no haber sucedido temporalmente! . Y, sin embargo, Lamport declara estos eventos potencialmente futuros en tiempo pasado.j < $i$$j < i$

Los sistemas y pruebas de Lamports tienden a tener una variable o un conjunto de variables que solo pueden ir en una dirección; solo incrementando números y solo agregando a conjuntos. Esto se usa ampliamente en sus pruebas. Por ejemplo, en la página 8, Lamport muestra cómo neutralizó la capacidad futura de para emitir otro voto:$a$

... Dado que estableció en al enviar un mensaje, no pudo haber votado posteriormente en una ronda numerada menor que ...i a $rnd[a]$$i$$a$$i$

Definitivamente es un estiramiento mental para probar este tipo de sistemas.

(actualización) : enumere los invariantes; Lamport usa muchos invariantes cuando se desarrolla y sus pruebas. A veces se encuentran dispersos por las pruebas; a veces solo están presentes en la prueba verificada por la máquina. Razón sobre cada invariante; por que esta ahi ¿Cómo interactúa con los otros invariantes? ¿Cómo cada paso en el sistema mantiene esta invariante?

Revelación completa : no había leído Fast Paxos hasta que me pidieron que respondiera esta pregunta; y solo miraba las páginas citadas. Soy ingeniero y no matemático; mi pincel con el trabajo de Lamport se basa únicamente en la necesidad de inventar y mantener correctamente sistemas distribuidos a gran escala.

Mi respuesta se basa en gran medida en mi experiencia con el trabajo de Lamport. He leído varios de los protocolos y pruebas de Lamport; Mantengo profesionalmente un sistema basado en paxos; He escrito y probado un protocolo de consenso de alto rendimiento, y nuevamente mantengo profesionalmente un sistema basado en él (estoy tratando de hacer que mi compañía me permita publicar un artículo). Yo he colaborado en un papel insignificante con Lamport, en la que me encontré con él tres veces (el papel todavía está pendiente de revisión por pares).