iddqd, hay kiểu unsafe Rust khó nhất

• iddqd là thư viện map Rust cho phép mượn khóa từ giá trị, được Oxide dùng trong control plane Omicron để duy trì các chỉ mục in-memory cho những bản ghi lớn như inventory của disk và sled, nên tính đúng đắn là yếu tố sống còn
• BTreeMap tiêu chuẩn lưu khóa và giá trị tách rời, khiến việc truyền đi trở nên bất tiện hoặc có thể làm các khóa trùng lặp bị lệch nhau, trong khi IdOrdMap trích xuất khóa từ một trường bên trong bản ghi để tra cứu
• unsafe Rust là lối thoát để biểu đạt các chương trình an toàn mà compiler không thể chứng minh được, và mã generic khi gọi trait implementation do người dùng cung cấp phải chịu được cả những trường hợp safe Rust bệnh hoạn nhất
• mutable iteration của iddqd dựa vào bất biến rằng mọi chỉ mục đều khác nhau để kéo dài lifetime, nhưng một triển khai Ord bệnh hoạn có thể làm B-tree và item set lệch nhau, tạo ra chỉ mục trùng lặp cho cùng một phần tử
• Bản sửa đổi so sánh cả khóa lẫn chỉ mục, và nếu thất bại thì quay về linear scan không gọi mã người dùng; chỉ khi kết hợp Miri, kiểm thử dựa trên mô hình, panic fault injection và rà soát đối kháng bằng LLM mới đạt được mức tin cậy đủ cao

---

Vấn đề mà iddqd giải quyết

• iddqd là thư viện Rust cung cấp map mượn khóa từ giá trị, và Oxide sử dụng nó rộng rãi trong control plane Omicron
• Omicron là phần mềm ở trung tâm rack của Oxide, chịu trách nhiệm provision tài nguyên như compute và storage cũng như giữ cho rack tiếp tục hoạt động; nếu iddqd trục trặc, control plane có thể hoạt động sai theo những cách khó dự đoán và khó chẩn đoán
• Cấu trúc như BTreeMap<Email, User> trong thư viện chuẩn Rust lưu email làm khóa tách riêng khỏi giá trị
• Muốn truyền khóa và giá trị cùng nhau thì phải lấy (email, user) bằng get_key_value; nếu tại thời điểm fetch tạo thêm một struct riêng như UserRecord thì sẽ khó quản lý khi có nhiều kiểu bản ghi
• Nếu sao chép email cả vào bên trong User, sẽ phát sinh rủi ro email trong khóa của map và email trong giá trị khác nhau
• IdOrdMap dùng trait IdOrdItem để trích xuất khóa từ bản ghi, và kiểu khóa có thể được mượn từ giá trị, như type Key<'a> = &'a Email
• Tại Oxide, mẫu này đặc biệt phù hợp với các bản ghi lớn như kết quả truy vấn cơ sở dữ liệu, và hữu ích cho việc lập chỉ mục các bản ghi lớn trên toàn bộ control plane

Tính năng bổ sung

• iddqd hỗ trợ hạng nhất các khóa phức tạp được mượn từ nhiều trường, nên có thể xử lý mà không cần các đường vòng như dynamic dispatch
• BiHashMap và TriHashMap lập chỉ mục mỗi phần tử theo hai hoặc ba khóa riêng biệt, giúp tránh mẫu phổ biến là tự duy trì nhiều map bằng tay
• Phần triển khai Serde tuần tự hóa theo dạng sequence thay vì map, để cả khóa không phải string cũng có thể được tuần tự hóa trong JSON, đồng thời từ chối khóa trùng lặp
• Vì lý do tương thích ngược, dạng tuần tự hóa kiểu map cũng vẫn được hỗ trợ

Điểm khiến unsafe Rust trở nên khó hơn

• Trong Rust, rủi ro cốt lõi là hành vi không xác định (undefined behavior, UB); nếu mã an toàn không thể gây ra UB dưới bất kỳ hình thức nào thì nó là sound, ngược lại là unsound
• Trong safe Rust, compiler sẽ từ chối các chương trình có UB, nhưng do giới hạn của phân tích tĩnh nên nó cũng từ chối luôn một số chương trình thực ra không có UB
• Từ khóa unsafe là lối thoát để biểu đạt các chương trình như vậy; tác giả tự nhận trách nhiệm về soundness và yêu cầu compiler tin tưởng mình
• Các quy tắc Rust mà mã unsafe phải tuân theo gồm: cấm data race, cấm đọc bộ nhớ chưa khởi tạo hoặc đã giải phóng, cấm nhiều alias &mut tới cùng một vùng nhớ, và cấm thay đổi dữ liệu immutable
• Những quy tắc này đặc biệt khó suy luận, nhất là do mutable aliasing, nên thường phải đóng gói unsafe phía sau một abstraction an toàn

