Bukti kebenaran Paxos klasik dan Fast Paxos

Saya membaca kertas "Fast Paxos" oleh Leslie Lamport dan terjebak dengan bukti kebenaran dari Paxos klasik dan Fast Paxos.

Untuk konsistensi, nilai $v$ dipilih oleh koordinator dalam fase $2a$ di babak $i$ harus memuaskan

$CP(v,i):$ Untuk setiap ronde$j < i$ , tidak ada nilai selain$v$ telah atau mungkin belum dipilih dalam bulat$j$ .

Untuk Paxos klasik , buktinya (Halaman 8) dibagi menjadi tiga kasus: $k < j < i$ , $j = k$ , dan $j < k$ , di mana $k$ adalah angka bulat terbesar di mana beberapa akseptor telah melaporkan kepada koordinator dengan fase $1b$ pesan. Saya gagal memahami argumen untuk kasus ketiga:

Kasing $j < k$ . Kita dapat berasumsi dengan induksi bahwa properti $CP$ diadakan ketika akseptor $a_0$ sebagai untuk $v$ di putaran $k$ . Ini menyiratkan bahwa tidak ada nilai selain $v$ telah atau mungkin belum dipilih di babak $j$ .

Pertanyaanku adalah:

1. Mengapa kita dapat mengasumsikan bahwa properti $CP$ diadakan ketika akseptor $a_0$ sebagai untuk $v$ di putaran $k$ ?

Tampaknya kita menggunakan induksi matematika, oleh karena itu, apa dasar, hipotesis induktif, dan langkah-langkah induktif?

Untuk Fast Paxos , argumen yang sama (Halaman 18) berlanjut. Ia mengatakan,

Kasing . Untuk setiap v dalam V , tidak ada nilai selain v telah atau mungkin belum dipilih dalam r bulat j .$j < k$$v$$V$$v$$j$

Pertanyaanku adalah:

2. Bagaimana ini diperoleh? Secara khusus, mengapa "Untuk dalam V " di sini?$v$$V$

Menurut pendapat saya, bukti kebenaran dari kasus bergantung (secara rekursif) pada kasus-kasus k < j < i dan j = k . $j < k$$k < j < i$$j = k$

Oleh karena itu, bagaimana kita bisa menyimpulkan case tanpa terlebih dahulu membuktikan j = k sepenuhnya (yaitu, melewatkan subkotak j = k di mana V berisi lebih dari satu nilai)?$j < k$$j = k$$j = k$$V$

Mengapa kita dapat mengasumsikan bahwa properti CP diadakan ketika akseptor a0 memilih v di babak k? Tampaknya kita menggunakan induksi matematika, oleh karena itu, apa dasar, hipotesis induktif, dan langkah-langkah induktif?

Anda sedang melihat contoh induksi yang kuat . Dalam induksi sederhana, Anda menganggap properti tahan untuk dan membuktikannya berlaku untuk n = m + 1 . Dalam induksi yang kuat Anda mengasumsikan properti berlaku untuk ∀ n : n < m dan membuktikannya berlaku untuk n = m + 1 .$n=m$$n=m+1$$\forall n: n<m$$n=m+1$

Dasar (saya percaya): . Yaitu, putaran nol (sejak putaran dimulai dari 1). Ini sepele benar, yang mungkin mengapa tidak dinyatakan secara eksplisit.$j = 0$

Langkah induktif : Asumsikan ; buktikan C P ( v ; j + 1 ) di mana j < i .$\forall n, n \le j : CP(v; n)$$CP(v; j+1)$$j < i$

Percaya atau tidak, ini hanya sketsa bukti . Bukti nyata ada di kertas Paruh Waktu Parlemen . (Beberapa menganggap kertas itu samar, yang lain menganggapnya lucu.)

Bagaimana ini diperoleh?

Menurut pendapat saya, bukti kebenaran dari kasus bergantung (secara rekursif) pada kasus-kasus k < j < i dan j = k .$j<k$$k<j<i$$j=k$

Oleh karena itu, bagaimana kita bisa menyimpulkan case tanpa terlebih dahulu membuktikan j = k sepenuhnya (yaitu, melewatkan subkotak j = k di mana V berisi lebih dari satu nilai)?$j<k$$j=k$$j=k$$V$

