Anda tidak bisa melakukan unit test pada protocol terdistribusi. Unit test menjalankan satu proses di satu mesin dalam satu urutan. Protocol Anda menjalankan sepuluh proses di lima mesin dalam urutan yang tidak Anda kendalikan. Celah antara kedua realitas tersebut adalah tempat bug Anda hidup.

Model checking menutup celah tersebut. Ia mengeksplorasi setiap interleaving yang mungkin dari setiap state yang mungkin dicapai protocol Anda. Jika ada cara agar dua replica tidak setuju, cara agar leader election mengalami deadlock, atau cara agar skenario split-brain muncul, model checker akan menemukannya. Dan itu akan menemukannya sebelum Anda menulis RPC handler pertama.

Mengapa bug terdistribusi bertahan dari pengujian tradisional

State explosion adalah masalahnya. Tiga node yang bertukar pesan dapat menghasilkan miliaran jalur eksekusi. Integration test yang ditulis tangan mungkin hanya mencakup sedikit dari mereka, biasanya happy path dan beberapa failure mode yang jelas. Bug di mana node A crash tepat di antara mengirim prepare dan ack? Semoga beruntung memicu itu di CI.

Verifikasi formal terdengar seperti latihan akademik, tetapi model checking berbeda. Anda tidak membuktikan protocol benar untuk selamanya. Anda mendeskripsikan protocol dalam bahasa spesifikasi, mendefinisikan properti yang Anda pedulikan, dan membiarkan alat mencari ruang state secara eksaustif hingga batas tertentu. Ketika menemukan pelanggaran, ia memberikan Anda trace minimal. Anda mendapatkan resep langkah demi langkah untuk mereproduksi bug. Tidak ada heisenbugs. Tidak ada “berjalan di mesin saya.”

Alat yang paling praktis untuk ini adalah TLA+, yang dikembangkan oleh Leslie Lamport. Ini terlihat seperti matematika karena memang matematika. Tetapi matematikanya lebih sederhana dari yang Anda harapkan, dan payoff-nya adalah menemukan bug yang jika tidak akan muncul pada pukul 2 pagi di production.

Apa yang sebenarnya dilakukan model checking

Sebuah model checker mengambil tiga input: deskripsi sistem Anda, deskripsi lingkungannya, dan properti yang ingin Anda pertahankan. Deskripsi sistem menangkap logika protocol Anda. Deskripsi lingkungan menangkap semua yang tidak Anda kendalikan: delay jaringan, kehilangan pesan, crash node, skew jam. Properti biasanya adalah invariant (“log yang committed tidak pernah ditimpa”) atau kondisi liveness (“setiap request akhirnya mendapat response”).

Checker kemudian menghasilkan setiap state yang dapat dicapai dan setiap transisi valid di antaranya. Ia melakukan ini secara eksaustif untuk ruang state yang finite, atau dengan eksplorasi terbatas untuk yang infinite. Jika sebuah invariant dilanggar, ia berhenti dan melaporkan jalur terpendek ke failure.

Ini adalah brute force, bukan keajaiban. Model checker tidak memahami maksud Anda. Ia hanya mencoba segalanya. Itulah intinya. Integration test Anda bias oleh asumsi Anda. Model checker tidak memiliki asumsi.

Menentukan spesifikasi protocol consensus sederhana dalam TLA+

Mari kita lihat contoh minimal: protocol consensus single-decree di mana leader mengusulkan nilai dan quorum acceptor harus menerimanya sebelum nilai dipilih. Ini adalah ide inti di balik Paxos, Raft, dan setiap algoritma consensus lain yang pernah Anda dengar.

Berikut adalah spec TLA+ untuk sistem tersebut:

------------------------------ MODULE Consensus ------------------------------
EXTENDS Integers, Sequences, FiniteSets

CONSTANTS Values, Acceptors, Quorum

VARIABLES chosen

Init == chosen = {}

Propose(v) ==
  /\\ v \\in Values
  /\\ chosen = {}
  /\\ chosen' = {v}

Next ==
  \\E v \\in Values : Propose(v)

Spec == Init /\\ [][Next]_chosen /\\ WF_chosen(Next)

ChosenUniqueness ==
  Cardinality(chosen) \\leq 1
=============================================================================

Spec ini mengatakan: pada awalnya tidak ada yang dipilih. Sebuah action propose dapat mengatur chosen ke nilai tunggal, tetapi hanya jika belum ada yang dipilih. Invariant ChosenUniqueness menyatakan bahwa paling banyak satu nilai yang dapat dipilih.

Model checker TLA+, TLC, akan memverifikasi bahwa tidak ada execution trace yang melanggar ChosenUniqueness. Jika Anda memperkenalkan bug di mana dua leader dapat mengusulkan secara bersamaan tanpa memeriksa nilai sebelumnya, TLC menemukan counterexample dalam milidetik.

Menambahkan bagian yang berantakan: crash dan kehilangan pesan

Spec di atas terlalu bersih. Sistem terdistribusi nyata tidak bersih. Pesan hilang. Node reboot. Network partition mengisolasi kelompok node satu sama lain. Model baru menjadi berguna ketika Anda memodelkan failure-failure ini.

Berikut adalah fragmen yang lebih realistis yang memodelkan message passing dengan potensi kehilangan:

VARIABLES msgs, acceptorState

Send(m) == msgs' = msgs \\cup {m}

Deliver(m) ==
  /\\ m \\in msgs
  /\\ msgs' = msgs \\ {m}
  /\\ acceptorState' = [acceptorState EXCEPT ![m.to] = @ \\cup {m.value}]

