Pada artikel ini, kami mensimulasikan dan memeriksa protokol komit dua fase menggunakan TLA +.
Protokol komit dua fase praktis dan digunakan saat ini di banyak sistem terdistribusi. Namun demikian, ini agak pendek. Karena itu, kita dapat dengan cepat memodelkannya dan belajar banyak. Faktanya, dengan contoh ini kita akan menggambarkan hasil sistem terdistribusi yang pada
dasarnya tidak mungkin .
Masalah biphase melakukan
Transaksi melewati
manajer sumber daya (RM) . Semua RM harus menyetujui apakah transaksi akan
selesai atau
dibatalkan .
Manajer Transaksi (TM) membuat keputusan akhir:
berkomitmen atau
membatalkan . Kondisi untuk komit adalah kesediaan untuk melakukan semua RM. Kalau tidak, transaksi harus dibatalkan.
Beberapa catatan tentang pemodelan
Untuk mempermudah, kami melakukan simulasi dalam model memori bersama, bukan dalam sistem pesan. Ini juga menyediakan validasi model cepat. Tapi kami akan menambahkan non-atomicity ke tindakan "membaca dari node tetangga dan memperbarui negara" untuk menangkap perilaku menarik saat mengirim pesan.
RM hanya dapat membaca status TM dan membaca / memperbarui kondisinya sendiri. Itu tidak dapat membaca status manajer sumber daya lain. TM dapat membaca status semua node RM dan membaca / memperbarui kondisinya sendiri.
Definisi
Baris 9-10 mengatur
rmState awal untuk setiap RM agar
working , dan TM untuk
init .
Predikat
canCommit true jika semua RM "disiapkan" (siap untuk berkomitmen). Jika RM ada dalam kondisi akhir, maka predikat
canAbort menjadi
canAbort .
Pemodelan TM sederhana. Manajer transaksi memeriksa kemungkinan komit atau pembatalan - dan karenanya memperbarui
tmState .
Ada kemungkinan bahwa TM tidak akan dapat membuat
tmState "tidak dapat diakses", tetapi hanya jika konstanta
TMMAYFAIL disetel ke
true sebelum validasi model dimulai. Dalam label TLA + menentukan tingkat atomisitas, yaitu granularitasnya. Dengan label F1 dan F2 kami menyatakan bahwa operator yang sesuai dilakukan secara nonatomik (setelah waktu yang tidak terbatas) sehubungan dengan operator sebelumnya.
Model RM
Model RM juga sederhana. Karena status “berfungsi” dan “siap” tidak final, RM secara non-deterministik memilih di antara tindakan hingga mencapai kondisi akhir. RM "yang berfungsi" dapat berubah menjadi status "terganggu" atau "siap". "Siap" RM mengharapkan komit / pembatalan dari TM - dan bertindak sesuai itu. Gambar di bawah ini menunjukkan kemungkinan transisi status untuk satu RM. Tetapi perhatikan bahwa kami memiliki beberapa RM, yang masing-masing melewati statusnya dengan kecepatannya sendiri tanpa mengetahui keadaan RM lainnya.
Model komit dua fase
Kita perlu memeriksa konsistensi komit dua fase kita: sehingga tidak ada RM yang berbeda, salah satunya mengatakan "komit" dan yang lainnya "aborsi".
Predikat
Completed memverifikasi bahwa protokol tidak menggantung selamanya: pada akhirnya, setiap RM mencapai kondisi akhir
committed atau
aborted .
Sekarang kita siap untuk menguji model protokol. Awalnya, kami menetapkan
TMMAYFAIL=FALSE, RM=1..3 untuk memulai protokol dengan tiga RM dan satu TM, yaitu, dalam konfigurasi yang dapat diandalkan. Menguji model membutuhkan waktu 15 detik dan mengatakan bahwa tidak ada kesalahan. Baik
Consistency dan
Completed puas dengan kemungkinan eksekusi protokol dengan pergantian tindakan RM dan tindakan TM.
Sekarang atur
TMMAYFAIL=TRUE dan mulai ulang cek. Program ini dengan cepat menghasilkan hasil yang berlawanan, di mana RM macet menunggu jawaban dari TM yang tidak tersedia.
Kita melihat bahwa di
State=4 transisi RM2 terganggu, di
State=7 transisi RM3 terganggu, di
State=8 TM masuk ke keadaan "hang up" dan jatuh ke
State=9 . Di
State=10 sistem membeku karena RM1 tetap selamanya dalam keadaan siap, menunggu keputusan dari TM yang jatuh.
Simulasi BTM
Untuk menghindari pembekuan transaksi, kami menambahkan cadangan TM (BTM), yang dengan cepat mengambil kendali jika TM utama tidak tersedia. BTM menggunakan logika yang sama dengan TM untuk membuat keputusan. Dan untuk kesederhanaan, kami mengasumsikan bahwa BTM tidak pernah crash.
Saat kami menguji model dengan proses BTM yang ditambahkan, kami mendapatkan pesan kesalahan baru.
BTM tidak dapat menerima komit karena kondisi asli kami,
canCommit menyatakan bahwa semua
RMstates harus “disiapkan” dan tidak memperhitungkan kondisi bahwa beberapa RMs telah menerima keputusan komit dari TM asli sebelum TMB mengambil kendali. Penting untuk menulis ulang kondisi
canCommit dengan mempertimbangkan situasi seperti itu.
Sukses! Ketika kami menguji model, kami mencapai konsistensi dan kelengkapan, karena BTM mengambil kendali dan menyelesaikan transaksi jika TM jatuh.
Berikut adalah model 2PCwithBTM di TLA + (BTM dan baris kedua canCommit pada awalnya tidak dikomentari) dan
pdf yang sesuai .
Bagaimana jika RM gagal juga?
Kami berasumsi bahwa RM dapat diandalkan. Sekarang batalkan kondisi ini dan lihat bagaimana protokol berperilaku ketika RM gagal. Tambahkan status "tidak dapat diakses" ke model kegagalan. Untuk menyelidiki perilaku dan mensimulasikan hilangnya ketersediaan secara intermiten, biarkan RM darurat pulih dan terus bekerja dengan membaca statusnya dari log. Berikut adalah diagram transisi status RM lainnya dengan status “tidak dapat diakses” dan transisi ditandai dengan warna merah. Dan di bawah ini adalah model revisi untuk RM.
Hal ini juga diperlukan untuk memperbaiki
canAbort dengan mempertimbangkan kondisi tidak tersedianya. TM dapat membuat keputusan "menutup telepon" jika salah satu layanan dalam keadaan terputus atau tidak dapat diakses. Jika kondisi ini dihilangkan, RM yang jatuh dan tidak dikembalikan akan mengganggu kemajuan transaksi. Tentu saja, sekali lagi, Anda harus mempertimbangkan RM, yang mempelajari keputusan untuk menyelesaikan transaksi dari sumber TM.
Cek model
Saat kami menguji model, ada masalah ketidakkonsistenan! Bagaimana ini bisa terjadi? Kami melacak jejaknya.
Dengan Status
State=6 semua RM dalam keadaan siap, TM membuat keputusan untuk menyelesaikan transaksi, RM1 melihat keputusan ini dan beralih ke label RC, yang berarti kesiapan untuk mengubah statusnya menjadi "selesai". (Ingat RM1, senjata ini akan menembak pada babak terakhir). Sayangnya, TM jatuh di
State=7 , dan RM2 menjadi tidak tersedia di
State=8 . Pada langkah kesembilan, BTM cadangan mengambil kendali dan membaca status tiga RM sebagai "siap, tidak dapat diakses, disiapkan" - dan memutuskan untuk membatalkan transaksi pada langkah kesepuluh. Ingat RM1? Dia memutuskan untuk menyelesaikan transaksi karena dia menerima keputusan seperti itu dari TM asli, dan memasuki negara yang
committed pada langkah 11. Di
State=13 RM3 memenuhi keputusan untuk membatalkan transaksi dari BTM dan memasuki negara yang
aborted - dan sekarang kami telah kehilangan konsistensi dengan RM1.
Dalam hal ini, BTM membuat keputusan yang melanggar
konsistensi . Di sisi lain, jika Anda membuat BTM menunggu RM meninggalkan kondisi tidak dapat diakses, itu dapat membeku selamanya jika terjadi kecelakaan di simpul, dan ini akan melanggar kondisi
pemenuhan (kemajuan).
File model TLA + yang diperbarui tersedia di sini , serta
pdf yang sesuai .
Kemungkinan FLP
Jadi apa yang terjadi? Kami menemukan
teorema Fisher, Lynch, Paterson (FLP) tentang ketidakmungkinan konsensus dalam sistem asinkron dengan kegagalan.
Dalam contoh kami, BTM tidak dapat memutuskan dengan benar apakah RM2 dalam keadaan gagal atau tidak - dan salah memutuskan untuk membatalkan transaksi. Jika hanya TM asli yang membuat keputusan, ketidaktepatan dalam mengenali kegagalan tidak akan menjadi masalah. RM akan mematuhi setiap keputusan TM, sehingga konsistensi dan kemajuan akan dipertahankan.
Masalahnya adalah bahwa kita memiliki dua objek yang membuat keputusan: TM dan BTM, mereka melihat keadaan RM pada waktu yang berbeda dan membuat keputusan yang berbeda. Asimetri informasi semacam itu adalah akar dari semua kejahatan dalam sistem terdistribusi.
Masalahnya tidak hilang bahkan dengan ekspansi ke komit tiga fase.
Berikut ini adalah komit tiga fase yang dimodelkan dalam TLA + (
versi pdf ), dan di bawah ini adalah jejak kesalahan yang menunjukkan bahwa kali ini kemajuan telah dilanggar (pada
halaman Wikipedia tentang komit tiga fase , situasi dijelaskan ketika RM1 membeku setelah menerima keputusan sebelum komit, dan RM2 dan RM3 komit komit, yang melanggar konsistensi).
Paxos sedang mencoba membuat dunia menjadi tempat yang lebih baik.
Tapi tidak semuanya hilang, harapan belum mati.
Kami punya Paxos . Kerjanya rapi dalam kerangka teorema FLP. Inovasi Paxos adalah
selalu aman (bahkan dengan detektor yang tidak akurat, eksekusi tidak sinkron, dan kegagalan), dan
pada akhirnya menyelesaikan transaksi ketika konsensus menjadi mungkin.
Anda bisa meniru TM pada sebuah cluster dengan tiga node Paxos, dan ini akan menyelesaikan masalah inkonsistensi TM / BTM. Atau, seperti yang ditunjukkan Gray dan Lampport dalam
artikel ilmiah tentang konsensus dalam melakukan transaksi , jika RM menggunakan wadah Paxos untuk menyimpan keputusan mereka bersamaan dengan respons TM, ini menghilangkan satu langkah ekstra dalam algoritma protokol standar.