یه باگ ۱۶ ساله تو SQLite که با TLA+ پیدا شد
تستخلاصهٔ کاملتر
نویسندههای این پست، مارکو مانینو و آلبرتو کارترو از تیم دیکوایت کنونیکال، درباره یه نسخه تازه SQLite مینویسن که یه باگ قدیمی رو تو نحوه چکپوینتکردن WAL (لاگ پیشنوشت) رفع کرده -- باگی که میتونه باعث خرابی دیتابیس بشه. نکته جالب این باگ، تأثیر واقعیش تو دنیای واقعی نیست (که خیلی کمه)، بلکه اینه که از سال ۲۰۱۰ یعنی ۱۶ سال تو کد بوده و پیدا کردن و بازتولیدش خیلی سخت بوده.
تو حالت WAL، بهجای نوشتن مستقیم رو فایل اصلی دیتابیس، نوشتهها به انتهای یه فایل جدا به اسم WAL اضافه میشن و خوانندهها تا وقتی داده پایدار نشده، بهش کاری ندارن. هر از گاهی این دادههای WAL به فایل اصلی دیتابیس منتقل میشه که بهش چکپوینت میگن. برای هماهنگی بین نویسندهها، چکپوینتکنندهها و خوانندهها، SQLite از دو تا قفل و چندتا متغیر تو حافظه مشترک استفاده میکنه: mxFrame (طول WAL) و nBackfill (چقدر از WAL تا الان چکپوینت شده).
تیم دیکوایت با TLA+ یه مدل ساده ولی وفادار از این رفتار ساختن: هر صفحه داده رو با یه عدد یکتا نشون دادن، WAL رو یه دنباله از این اعداد و دیتابیس رو یه مجموعه از همون اعداد در نظر گرفتن. دو عملیات اصلی که مدل کردن، append (اضافه کردن به WAL) و checkpoint (انتقال WAL به دیتابیس) بودن؛ هرکدوم بر اساس کد واقعی C توابع walFrames و walCheckpoint تو SQLite طراحی شدن.
با تعریف یه ثابت (invariant) به اسم NoPageIsLost که میگه هیچ صفحهای نباید تو دیتابیس گم بشه، مدلچکر تو فقط ۲۰ حالت تونست یه مثال نقض پیدا کنه که دقیقاً شبیه سناریوی توضیحدادهشده تو مستندات خود SQLite بود -- همین هم مدل رو تأیید میکرد.
برای جواب دادن به سؤال اصلی، تیم یه مدل جدا برای دیکوایت ساختن که تفاوتهاش با SQLite خام رو هم لحاظ میکنه. دیکوایت چون باید نوشتنهاشو با Raft هماهنگ کنه، محدودیت بیشتری رو همزمانی عملیاتها میذاره: چکپوینت دستیِ کاربر رو مسدود میکنه، چکپوینت خودکار رو غیرفعال میکنه و قفلهای بیشتری هم میگیره -- در عمل چکپوینت تو دیکوایت یه عملیات کاملاً توقفکنندهست.
نکات کلیدی:
- SQLite تازه یه باگ ۱۶ ساله تو چکپوینت WAL رو که میتونست باعث خرابی داده بشه رفع کرده
- تیم دیکوایت کنونیکال با TLA+ رفتار WAL و چکپوینت SQLite رو مدل کردن
- مدلچکر تو ۲۰ قدم تونست یه سناریوی گمشدن صفحه دیتابیس رو بازتولید کنه
- دیکوایت بهخاطر هماهنگی با Raft، چکپوینت خودکار رو غیرفعال و چکپوینت دستی رو مسدود میکنه
- تو دیکوایت، چکپوینت عملاً یه عملیات کاملاً توقفکنندهست که همزمانی محدودتری داره
