Preuves d'exactitude des Paxos classiques et des Paxos rapides

Je lis le document "Fast Paxos" de Leslie Lamport et je suis coincé avec les preuves d'exactitude des deux Paxos classiques et Fast Paxos.

Par souci de cohérence, la valeur $v$ choisie par le coordinateur dans la phase $2a$ du tour $i$ doit satisfaire

$CP(v,i):$ Pour tout tour$j < i$ , aucune valeur autre que$v$ n'a été ou pourrait encore être choisie au tour$j$ .

Pour les Paxos classiques , la preuve (page 8) est divisée en trois cas: , j = k et j < k , où k est le plus grand nombre rond dans lequel un accepteur a signalé au coordinateur par la phase 1 b message. Je n'ai pas compris l'argument du troisième cas:$k < j < i$$j = k$$j < k$$k$$1b$

Cas . On peut supposer par induction que la propriété C P maintenu lorsque l' accepteur a 0 voté pour v dans tour $j < k$$CP$$a_0$$v$$k$ . Cela implique qu'aucune valeur autre que n'a été ou pourrait encore être choisie au tour j .$v$$j$

Ma question est:

1. Pourquoi peut - on supposer que la propriété tenu lorsque l' accepteur a 0 voté pour v dans tour k ?$CP$$a_0$$v$$k$

Il semble que nous utilisons l'induction mathématique, par conséquent, quelle est la base, l'hypothèse inductive et les étapes inductives?

Pour Fast Paxos , le même argument (Page 18) continue. Ça dit,

Cas . Pour tout v dans V , aucune valeur autre que $j < k$$v$$V$$v$ n'a été ou pourrait encore être choisie au tour .$j$

Ma question est:

2. Comment est-ce obtenu? En particulier, pourquoi "Pour tout dans$v$ " est-il ici?$V$

À mon avis, la preuve d'exactitude du cas repose (récursivement) sur celles des cas de k < j < i et $j < k$$k < j < i$ . $j = k$

Par conséquent, comment pouvons-nous conclure le cas sans prouver d'abord j = k complètement (à savoir, manquer le sous-cas de j = k où $j < k$$j = k$$j = k$$V$ contient plus d'une valeur)?

Pourquoi pouvons-nous supposer que la propriété CP était détenue lorsque l'accepteur a0 a voté pour v au tour k? Il semble que nous utilisons l'induction mathématique, par conséquent, quelle est la base, l'hypothèse inductive et les étapes inductives?

Vous regardez un exemple d' induction forte . Dans l'induction simple, vous supposez que la propriété est vraie pour et prouvez qu'elle est vraie pour n = m + 1 . Dans une forte induction, vous supposez que la propriété est vraie pour ∀ n : n < m et prouvez qu'elle est vraie pour n = m + $n=m$$n=m+1$$\forall n: n<m$$n=m+1$ .

Base (je crois): $j = 0$ . C'est-à-dire le round nul (puisque les rounds commencent à 1). C'est trivialement vrai, c'est probablement pourquoi cela n'a pas été dit explicitement.

Étape inductive : Supposons ; prouver C P ( v ; j + 1 ) où j < $\forall n, n \le j : CP(v; n)$$CP(v; j+1)$$j < i$ .

Croyez-le ou non, ce n'est qu'un croquis de preuve . La vraie preuve se trouve dans le document du Parlement à temps partiel . (Certains considèrent le papier cryptique, d'autres le considèrent comme humoristique.)

Comment est-ce obtenu?

À mon avis, la preuve d'exactitude du cas repose (récursivement) sur celles des cas de k < j < i et j = k .$j<k$$k<j<i$$j=k$

Par conséquent, comment pouvons-nous conclure le cas sans prouver d'abord j = k complètement (à savoir, manquer le sous-cas de j = k où V contient plus d'une valeur)?$j<k$$j=k$$j=k$$V$

Il s'agit là encore d'une forte induction, donc le cas repose sur les cas de k < j et j = k , mais à travers l'hypothèse d'induction$j<k$$k<j$$j=k$ , à savoir du précédent tour de Paxos.

Conseils généraux pour les épreuves de Lamport.

Lamport utilise une technique de preuves hiérarchiques. Par exemple, la structure de la preuve aux pages 7-8 ressemble un peu à ceci:

• Supposons que ; prouver C P ( v ; j + 1 ) où j < i . $\forall n, n \le j : CP(v; n)$$CP(v; j+1)$$j < i$
  1. Observation 1
  2. Observation 2
  3. Observation 3
  4. $k = argmax (...)$
  5. cas k = 0
  6. cas k> 0
     • cas k <j
     • cas k = j
     • cas j <k

Lamport a tendance à utiliser un autre type de hiérarchie. Il prouvera un algorithme plus simple, puis prouvera qu'un algorithme plus complexe correspond (ou "étend" ) à l'algorithme plus simple. Cela ne semble pas se produire à la page 18, mais c'est quelque chose à surveiller. (La preuve de la page 18 semble être une modification de la preuve des pages 7-8, pas une extension de celle-ci.)

Lamport s'appuie fortement sur une forte induction ; il a également tendance à penser en termes d' ensembles plutôt qu'en termes de nombres. Vous pouvez donc obtenir des ensembles vides là où d'autres auraient des zéros ou des valeurs nulles; ou mettre en place des syndicats là où d'autres auraient plus.

La démonstration de l'exactitude des systèmes de transmission de messages asynchrones nécessite une vue omnisciente du système par rapport au temps . Par exemple, lorsque vous envisagez des actions dans le tour , gardez à l'esprit que les actions pour un tour j < i peuvent ne pas avoir eu lieu temporairement!$i$$j < i$ . Et pourtant, Lamport déclare ces événements potentiellement futurs au passé.

Les systèmes Lamports et les preuves ont généralement une variable ou un ensemble de variables qui ne peuvent aller que dans une seule direction; incrémenter uniquement les nombres et uniquement ajouter aux ensembles. Ceci est largement utilisé dans ses épreuves. Par exemple, à la page 8, Lamport montre comment il a annulé la capacité future d' à voter un autre:$a$

... Puisqu'il a mis à i lors de l'envoi d'un message, a n'aurait pas pu voter par la suite dans un tour de moins de i ....$rnd[a]$$i$$a$$i$

C'est définitivement une civilisation cérébrale pour prouver ce genre de systèmes.

(mise à jour) : Liste les invariants; Lamport utilise beaucoup d'invariants lors du développement et de ses preuves. Ils sont parfois dispersés dans les épreuves; parfois, ils ne sont présents que dans l'épreuve vérifiée par machine. Raison de chaque invariant; pourquoi est-il là? Comment interagit-il avec les autres invariants? Comment chaque étape du système conserve-t-elle cet invariant?

Divulgation complète : je n'avais pas lu Fast Paxos jusqu'à ce qu'on me demande de répondre à cette question; et n'a regardé que les pages citées. Je suis ingénieur et non mathématicien; mon pinceau avec le travail de Lamport est basé uniquement sur la nécessité d'inventer et de maintenir correctement des systèmes distribués à grande échelle.

Ma réponse repose largement sur mon expérience avec le travail de Lamport. J'ai lu plusieurs protocoles et preuves de Lamport; Je maintiens professionnellement un système basé sur paxos; J'ai écrit et prouvé un protocole de consensus à haut débit, et encore une fois, je maintiens professionnellement un système basé sur celui-ci (j'essaie d'obtenir que mon entreprise me permette de publier un article). J'ai collaboré à un document insignifiant avec Lamport, où je l' ai rencontré trois fois (le papier est toujours en attente d' examen par les pairs.)