‏تو هر پیاده‌سازی Raft که تست شد، باگ پیدا شد

تیم Antithesis تو گزارشی که منتشر کرده می‌گه تو هر پیاده‌سازی‌ای از Raft که تست کرده باگ پیدا شده — از HashiCorp Raft و Aeron Cluster گرفته تا OpenRaft و MicroRaft. باگ‌ها هم از نوع کم‌اهمیت نیستن: تضمین اصلی Raft یعنی state machine safety (همون تحویل دستورها با ترتیب یکسان به همهٔ replicaها) نقض می‌شه، یعنی نودها سر محتوای لاگ با هم اختلاف پیدا می‌کنن. نویسنده‌ها تأکید می‌کنن این نقد Raft یا پیاده‌سازها نیست؛ نوشتن Raft درست، حتی با spec و راهنما، سخته.

روش تستشون به‌طرز عجیبی ساده‌ست: یه کلاستر سه‌نودی Raft با workloadی به اسم Chain of Blocks که فقط بایت‌های هر دستور رو هش می‌کنه و بعد از هر دستور، تعداد دستورهای اعمال‌شده و هش فعلی رو نگه می‌داره. اگه هش دو نود بعد از تعداد دستور یکسان فرق کنه، یعنی state واگرا شده. به گفتهٔ نویسنده‌ها یه مهندس جونیور می‌تونه این تست رو تو کمتر از یه روز بنویسه؛ چیزی که فرق می‌کنه اینه که سیستم تو یه محیط شبیه‌سازی قطعی و زیر تزریق خطای تهاجمی اجرا می‌شه. حتی فقط پارتیشن شبکه برای دیدن واگرایی کافی بوده.

جدی‌ترین باگی که تو HashiCorp Raft پیدا شده از یه بهینه‌سازی میاد که عمداً از پروتکل فاصله گرفته: پیام‌های heartbeat به‌جای اینکه برای حلقهٔ اصلی صف بشن، همون‌جا روی ترد شبکه پردازش می‌شن. مشکل اینه که همون heartbeat می‌تونه currentTerm رو بالا ببره و نود رو follower کنه، و این تغییر وضعیت هم‌زمان با ترد اصلی یه race condition می‌سازه. نتیجه‌ش می‌تونه ساخته شدن یه ورودی لاگ با term اشتباه و در نهایت واگرایی state machineها باشه، یا حتی دو رأی تو یک term و انتخاب دو رهبر هم‌زمان.

دوتا باگ دیگه از جنس liveness هستن. یکی deadlock موقع leadership transfer: اگه رهبر وسط انتقال رهبری به دلیل دیگه‌ای کنار بره، گوروتین انتقال برای همیشه بلاک می‌مونه و فلگ «انتقال رهبری در جریانه» پاک نمی‌شه؛ همون نود بعداً می‌تونه دوباره رهبر بشه ولی هیچ درخواستی رو قبول نمی‌کنه تا وقتی ری‌استارت بشه. باگ سوم یه livelock موقع InstallSnapshot هست: پیاده‌سازی برخلاف قانون ۷ مقالهٔ Raft لاگ قبلی رو دور نمی‌ندازه، پس AppendEntries بعدی رد می‌شه، رهبر دوباره snapshot می‌فرسته و این چرخه تموم نمی‌شه.

جمع‌بندی نویسنده‌ها اینه که روش‌های فرمال به‌تنهایی کافی نیستن، چون چیزی که اثبات می‌شه مدله نه کد. اونا چند فرض ضمنی مقالهٔ Raft رو هم لیست کردن که پیاده‌ساز راحت ازشون رد می‌شه: اینکه هر نود یه پروسهٔ همگام با تغییر وضعیت اتمیکه، اینکه هر پاسخ به درخواست خودش نگاشت می‌شه، و اینکه currentTerm و votedFor باید با هم و اتمیک ذخیره بشن. ضمناً spec رسمی TLA+ اصلاً InstallSnapshot و leadership transfer رو پوشش نمی‌ده.

نکات کلیدی:

• تو همهٔ پیاده‌سازی‌های Raft که تست شدن، باگ ناقض state machine safety پیدا شده
• تست با یه workload خیلی ساده روی کلاستر سه‌نودی و زیر تزریق خطا انجام شده
• جدی‌ترین باگ HashiCorp Raft از پردازش ناهمگام heartbeat روی ترد شبکه میاد
• دو باگ liveness دیگه: deadlock تو leadership transfer و livelock تو InstallSnapshot
• درس اصلی: اثبات فرمال درستی مدل رو تضمین می‌کنه، نه درستی پیاده‌سازی