Dowody poprawności klasycznych Paxos i Fast Paxos

13

Czytam artykuł „Fast Paxos” autorstwa Leslie Lamport i utknąłem z dowodami poprawności zarówno klasycznych Paxos, jak i Fast Paxos.

Aby zachować spójność, wartość wybrana przez koordynatora w fazie 2 a w rundzie i powinna spełniaćv2ai

Dla dowolnej rundy j < i żadna wartość inna niż v nie była lub może być wybrana w rundzie j .CP(v,i):j<ivj


W przypadku klasycznego Paxos dowód (strona 8) jest podzielony na trzy przypadki: , j = k oraz j < k , gdzie k jest największą liczbą zaokrągloną, w której jakiś akceptor zgłosił koordynatorowi w fazie 1 b wiadomość. Nie zrozumiałem argumentu trzeciego przypadku:k<j<ij=kj<kk1b

Przypadek . Możemy założyć, przez indukcję , że własność C P odbyło gdy akceptor 0 głosował na V w rundzie k . Oznacza to, że w rundzie j nie wybrano ani nie można było wybrać innej wartości niż v .j<kCPa0vkvj

Moje pytanie brzmi:

  1. Dlatego można założyć, że nieruchomość odbyło gdy akceptor 0 głosował na V w rundzie k ?CPa0vk

Wydaje się, że używamy indukcji matematycznej, a zatem, na czym polegają podstawy, hipoteza indukcyjna i kroki indukcyjne?


W przypadku Fast Paxos ten sam argument (Strona 18) jest kontynuowany. To mówi,

Przypadek . Dla dowolnego v w V , żadna inna wartość niż v nie była lub może być jeszcze wybrana w rundzie j .j<kvVvj

Moje pytanie brzmi:

  1. Jak to uzyskać? W szczególności dlaczego tutaj jest „For any in V ”?vV

Moim zdaniem dowód poprawności przypadku opiera się (rekurencyjnie) na przypadkach k < j < i oraz j = k . j<kk<j<ij=k

Zatem jak możemy zakończyć przypadek bez uprzedniego pełnego udowodnienia j = k (czyli pominięcia podtekstu j = k, gdzie V zawiera więcej niż jedną wartość)?j<kj=kj=kV

hengxin
źródło

Odpowiedzi:

10

Dlaczego możemy założyć, że nieruchomość CP jest utrzymywana, gdy akceptor a0 głosował za v w rundzie k? Wydaje się, że używamy indukcji matematycznej, a zatem, na czym polegają podstawy, hipoteza indukcyjna i kroki indukcyjne?

n=mn=m+1n:n<mn=m+1

j=0

n,nj:CP(v;n)CP(v;j+1)j<i

Wierzcie lub nie, to tylko szkic próbny . Prawdziwy dowód znajduje się w dokumencie Parlamentu w niepełnym wymiarze godzin . (Niektórzy uważają papier za tajemniczy, inni uważają, że jest to śmieszne).


Jak to uzyskać?

j<kk<j<ij=k

Zatem jak możemy zakończyć przypadek j < k bez uprzedniego pełnego udowodnienia j = k (czyli pominięcia podtekstu j = k, gdzie Vj<kj=kj=kV

j<kk<jj=k


Ogólne wskazówki dotyczące dowodów Lamporta.

Lamport stosuje technikę dowodów hierarchicznych. Na przykład struktura dowodu na stronach 7-8 wygląda mniej więcej tak:

  • n,nj:CP(v;n)CP(v;j+1)j<i
    1. Obserwacja 1
    2. Obserwacja 2
    3. Obserwacja 3
    4. k=argmax(...)
    5. przypadek k = 0
    6. przypadek k> 0
      • przypadek k <j
      • przypadek k = j
      • przypadek j <k

Lamport ma tendencję do używania innego rodzaju hierarchii. Udowodni prostszy algorytm, a następnie udowodni, że bardziej złożony algorytm odwzorowuje (lub „rozszerza” ) prostszy algorytm. Wydaje się, że tak się nie dzieje na stronie 18, ale należy na to uważać. (Dowód na stronie 18 wydaje się być modyfikacją dowodu na stronach 7-8; nie jest jego przedłużeniem ).

Lamport opiera się w dużej mierze na silnej indukcji ; on również myśli w kategoriach zbiorów zamiast liczb. Możesz więc otrzymać puste zestawy, w których inni mieliby zera lub null; lub zakładaj związki, do których inni będą dodawać.

ij<i

a

rnd[a]iai

Zdecydowanie jest to rozrost mózgu, aby udowodnić tego rodzaju systemy.

(aktualizacja) : Wymień niezmienniki; Lamport używa wielu niezmienników podczas opracowywania i swoich dowodów. Czasami są rozrzucone po dowodach; czasami są one obecne tylko w dowodzie sprawdzonym maszynowo. Powód każdego niezmiennika; dlaczego tam jest Jak to współdziała z innymi niezmiennikami? W jaki sposób każdy krok w systemie utrzymuje tę niezmienność?


Pełne ujawnienie : nie przeczytałem Fast Paxos, dopóki nie zostałem poproszony o odpowiedź na to pytanie; i tylko spojrzał na cytowane strony. Jestem inżynierem, a nie matematykiem; moja praca z Lamportem opiera się wyłącznie na potrzebie prawidłowego wynalezienia i utrzymania dużych systemów rozproszonych.

Moja odpowiedź zależy w dużej mierze od mojego doświadczenia z pracą Lamporta. Przeczytałem kilka protokołów i dowodów Lamport; Profesjonalnie utrzymuję system oparty na paxos; Napisałem i sprawdziłem protokół konsensusu o dużej przepustowości i ponownie profesjonalnie utrzymuję oparty na nim system (staram się, aby moja firma pozwoliła mi opublikować artykuł). I nie współpracował przy nieznacznej papieru z Lamport, w którym spotkałem się z nim trzykroć (papier jest nadal w toku przeglądu).

Michael Deardeuff
źródło
ik=max()CP(v,i)k<j<ij=kCP(v,k)CP(v,k)k=max()k<j<kj=kCP(v,k)kn=0ks. Mam trudności w tłumaczeniu to do silnej indukcji czas płynący do przodu .
hengxin
1
i=0i=1
P18vV,CP(v,i)j<kP18P17vVCP(v,i)
W końcu zdałem sobie sprawę, czym jest niezmiennik i jak działa silna indukcja. Dzięki jeszcze raz. BTW, wspomniałeś o Lamport tends to use another type of hierarchy. He'll prove a simpler algorithm, and then prove that a more complex algorithm maps onto (or "extends") the simpler algorithmtym, czy mógłbyś zatem podać przykład lub zacytować powiązany artykuł? Ponadto, czy wasze artykuły mają wcześniej wydrukowane, (komercyjnie) niesklasyfikowane wydania?
hengxin
1
Lamport wyjaśnia pierwszy typ hierarchii w swoim artykule Jak napisać dowód i podaje przykład drugiego w Bizancjum Paxos poprzez udoskonalenie . Drugi typ hierarchii jest zwykle nazywany udoskonaleniem lub odwzorowaniem .
Michael Deardeuff,