Các bước xác minh abstraction an toàn

• split_at_mut là phương thức an toàn để chia một mutable slice thành hai phần, nhưng chỉ dùng safe Rust thì không thể biểu đạt kiểu chia cắt này nên cần unsafe
• Soundness của split_at_mut phụ thuộc vào các bất biến ở phần mã an toàn xung quanh, chẳng hạn có thực sự nhận &mut [T] hay không, có kiểm tra mid <= slice.len() hay không, và có tính đúng phần độ dài còn lại hay không
• get của MyVec<T> phụ thuộc vào việc len là chính xác và chỉ số nằm trong phạm vi; điều kiện này phải được mọi phương thức khác trong cùng module duy trì
• Độ khó đạt mức cao nhất khi mã unsafe generic gọi vào mã do người dùng cung cấp
• Mã safe Rust, dù được viết bệnh hoạn hay mang tính đối kháng đến đâu, cũng không được phép khiến mã unsafe gây ra UB
• Mã như collect_exact tin vào len() của ExactSizeIterator rồi ghi đủ theo capacity thường là unsound, vì nếu iterator trả về độ dài giả thì nó sẽ ghi vào vùng nhớ chưa được cấp phát
• std::io::Read cũng là một trait mà các triển khai lỗi có thể trả sai số byte đã đọc, và Rust RFC 2930 bàn về vấn đề này
• iddqd thuộc đúng nhóm khó nhất này vì nó là cấu trúc dữ liệu generic gọi vào trait implementation do người dùng cung cấp

Cấu trúc bên trong của iddqd

• iddqd kết hợp một ItemSet là danh sách phần tử với một bảng chứa các chỉ mục slot
• IdHashMap<T> sử dụng ItemSet<T> cùng hashbrown::HashTable chứa ItemIndex
• ItemSet<T> có một Vec<ItemSlot<T>>, trong đó ItemSlot<T> là Occupied(T) hoặc Vacant { next: ItemIndex }
• free_head trỏ tới slot Vacant vừa được giải phóng gần nhất, hoặc một sentinel biểu thị không còn free slot; free_head cùng các slot Vacant tạo thành free chain
• Khi chèn phần tử mới, hệ thống kiểm tra free_head để xem có slot tái sử dụng được hay không; nếu có thì ghi đè slot Vacant thành Occupied rồi chuyển free_head sang giá trị kế tiếp
• Nếu không có free slot, nó push một slot Occupied mới vào cuối, sau đó lấy khóa, tính hash và ghi chỉ mục mới vào hash table
• Xóa thì làm ngược lại: tìm chỉ mục theo khóa trong hash table rồi xóa, sau đó đổi ItemSlot tương ứng thành Vacant và nối free_head cũ vào next
• IdOrdMap dùng chỉ mục B-tree thay vì hash table, còn BiHashMap và TriHashMap lần lượt lưu hai và ba hash table

Mutable iteration và kéo dài lifetime

• IdOrdMap::iter_mut duyệt mutable các phần tử theo thứ tự khóa
• Iterator trong Rust yêu cầu giá trị được trả về không được mượn từ chính iterator; các combinator như collect có thể để lại những giá trị như Vec<&mut T> ngay cả sau khi iterator đã biến mất
• Để điều này an toàn, iterator không được trả về cùng một giá trị hai lần
• Borrow checker chỉ thấy việc truy cập tuần tự vào danh sách, chứ không biết rằng mọi chỉ mục đều khác nhau
• iddqd dùng kéo dài lifetime bằng std::mem::transmute::<&mut T, &'a mut T>, và điều này phụ thuộc vào bất biến rằng mọi chỉ mục mà self.iter trả về đều khác nhau

Lỗi do triển khai Ord bệnh hoạn tạo ra

