Raft Simulator

Simulator konsensus Raft

Cara simulator ini dibuat

Sebuah simulator Raft yang bisa dirusak dengan sengaja — dan rekayasa yang membuat kerusakan itu bisa dipercaya.

Simulator Raft yang bisa Anda rusak dengan sengaja. Simulasi diskret deterministik, pemeriksaan invariant keamanan yang berjalan terus, dan mode ablasi yang mematikan satu per satu aturan Raft supaya jaminan yang dijaganya benar-benar terlihat gagal.

Kode sumber di GitHub ↗Simulator

  1. Fungsi murni, diputar ulang persis

    Simulasi adalah fungsi murni dari (config, seed, actions, flags). Jam virtual, PRNG ber-seed, dan tiebreak eksplisit untuk timestamp yang sama membuat setiap trace identik byte demi byte di mesin mana pun. Dari situlah datang time travel, tautan yang bisa dibagikan, dan laporan bug yang bisa direproduksi.

    lib/sim

  2. Figure 2, diimplementasikan secara harfiah

    Setiap aturan di lib/raft menyebutkan figure dan rule yang diimplementasikannya. Setiap rule punya fixture kesesuaian, ditambah suite untuk Figure 8, Figure 13, dan §6. Raft mudah dibuat hampir benar, dan hampir benar itu salah.

    lib/raft

  3. Checker yang tidak berbagi kode

    lib/invariants mengevaluasi lima properti keamanan dari definisinya atas state global, dan tidak mengimpor apa pun dari algoritma selain tipe. Checker yang memakai asumsi implementasinya sendiri akan memvalidasi bug-nya sendiri.

    lib/invariants

  4. Ablasi yang tidak bisa berbohong

    Ketujuh aturan adalah guard bernama di satu tempat, masing-masing dikonsultasikan di tepat satu call site. Setiap sakelar punya tes yang membuktikan propertinya gagal saat dimatikan dan bertahan saat dinyalakan — dua arah.

    lib/raft/rules.ts

  5. Di-fuzz sebelum setiap deploy

    Kelima properti bertahan di 10.000 run acak di bawah Raft yang tidak diubah, dengan log compaction dan perubahan keanggotaan aktif. Suite itu menjaga setiap deploy; seed yang gagal menjadi tes regresi permanen.

    tests/fuzz

Karya terdahulu dan sumber

Karya terdahulu

RaftScope sudah ada, kualitasnya bagus, dan ditulis oleh penulis makalah Raft sendiri. Ia adalah visualiser Raft yang kanonis — kalau Anda ingin melihat Raft berjalan, mulailah dari sana. The Secret Lives of Data juga penjelasan yang baik.

RaftScope ↗

Yang ditambahkan proyek ini

Bukan pengganti keduanya. Kontribusinya sempit: ablasi dan pemeriksaan invariant. RaftScope menunjukkan mekanismenya; di sini Anda mematikan sebuah aturan lalu menonton properti keamanan yang dijaganya runtuh, sementara lima indikator invariant menyebutkan mana yang gagal dan mengapa.

Sumber normatif

Ongaro & Ousterhout, In Search of an Understandable Consensus Algorithm (USENIX ATC 2014), versi extended — terutama Figure 2. Setiap aturan di lib/raft menyebutkan nomor figure dan rule yang diimplementasikannya.

raft.pdf ↗