Drop(m) ==
  /\\ m \\in msgs
  /\\ msgs' = msgs \\ {m}
  /\\ UNCHANGED acceptorState

Next ==
  \\E m \\in msgs : Deliver(m) \\/ Drop(m)

Drop adalah tambahan yang penting. Ini memodelkan kehilangan pesan tanpa mengubah acceptor state. TLC akan mengeksplorasi trace di mana pesan apa pun di-deliver, di-drop, atau di-delay tanpa batas. Ketika Anda menambahkan crash dan recovery leader, ruang state tumbuh, tetapi TLC masih mengeksplorasinya secara sistematis.

Ini adalah bagian yang membuat saya bingung ketika pertama kali memulai dengan TLA+. Saya ingin memodelkan hanya logika protocol. Tetapi bug-bug tidak ada di logika. Mereka ada di interaksi antara logika dan failure mode yang belum saya pertimbangkan. Anda harus memodelkan keduanya.

Trade-off: ledakan ruang state dan abstraksi

Model checking tidak gratis. Jumlah state tumbuh secara eksponensial dengan jumlah proses dan ukuran payload pesan Anda. Sebuah spec dengan lima nilai dan tiga acceptor mungkin menghasilkan jutaan state. Tambahkan acceptor keempat dan Anda masuk ke miliaran. Jalankan ini di laptop Anda dan akan kehabisan memori sebelum selesai.

Solusinya adalah abstraksi. Anda tidak memodelkan nilai 64-byte Anda yang sebenarnya. Anda memodelkan dua nilai: V1 dan V2. Jika protocol berperilaku benar untuk dua nilai, nilai spesifik tidak penting. Anda tidak memodelkan log dengan 10.000 entri. Anda memodelkan log dengan kedalaman 2. Jika safety berlaku untuk kedalaman 2, hampir selalu berlaku untuk kedalaman arbitrer. Ini disebut small-model checking, dan merupakan praktik standar di bidang ini.

Keterampilan kuncinya adalah mempelajari detail mana yang penting dan mana yang tidak. Message contents biasanya tidak penting untuk safety properties. Message ordering hampir selalu penting. Node identities mungkin tidak penting, tetapi jumlah node di setiap peran penting.

Jika ruang state masih terlalu besar, Anda memiliki opsi lain. Anda dapat menggunakan symmetry reduction untuk memperlakukan node identik sebagai dapat dipertukarkan. Anda dapat membatasi kedalaman pencarian. Atau Anda dapat beralih ke model checker simbolik seperti Apalache, yang menggunakan SMT solvers untuk bernalar tentang state tanpa menghitung semuanya.

Dari spec ke implementasi: menjaga sinkronisasi

Spec yang terverifikasi tidak ada gunanya jika implementasi Anda menyimpang darinya. Spec adalah blueprint. Kode adalah bangunannya. Tidak ada jembatan otomatis antara keduanya, dan celah itulah tempat bug menyelinap masuk.

Pendekatan praktisnya adalah memperlakukan spec TLA+ sebagai design document yang kebetulan dapat dieksekusi. Tinjau bersama kode selama pull request. Ketika implementasi menangani edge case, tanyakan apakah spec juga menanganinya. Ketika Anda menemukan bug di production, periksa apakah spec akan menangkapnya. Jika tidak, perbarui spec.

Beberapa tim melangkah lebih jauh dan menghasilkan test cases dari counterexamples yang dihasilkan TLC. Sebuah trace TLC yang menunjukkan bagaimana dua replica divergen menjadi skenario integration test. Ini adalah pekerjaan manual, tetapi menghubungkan model formal dengan test suite Anda.

Di Sentry, kami menggunakan pendekatan ini untuk memvalidasi protocol rate limiting terdistribusi. Spec menangkap masalah liveness di mana node yang sedang pulih dapat starve dalam skenario partition tertentu. Integration test kami belum pernah memicunya karena mereka selalu menyembuhkan partition dengan bersih. Model checker tidak peduli dengan yang bersih. Ia mencoba kasus yang berantakan, menemukan bug, dan menyelamatkan kami dari incident yang sangat membingungkan.

Memulai: model check pertama Anda

Jika Anda ingin mencoba ini, mulailah dengan TLA+ Toolbox. Ini adalah IDE gratis untuk menulis dan memeriksa spec. Kerjakan contoh Paxos dan Raft yang disertakan. Mereka lebih kompleks dari cuplikan consensus di atas, tetapi mereka menunjukkan bagaimana protocol nyata dimodelkan.

Untuk spec pertama Anda, pilih sesuatu yang kecil dari sistem Anda sendiri. Sebuah protocol leader election. Skema cache invalidation terdistribusi. Varian two-phase commit. Tulis invariant yang Anda yakini berlaku. Kemudian biarkan TLC memberi tahu Anda apakah Anda benar. Biasanya jawabannya tidak, dan biasanya dalam jam pertama.

Model checking tidak akan menemukan setiap bug. Ini tidak akan membantu dengan performance, tidak akan menangkap serialization mistakes, dan tidak akan memverifikasi bahwa implementasi Anda cocok dengan spec Anda. Apa yang dilakukannya adalah menemukan bug protocol yang mendalam yang terlewat oleh integration test, dan menemukannya pada saat desain, ketika perbaikan tidak memakan biaya.

Itulah perbaikan bug termurah dalam sistem terdistribusi. Bukan debugger yang lebih baik. Bukan monitoring yang lebih banyak. Menangkap bug sebelum kode tersebut sama sekali ada.