• Trong một IdOrdMap có năm phần tử với khóa từ 0 đến 4 theo thứ tự, nếu tra cứu khóa 0 bằng Entry API thì OccupiedEntry sẽ lưu chỉ mục 0 bên trong
• Sau đó, nếu triển khai Ord của Key bị đổi thành luôn trả về Equal bất kể giá trị, thì khi OccupiedEntry::remove đi lại xuống B-tree, chỉ riêng việc so sánh khóa có thể khiến nó xóa nhầm phần tử
• Ví dụ, nếu B-tree so sánh (key = 2, index = 2) trước, thì do Equal, entry đó sẽ bị xóa; còn vì OccupiedEntry đang giữ chỉ mục 0 nên ở item set, phần tử 0 sẽ bị xóa
• Lúc này B-tree vẫn còn chỉ mục 0, nhưng slot 0 trong item set đã trở thành vacant, còn phần tử 2 vẫn nằm trong item set nhưng mất con trỏ từ B-tree
• Sau đó nếu Ord trở lại hoạt động bình thường và chèn phần tử có khóa 1000, hệ thống sẽ tái sử dụng slot 0 mà free_head đang trỏ tới
• Kết quả là trong B-tree sẽ có các chỉ mục trùng lặp cùng trỏ tới một slot, và IterMut có thể tạo ra nhiều tham chiếu &mut tới cùng một vùng nhớ, dẫn đến unsoundness

Cách sửa và đánh đổi hiệu năng

• Khi đi xuống B-tree, hệ thống được sửa để kiểm tra cả tính bằng nhau của khóa lẫn chỉ mục
• Khi tìm khóa với chỉ mục đã biết, nó so sánh cả (key, index); vì vậy ngay cả khi Ord bệnh hoạn trả về Equal, phép so sánh giữa (key = 2, index = 2) và chỉ mục cần tìm là 0 vẫn thành Less nhờ tie-breaker là chỉ mục
• Để việc tìm kiếm này thành công, chỉ mục được lưu trữ phải thực sự trùng với chỉ mục đang tìm
• Tie-breaker ngăn việc khớp nhầm phần tử, nhưng không đảm bảo luôn tìm được đúng phần tử
• B-tree được sắp theo khóa, còn tie-breaker lại so chỉ mục, nên hai thứ tự này nhìn chung độc lập với nhau
• Nếu tree search thất bại, hệ thống quay về linear scan để xóa chỉ mục đó khỏi B-tree mà không gọi mã người dùng
• Fallback này biến thao tác xóa từ thời gian logarithmic thành linear, nhưng vì nó chỉ xảy ra khi có mã người dùng lỗi nên được xem là đánh đổi chấp nhận được

Các lớp xác minh

• Vì iddqd được dùng như một cấu trúc dữ liệu nền tảng, nó kết hợp rà soát mang tính phân tích với nhiều hình thức xác minh thực nghiệm
• Mọi khối unsafe và mọi mẫu unsafe đều được từ một đến ba tác giả và reviewer Rust phân tích
• Phía trên mỗi khối unsafe đều có chú thích // SAFETY: ghi lại lập luận, và lint undocumented_unsafe_blocks của Clippy kiểm tra sự tồn tại của chú thích này
• Kiểm thử dựa trên ví dụ tạo map, thực hiện thao tác rồi kiểm tra kết quả; iddqd có cả unit test nội bộ lẫn integration test cho API công khai
• Các bài test này cũng tồn tại dưới dạng doctest và kiêm luôn vai trò tài liệu
• Các bài test bệnh hoạn cung cấp Ord lỗi và các trait implementation bất thường khác
• Trong CI, cả test thường lẫn test bệnh hoạn đều được chạy dưới Miri để phát hiện nhiều loại UB
• Các điều kiện như bất biến không được có chỉ mục trùng lặp cũng có thể được kiểm tra trong môi trường test thông thường ngoài Miri

Kiểm thử dựa trên mô hình và fault injection

• iddqd dùng hai lớp randomized testing: model-based testing đối chiếu với oracle đúng, và fault injection đặt bên trên lớp đó
• Model-based testing, hay stateful property-based testing, áp dụng các chuỗi thao tác ngẫu nhiên lên một instance của kiểu dữ liệu rồi so sánh kết quả với một oracle đã biết là đúng
• iddqd chạy các bài test dựa trên mô hình ở quy mô lớn, dựa vào NaiveMap oracle tuy kém hiệu quả nhưng rõ ràng là đúng
• Fault injection là cách đưa lỗi ngẫu nhiên vào mã người dùng; với iddqd, trục đặc biệt hiệu quả là panic safety
• Dù mã người dùng có panic giữa chừng trong thao tác, các bất biến của map vẫn không được phép bị phá vỡ
• Hệ thống gắn một panic countdown ngẫu nhiên vào mỗi thao tác của map, rồi giảm countdown mỗi lần gọi mã người dùng; khi về 0 thì panic, qua đó thực hiện kiểm thử panic safety ngẫu nhiên
• Cách này đã tìm ra nhiều lỗi tinh vi trong iddqd, và một số dẫn thẳng tới unsoundness
• Sau mỗi thao tác, các bài test dựa trên mô hình cũng kiểm tra các bất biến nội bộ như không có duplicate index
• Vì model-based test quá chậm để chạy dưới Miri, các bất biến mà soundness và correctness phụ thuộc vào được kiểm tra riêng

