Jepsen: PostgreSQL 12.3

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

Báo cáo kiểm thử độc lập (Jepsen làm không nhận tiền), không phải bài của một công ty kể về hệ của mình. Jepsen tự nói: phương pháp thực nghiệm chứng minh được có bug, không chứng minh được không có bug.

Bối cảnh

• Trước 9.1, chế độ "serializable" của PostgreSQL thực ra là snapshot isolation (SI); từ 9.1 (2011) có serializable snapshot isolation (SSI): SI cộng kiểm lúc chạy các "cấu trúc nguy hiểm" (hai cạnh phụ thuộc đọc-ghi kề nhau giữa ba transaction). "Repeatable read" vẫn là SI, nhưng tài liệu không dùng từ đó.
• Jepsen thường kiểm hệ phân tán; lần này áp công cụ lên DB một node.

Thay đổi chính (phương pháp và kết quả)

• Kiểm theo tính chất, không theo kịch bản: sinh transaction ngẫu nhiên gồm append và đọc trên nhiều danh sách (khoá theo phân phối mũ, có khoá chính và khoá phụ không index), ghi lại lịch sử, rồi Elle suy ra đồ thị phụ thuộc giữa transaction và tìm chu trình theo định nghĩa của Adya (G0, G1a/b/c, G-single, G2-item) cùng các lỗi nhất quán nội bộ.
• Read committed: đúng như mong đợi.
• Repeatable read: khớp strong SI, nhưng có rất nhiều chu trình G2-item (khoảng 140 chu trình anti-dependency mỗi phút ở một lần chạy); vi phạm repeatable read theo định nghĩa hình thức, dù có thể hợp lệ theo cách đọc "hẹp" của chuẩn ANSI (vốn mơ hồ).
• Serializable: không serializable. Có G2-item trong vận hành bình thường (6 trường hợp trong 2 phút), trùng đúng ví dụ "write skew" và "batch processing" trong bài báo SSI của PostgreSQL mà SSI sinh ra để chặn; mọi trường hợp đều có xung đột đọc-ghi trên dòng vừa insert. Nguyên nhân (Peter Geoghegan tìm ra): với ba transaction đồng thời, bộ phát hiện xung đột gán nhầm XID của transaction update cho cả phiên bản cũ lẫn mới của tuple. Đoạn code gần như không đổi từ 2011; bug có ở 9.5 tới 13, có lẽ ở mọi phiên bản. Bản vá kèm regression test vào bản phụ 8/2020.
• Vì sao bug sống 9 năm: isolationtester của PostgreSQL, Hermitage, và các test Jepsen trước Elle đều dùng vài transaction khéo dựng với bất biến chứng minh tay; Elle sinh lớp transaction rộng mà vẫn suy được tính chất chặt, nên bắt được thứ không ai nghĩ để thử.
• Khuyến nghị: tài liệu nên gọi repeatable read là SI; ứng dụng dựa vào repeatable read nên chạy transaction nhạy cảm ở serializable, khoá tường minh, hoặc thiết kế lại. Giới hạn: workload chỉ có đọc và append, chưa mô hình hoá predicate nên chỉ phát hiện G2-item, không G2 nói chung.

Vì sao

• Mức cô lập là hợp đồng mà ứng dụng dựa vào nhưng hiếm khi ai kiểm; test bằng ví dụ chọn tay chỉ phủ những bất thường đã biết.

Bài học cho SWE

• Tên mức cô lập trong DB không nói chính xác nó cấm gì; đọc theo định nghĩa hình thức (SI cho phép write skew).
• Kiểm thử theo tính chất trên lịch sử sinh ngẫu nhiên tìm được bug mà bộ test thủ công lâu năm bỏ sót, kể cả ở DB trưởng thành.

Liên quan

• Giao dịch phân tán và nhất quán xuyên service · Kiểm thử độ tin cậy (chaos, fault injection, mô phỏng tất định)
• Dùng Jepsen ở một công ty: Appian 2019 · Appian 2019
• Kiểm serializability bằng đồ thị thứ tự trong hệ tự xây: Dropbox 2018