Protocol-Aware Deterministic Simulation Testing

TigerBeetle · 2026 · 3. Quy mô lớn · Độ khó: Khó — bài gốc

Bài nhà cung cấp; mọi nhận định ghi "theo TigerBeetle".

Bối cảnh

• TigerBeetle dùng Viewstamped Replication (VSR): liveness là còn phản hồi khi đa số replica sống; safety là các replica thống nhất thứ tự (dẫn tới strict serializability).
• Năm 2025 họ đã qua Jepsen (kiểm tra từ ngoài vào qua API, sinh input ngẫu nhiên, tiêm lỗi): không thấy vi phạm strict serializability. Theo TigerBeetle, kiểm tra từ ngoài vào (Jepsen, hay hypervisor tất định kiểu Antithesis) không thấy được bất biến nằm dưới ranh giới API; với hạ tầng nền tảng phải kiểm thêm từ trong ra.

Thay đổi chính

• Tất định cả logic lẫn vật lý: như FoundationDB, code DB tất định và tránh đa luồng ở control plane; thêm nữa các replica hội tụ về trạng thái giống nhau từng byte. Nhờ đó chạy được code đồng thuận và storage thật trong simulator VOPR: mạng, đĩa, thời gian đều giả lập; cả cụm chạy trong một process, thời gian tăng tốc nhiều bậc; sinh ngẫu nhiên phân vùng mạng, hỏng đĩa, crash replica khi client đang ghi; lỗi tìm được thì tái hiện y hệt.
• Bất biến an toàn sâu: ở production, assertion bật sẵn và crash replica khi phát hiện vi phạm (hạ vi phạm an toàn thành mất khả dụng), nhưng chỉ kiểm được rẻ (WAL so khi nhận commit, checkpoint_id của LSM). Trong simulator thì kiểm đắt hơn: mọi request đã commit có checksum khớp giữa mọi replica; cấu trúc manifest LSM khớp hoàn toàn; checksum dữ liệu thật (superblock, grid, phản hồi client) để khẳng định giống nhau từng byte.
• Liveness theo từng replica: đa số sống có thể che giấu replica bị kẹt. Kiểm: replica không hỏng đầu WAL thì không bao giờ phải nhờ cụm để khôi phục (nếu không, cả cụm cùng khởi động lại có thể kẹt); khi mỗi replica thiếu 6/9 block nhưng gộp lại vẫn đủ, mỗi replica phải tự sửa bằng cách lấy đúng các block thiếu từ replica khác (nhờ tất định vật lý), thay vì chép toàn bộ trạng thái như phần lớn giao thức đồng thuận.
• Cũng dùng simulator để hỏi "nếu… thì sao" bằng vài chục dòng code và đo tối ưu giao thức không bị nhiễu phần cứng.

Bài học cho SWE

• Thiết kế cho tính tất định từ đầu là điều kiện để mô phỏng chạy code thật; khó thêm vào sau.
• Kiểm hệ phân tán ở hai tầng: hành vi nhìn từ client và bất biến bên trong từng node.
• Assertion bật ở production biến lỗi im lặng (dữ liệu sai) thành lỗi ồn (node chết), dễ phát hiện và rẻ hơn.

Liên quan

• TigerBeetle 2024 · TigerBeetle 2026 · DoorDash 2022
• Kiểm thử độ tin cậy (chaos, fault injection, mô phỏng tất định) · Failover, replica và dự phòng dữ liệu