Rà soát đối kháng bằng LLM và kỹ thuật hình thức

• Các mô hình frontier thế hệ hiện tại đã tìm ra nhiều triển khai mã người dùng bệnh hoạn có thể phá hỏng map
• Trong một trường hợp đáng chú ý, LLM đã dựng được một đường đi mà custom allocator panic trong lúc unwind và làm hỏng các bất biến của map
• Đây là một kiểu vấn đề panic safety khác với những panic trong mã người dùng thông thường như triển khai Ord, vốn là thứ mà các bài test panic safety trước đó nhắm tới
• LLM cũng có thể dựng ra các tuyên bố soundness nghe hợp lý nhưng sai, nên red-green TDD dùng Miri làm oracle là hàng rào phòng thủ
• Với bug soundness, trước tiên người ta tạo một bài test thể hiện UB dưới Miri, rồi sau khi sửa thì xác nhận lại rằng chính bài test đó đã vượt qua
• Cách dùng model checker như Kani để chứng minh các bất biến của map gặp trở ngại vì iddqd quá phức tạp, khiến proof cần thiết phình to vượt quá khả năng xử lý của công cụ
• Creusot có thể giúp chứng minh mã Rust không có panic và các lỗi khác, nhưng hiện chưa chứng minh được những bất biến phải được duy trì ngay cả khi mã người dùng panic hoặc hoạt động sai
• NaiveMap đóng vai trò như specification gần nhất của iddqd, và việc CI chạy model-based test hàng nghìn lần đem lại mức tin cậy cao rằng phần triển khai khớp với specification
• cargo-anneal là một công cụ đang được phát triển, cho phép đặt proof soundness bằng Lean vào doc comment cạnh unsafe Rust, và là hướng đi đáng quan tâm
• iddqd có các bất biến rõ ràng và phạm vi tuy hữu hạn nhưng không hề tầm thường, nên là ứng viên benchmark cho các công cụ xác minh hình thức

Kết luận

• unsafe generic Rust cực kỳ khó vì phải duy trì từng bất biến trước các trait implementation tùy ý, kể cả các triển khai mang tính đối kháng
• Lỗi trong iddqd cho thấy một triển khai Ord bệnh hoạn có thể đánh lừa map để tạo mutable alias tới cùng một vùng nhớ
• Không có kỹ thuật đơn lẻ nào bắt được mọi lỗi, nên cần kết hợp suy luận từng dòng unsafe của con người, kiểm thử dựa trên ví dụ, kiểm thử bệnh hoạn, kiểm thử ngẫu nhiên và rà soát đối kháng bằng mô hình frontier
• Oxide cho rằng mức độ nghiêm ngặt này là xứng đáng đối với hạ tầng nền tảng

[GN⁺]

Ý kiến trên Lobste.rs

• Nếu tôi hiểu đúng (đang di chuyển nên đọc trên điện thoại), có vẻ chuyện này có thể giải quyết bằng kiểu bao bọc và dùng HashSet/BTreeSet thay cho HashMap/BTreeMap
  Kiểu bao bọc không hẳn là bắt buộc, nhưng xét về độ an toàn và khả năng bảo trì về sau thì đó là một lựa chọn tốt
  Thứ cần thiết chỉ là một wrapper kích thước 0 bọc quanh đối tượng, rồi thêm phần cài đặt PartialEq/Hash tùy chỉnh chỉ xem các trường cần quan tâm. Để tra cứu mà không phải tạo toàn bộ giá trị, có thể tạo một kiểu thứ hai triển khai AsRef cho kiểu giá trị
  Cách này là phương pháp tái sử dụng nguyên giao diện HashSet/BTreeSet hiện có mà không cần unsafe. Thay vì bọc kiểu giá trị/khóa, cũng có thể tạo một wrapper HashSet/BTreeSet mới để đảm nhiệm hành vi này

  • Ở đây, khóa là tổ hợp tùy ý của các trường và trường con trong kiểu bản ghi, và được biểu diễn bằng GAT. Ngoài ra, mẫu chỉ mục số nguyên/slab cũng được tổng quát hóa tự nhiên thành map đa chỉ mục
    Nó cũng có cả API Entry, truy cập/lặp có thể thay đổi. Trong iddqd, tính khả biến được xử lý khá cẩn thận, và ở một vài chỗ người ta dùng giá trị nguyên tử để cho phép khả biến nội tại. Việc này hẳn sẽ khá khó nếu không có tham chiếu gián tiếp qua chỉ mục