Lagi-lagi ini adalah induksi yang kuat, jadi case tidak bergantung pada case k < j dan j = k , tetapi melalui hipotesis induksi , yaitu dari putaran Paxos sebelumnya.$j<k$$k<j$$j=k$

Kiat umum untuk bukti Lamport.

Lamport menggunakan teknik bukti hierarkis. Sebagai contoh, struktur buktinya pada halaman 7-8 terlihat seperti ini:

• Asumsikan ; buktikan C P ( v ; j + 1 ) di mana j < i . $\forall n, n \le j : CP(v; n)$$CP(v; j+1)$$j < i$
  1. Pengamatan 1
  2. Pengamatan 2
  3. Pengamatan 3
  4. $k = argmax (...)$
  5. huruf k = 0
  6. huruf k> 0
     • huruf k <j
     • case k = j
     • huruf j <k

Lamport cenderung menggunakan jenis hierarki lain. Dia akan membuktikan algoritma yang lebih sederhana, dan kemudian membuktikan bahwa algoritma yang lebih kompleks memetakan ke (atau "meluas" ) algoritma yang lebih sederhana. Ini sepertinya tidak terjadi pada halaman 18, tetapi ini sesuatu yang harus diwaspadai. (Bukti pada halaman 18 tampaknya merupakan modifikasi dari bukti a halaman 7-8; bukan perpanjangan dari itu.)

Lamport sangat bergantung pada induksi yang kuat ; dia juga cenderung berpikir dalam hal set bukannya angka. Jadi, Anda mungkin mendapatkan set kosong di mana orang lain akan memiliki nol atau nol; atau mengatur serikat di mana orang lain akan memiliki tambahan.

Membuktikan kebenaran dari sistem penyampaian pesan yang tidak sinkron membutuhkan pandangan yang maha tahu dari sistem sehubungan dengan waktu . Sebagai contoh, ketika mempertimbangkan tindakan di putaran , perlu diingat bahwa tindakan untuk beberapa putaran j < i mungkin tidak terjadi temporal! . Namun Lamport menyatakan peristiwa yang berpotensi terjadi di masa mendatang dalam bentuk lampau.$i$$j < i$

Sistem dan bukti Lamport cenderung memiliki variabel atau serangkaian variabel yang hanya diizinkan untuk menuju satu arah; hanya menambah angka dan hanya menambah set. Ini digunakan secara luas dalam buktinya. Sebagai contoh, pada halaman 8 Lamport menunjukkan bagaimana ia dikebiri kemampuan masa depan memberikan suara lain:$a$

... Karena mengatur kepada saya setelah mengirim pesan, maka tidak dapat memberikan suara dalam putaran apa pun yang jumlahnya kurang dari saya ....$rnd[a]$$i$$a$$i$

Jelas merupakan peregangan otak untuk membuktikan sistem semacam ini.

(perbarui) : Sebutkan invarian; Lamport menggunakan banyak invarian ketika berkembang dan buktinya. Terkadang mereka tersebar di seluruh bukti; kadang-kadang mereka hanya hadir dalam bukti yang diperiksa mesin. Alasan tentang setiap invarian; kenapa ada disana Bagaimana cara berinteraksi dengan invarian lain? Bagaimana setiap langkah dalam sistem menjaga invarian ini?

Pengungkapan penuh : Saya belum membaca Fast Paxos sampai saya diminta untuk menjawab pertanyaan ini; dan hanya melihat halaman yang dikutip. Saya seorang insinyur dan bukan ahli matematika; sikat saya dengan karya Lamport semata-mata didasarkan pada kebutuhan untuk menemukan dan memelihara sistem distribusi skala besar dengan benar.

Jawaban saya sangat bergantung pada pengalaman saya dengan pekerjaan Lamport. Saya telah membaca beberapa protokol dan bukti Lamport; Saya secara profesional memelihara sistem berbasis paxos; Saya telah menulis dan membuktikan protokol konsensus throughput tinggi, dan sekali lagi secara profesional mempertahankan sistem berdasarkan itu (saya mencoba untuk membuat perusahaan saya mengizinkan saya untuk menerbitkan sebuah makalah). Saya telah berkolaborasi pada makalah yang tidak penting dengan Lamport, di mana saya bertemu dengannya tiga kali (makalah ini masih menunggu tinjauan sejawat.)