• Nếu cần kiểm chứng hình thức iddqd, lúc đầu tôi có lẽ sẽ thử dùng trình kiểm tra mô hình như Kani để chứng minh rằng map không phá vỡ các bất biến nội bộ. Nhưng tôi tò mò về đoạn nói rằng iddqd hơi phức tạp đối với khả năng của Kani, và chứng minh cần thiết trở nên quá lớn để công cụ xử lý
  Bạn có thể chia sẻ chi tiết hơn về phần này không? Tôi muốn biết liệu điều đó có nghĩa là độ phức tạp tính toán của thuật toán bị suy biến về trường hợp xấu nhất hay không
  Nhìn chung đây là một nghiên cứu tình huống thú vị về các phương pháp hình thức, và tôi rất vui vì bạn đã đề cập đến phần này. Khi nhìn vào các ví dụ thành công của công cụ kiểm chứng hình thức hiện có trong những dự án lớn, người ta có thể ngây thơ nghĩ rằng ít nhất cũng chứng minh được tính đúng đắn của cấu trúc dữ liệu; nhưng thực tế cho thấy độ khó khác nhau tùy từng cấu trúc dữ liệu, và ngay cả trong những ngôn ngữ được cho là thuận lợi hơn cho việc chứng minh so với các ngôn ngữ như Rust vốn cho phép aliasing không giới hạn, điều đó trong thực tế cũng không hề dễ
  Hơi lạc đề một chút, nhưng tôi cũng tò mò là các sơ đồ được làm như thế nào. Có phải bạn viết một script dùng một lần không, vì trông chúng giống đồ được làm riêng để khớp với thiết kế blog/trang web của Oxide hơn là một công cụ dùng chung

  • Ở cuối bài có ghi “Diagrams courtesy Ben Leonard.”, và Ben Leonard là nhà thiết kế của Oxide. Nên có vẻ khá có khả năng đó là sơ đồ làm thủ công
  • Ngay cả khi nhắm đến việc chứng minh thứ rất cơ bản trên một cài đặt trait cụ thể và hoạt động tốt, CBMC vẫn chạy CPU và hơn 10 phút sau cũng chưa xong
    Tôi cũng đã thử thu hẹp phạm vi. Ví dụ, tôi giả định hashbrown là đúng, nhưng như vậy cũng không tiến triển được bao nhiêu. Đến lúc đó thì tôi gần như bỏ cuộc. Với các cài đặt trait hoạt động tốt, tôi khá tin rằng iddqd là đúng, còn điều tôi thật sự quan tâm trong phương pháp hình thức là một chứng minh vẫn đúng ngay cả với những cài đặt tùy ý, hoạt động sai
    Tuy vậy tôi không phải là người dùng Kani giỏi nhất. Sẽ rất tuyệt nếu bạn hoặc ai đó khác thử làm chuyện này
    Các sơ đồ ban đầu được phác thảo bằng Mermaid, sau đó nhà thiết kế tuyệt vời Ben Leonard đã chỉnh tay chúng thành các sơ đồ phù hợp với bảng màu và chủ đề của chúng tôi

• Mẫu map dựa trên trường để đánh chỉ mục đối tượng bằng một trong các trường của chính nó là thứ tôi luôn ước có thể dùng được trong C#
  Trước đây tôi từng thử tự làm một phiên bản đơn giản, nhưng giao diện không thật sự gọn gàng nên đã bỏ dở. Bài viết này khiến tôi muốn thử lại một lần nữa

  • Đúng vậy, đây là một mẫu cực kỳ hữu ích. Tôi làm ra nó vì công việc cần, nhưng về sau lại dùng nó ở khắp nơi, từ các codebase production như cargo-nextest cho đến các dự án cá nhân
    Dùng một trường duy nhất làm khóa đúng là trường hợp phổ biến nhất, nhưng iddqd đủ linh hoạt để dùng bất kỳ tổ hợp nào của trường, trường con, hoặc hàm thuần và rẻ có thể tính từ các trường. Ví dụ, hãy tìm ArtifactKey tại https://docs.rs/iddqd/latest/iddqd/ (xin thông cảm nếu bạn không quen cú pháp Rust)
    Khi thiết kế iddqd, tôi rất muốn người dùng có thể tận dụng toàn bộ sức mạnh của hệ thống kiểu Rust. Bất kể tôi, với tư cách tác giả thư viện, phải đi bao nhiêu đường vòng. Tôi thực sự muốn iddqd trở thành một thư viện mang lại niềm vui cho người dùng, đặc biệt là các đồng nghiệp của tôi