iddqd, atau jenis unsafe Rust yang paling sulit

• iddqd adalah pustaka map Rust yang meminjam kunci dari nilai, dan dipakai untuk mempertahankan indeks in-memory dari record besar seperti inventaris disk dan sled di control plane Omicron milik Oxide, sehingga ketepatan sangat penting
• BTreeMap standar menyimpan kunci dan nilai secara terpisah sehingga alur pemindahan data jadi merepotkan atau kunci duplikat bisa saling tidak cocok, tetapi IdOrdMap melakukan lookup dengan mengekstrak kunci dari field di dalam record
• unsafe Rust adalah jalur keluar untuk mengekspresikan program aman yang tidak bisa dibuktikan oleh kompiler, dan kode generik harus tahan bahkan terhadap safe Rust yang patologis saat memanggil implementasi trait yang disediakan pengguna
• Iterasi mutable pada iddqd memperpanjang lifetime dengan bergantung pada invariant bahwa semua indeks berbeda, tetapi implementasi Ord yang patologis dapat membuat B-tree dan item set tidak sinkron sehingga indeks duplikat untuk item yang sama bisa tercipta
• Perbaikannya membandingkan kunci dan indeks sekaligus, lalu jika gagal kembali ke pemindaian linear yang tidak memanggil kode pengguna, dan kepercayaan yang memadai hanya bisa didapat dengan menggabungkan Miri, pengujian berbasis model, panic fault injection, dan review adversarial oleh LLM

---

Masalah yang diselesaikan iddqd

• iddqd adalah pustaka Rust yang menyediakan map dengan kunci yang dipinjam dari nilai, dan Oxide menggunakannya secara luas di control plane Omicron
• Omicron adalah perangkat lunak di pusat rack Oxide yang memprovisikan resource seperti compute dan storage serta menjaga rack tetap berjalan, dan jika iddqd salah berfungsi, control plane bisa berperilaku salah dengan cara yang sulit diprediksi dan didiagnosis
• Struktur seperti BTreeMap<Email, User> di pustaka standar Rust menyimpan email sebagai kunci secara terpisah dari nilainya
• Untuk mengoper kunci dan nilai bersama, kita harus mengambil (email, user) dengan get_key_value, dan jika membuat struktur terpisah seperti UserRecord saat fetch, pengelolaannya menjadi sulit ketika tipe record banyak
• Jika email juga diduplikasi di dalam User, muncul risiko email pada kunci map dan email di dalam nilai saling berbeda
• IdOrdMap menggunakan trait IdOrdItem untuk mengekstrak kunci dari record, dan tipe kunci bisa dipinjam dari nilai seperti type Key<'a> = &'a Email
• Di Oxide, pola ini cocok untuk record besar seperti hasil query database, dan berguna untuk pengindeksan record besar di seluruh control plane

Fitur tambahan

• iddqd mendukung sebagai fitur kelas satu kunci kompleks yang dipinjam dari beberapa field, sehingga bisa ditangani tanpa jalan memutar seperti dynamic dispatch
• BiHashMap dan TriHashMap masing-masing mengindeks satu item dengan dua atau tiga kunci, sehingga tidak perlu memakai pola umum berupa memelihara beberapa map secara manual
• Implementasi Serde melakukan serialisasi sebagai sequence, bukan map, sehingga kunci non-string juga bisa diserialisasi dalam JSON, serta menolak kunci duplikat
• Demi kompatibilitas ke belakang, serialisasi dalam bentuk map juga didukung

Titik ketika unsafe Rust menjadi sulit

• Dalam Rust, risiko intinya adalah undefined behavior (UB); jika kode aman tidak mungkin menimbulkan UB dengan cara apa pun maka ia sound, jika tidak maka unsound
• Di dalam safe Rust, kompiler menolak program yang memiliki UB, tetapi karena keterbatasan analisis statis, sebagian program yang sebenarnya bebas UB juga ikut ditolak
• Kata kunci unsafe adalah jalur keluar untuk mengekspresikan program semacam itu, dengan penulis mengambil tanggung jawab atas soundness dan meminta kompiler untuk mempercayainya
• Aturan Rust yang harus dipatuhi kode unsafe mencakup larangan data race, larangan membaca memori yang belum diinisialisasi atau sudah dibebaskan, larangan beberapa alias &mut pada area memori yang sama, dan larangan memodifikasi data immutable
• Aturan ini sulit ditalar, terutama karena mutable aliasing, sehingga biasanya perlu mengenkapsulasi unsafe di balik abstraksi aman

Tahapan memverifikasi abstraksi aman

• split_at_mut adalah metode aman untuk membagi mutable slice menjadi dua bagian, tetapi pembagian seperti ini tidak bisa diekspresikan hanya dengan safe Rust sehingga membutuhkan unsafe
• Soundness split_at_mut bergantung pada invariant di kode aman sekitarnya, seperti apakah ia menerima &mut [T], apakah mid <= slice.len() sudah diperiksa, dan apakah panjang sisanya dihitung dengan tepat
• get pada MyVec<T> bergantung pada kondisi bahwa len akurat dan indeks masih dalam batas, dan kondisi ini harus dijaga oleh semua metode lain dalam modul yang sama
• Tingkat kesulitan paling tinggi muncul ketika kode unsafe generik memanggil kode yang disediakan pengguna
• Kode safe Rust, betapapun patologis atau adversarial cara penulisannya, tidak boleh membuat kode unsafe menimbulkan UB
• Kode seperti collect_exact yang mempercayai len() dari ExactSizeIterator dan menulis sebanyak capacity umumnya unsound, karena jika iterator mengembalikan panjang palsu, ia bisa menulis ke memori yang tidak dialokasikan
• std::io::Read juga merupakan trait yang implementasinya bisa buggy dan salah melaporkan jumlah byte yang dibaca, dan Rust RFC 2930 membahas masalah ini
• iddqd termasuk dalam kategori tersulit ini karena merupakan struktur data generik yang memanggil implementasi trait yang disediakan pengguna

Struktur internal iddqd

• iddqd menggabungkan ItemSet, yaitu daftar item, dengan tabel yang menyimpan indeks slot
• IdHashMap<T> menggunakan ItemSet<T> dan hashbrown::HashTable yang menyimpan ItemIndex
• ItemSet<T> memiliki Vec<ItemSlot<T>>, dan ItemSlot<T> berbentuk Occupied(T) atau Vacant { next: ItemIndex }
• free_head menunjuk ke slot Vacant yang paling baru dibebaskan atau ke sentinel yang berarti tidak ada free slot, dan free_head bersama slot-slot Vacant membentuk free chain
• Saat menyisipkan item baru, free_head diperiksa untuk melihat apakah ada slot yang bisa dipakai ulang; jika ada, slot Vacant ditimpa menjadi Occupied lalu free_head dipindah ke nilai berikutnya
• Jika tidak ada free slot, slot Occupied baru di-push ke akhir, lalu kuncinya diambil, hash dihitung, dan indeks baru dicatat di hash table
• Penghapusan bekerja sebaliknya: mencari indeks di hash table lewat kunci lalu menghapusnya, kemudian ItemSlot terkait diubah menjadi Vacant dan free_head lama dihubungkan sebagai next
• IdOrdMap memakai indeks B-tree alih-alih hash table, sedangkan BiHashMap dan TriHashMap masing-masing menyimpan dua dan tiga hash table

Iterasi mutable dan perpanjangan lifetime

• IdOrdMap::iter_mut melakukan iterasi mutable atas item menurut urutan kunci
• Iterator Rust tidak boleh mengembalikan nilai yang masih meminjam iterator itu sendiri, dan kombinator seperti collect bisa menyisakan nilai seperti Vec<&mut T> bahkan setelah iteratornya hilang
• Agar perilaku ini aman, iterator tidak boleh mengembalikan nilai yang sama dua kali
• Borrow checker hanya melihat akses berurutan terhadap daftar dan tidak bisa mengetahui bahwa semua indeks pasti berbeda
• iddqd memakai perpanjangan lifetime dengan std::mem::transmute::<&mut T, &'a mut T>, yang bergantung pada invariant bahwa indeks yang dikembalikan self.iter semuanya berbeda

Bug yang dibuat oleh implementasi Ord patologis

• Dalam IdOrdMap berisi lima item dengan kunci 0 sampai 4 secara berurutan, jika kunci 0 diakses lewat Entry API, maka OccupiedEntry menyimpan indeks 0 di dalamnya
• Jika setelah itu implementasi Ord pada Key diubah sehingga selalu mengembalikan Equal tanpa memandang nilainya, OccupiedEntry::remove saat menelusuri ulang B-tree bisa menghapus item yang salah hanya berdasarkan perbandingan kunci
• Misalnya jika B-tree lebih dulu membandingkan (key = 2, index = 2), entri itu akan dihapus karena Equal, dan karena OccupiedEntry memegang indeks 0, item 0 akan dihapus dari item set
• Dalam keadaan ini, indeks 0 masih tertinggal di B-tree tetapi slot 0 pada item set menjadi vacant, sementara item 2 tetap ada di item set namun kehilangan pointer B-tree
• Setelah Ord kembali berfungsi normal dan item dengan kunci 1000 disisipkan, slot 0 yang ditunjuk free_head akan dipakai ulang
• Hasilnya, indeks duplikat yang menunjuk ke slot yang sama muncul di B-tree, dan IterMut bisa membuat beberapa referensi &mut ke memori yang sama sehingga menjadi unsound

Cara perbaikan dan kompromi performa

• Saat menelusuri B-tree ke bawah, kini yang diperiksa bukan hanya kesetaraan kunci tetapi juga kesetaraan indeks
• Saat mencari kunci dengan indeks yang sudah diketahui, pencarian membandingkan (key, index) sekaligus, sehingga meskipun Ord patologis mengembalikan Equal, perbandingan antara (key = 2, index = 2) dan indeks 0 yang dicari akan menjadi Less berkat tie-breaker indeks
• Agar pencarian ini berhasil, indeks yang tersimpan memang harus sama dengan indeks yang dicari
• Tie-breaker mencegah pencocokan item yang salah, tetapi tidak menjamin item yang benar selalu ditemukan
• B-tree diurutkan menurut kunci, sedangkan tie-breaker membandingkan indeks, sehingga kedua urutan ini pada umumnya saling independen
• Jika pencarian tree gagal, penghapusan indeks terkait di B-tree dilakukan dengan linear scan yang tidak memanggil kode pengguna
• Fallback ini memang mengubah operasi penghapusan dari waktu logaritmik menjadi linear, tetapi hanya tercapai bila ada kode pengguna yang buggy, sehingga dianggap kompromi yang dapat diterima

Lapisan verifikasi

• Karena iddqd dipakai sebagai struktur data fondasional, peninjauan analitis digabungkan dengan berbagai verifikasi empiris
• Setiap blok unsafe dan pola unsafe dianalisis oleh satu sampai tiga penulis dan reviewer Rust
• Di atas setiap blok unsafe ada komentar // SAFETY: yang mencatat penalarannya, dan lint undocumented_unsafe_blocks dari Clippy dipakai untuk memastikan komentarnya ada
• Example-based test membuat map, menjalankan operasi, lalu memeriksa hasilnya; iddqd memiliki unit test internal dan integration test untuk API publik
• Test-test ini juga ada sebagai doctest sehingga sekaligus berfungsi sebagai dokumentasi
• Test patologis memasok Ord buggy dan implementasi trait lainnya
• Di CI, test reguler dan test patologis dijalankan di bawah Miri untuk mendeteksi berbagai jenis UB
• Kondisi seperti invariant bahwa tidak boleh ada indeks duplikat juga bisa diperiksa di lingkungan test biasa di luar Miri

Pengujian berbasis model dan fault injection

• iddqd memakai dua lapis randomized testing: model-based testing yang membandingkan dengan oracle yang benar, dan fault injection di atasnya
• Model-based testing, atau stateful property-based testing, menerapkan urutan operasi acak pada sebuah instance tipe lalu membandingkan hasilnya dengan oracle yang diketahui benar
• iddqd menjalankan model-based test secara luas terhadap NaiveMap oracle yang tidak efisien tetapi jelas benar
• Fault injection berarti menyuntikkan bug secara acak ke dalam kode pengguna, dan pada iddqd, panic safety menjadi sumbu yang sangat efektif
• Invariant map tidak boleh rusak meskipun kode pengguna panic di tengah operasi
• Setiap operasi map diberi panic countdown acak, lalu countdown dikurangi 1 setiap kali kode pengguna dipanggil, dan ketika mencapai 0 program panic, sehingga tercipta pengujian panic safety acak
• Pendekatan ini menemukan beberapa bug halus di iddqd, dan sebagian di antaranya berujung pada unsoundness
• Model-based test juga memverifikasi invariant internal seperti no-duplicate-index setelah setiap operasi
• Karena model-based test terlalu lambat untuk dijalankan di bawah Miri, invariant yang menjadi dasar soundness dan correctness diperiksa secara terpisah

Review adversarial oleh LLM dan teknik formal

• Model frontier generasi saat ini berhasil menemukan beberapa implementasi kode pengguna patologis yang dapat merusak map
• Dalam satu kasus yang menonjol, LLM menyusun jalur ketika custom allocator panic dan unwind, lalu invariant map rusak
• Ini adalah masalah panic safety yang berbeda dari panic kode pengguna biasa seperti implementasi Ord, yang sudah dicakup oleh panic safety test sebelumnya
• LLM juga bisa menghasilkan klaim soundness yang terlihat masuk akal tetapi salah, sehingga red-green TDD dengan Miri sebagai oracle menjadi mekanisme pertahanan
• Untuk bug soundness, langkahnya adalah terlebih dulu membuat test yang menunjukkan UB di bawah Miri, lalu setelah perbaikan memeriksa kembali bahwa test yang sama lolos
• Pendekatan untuk membuktikan invariant map dengan model checker seperti Kani terkendala karena iddqd terlalu kompleks, sehingga proof yang dibutuhkan menjadi terlalu besar untuk ditangani alat tersebut
• Creusot dapat membantu membuktikan bahwa kode Rust bebas dari panic dan kesalahan lain, tetapi saat ini belum bisa membuktikan invariant yang harus tetap terjaga meskipun kode pengguna panic atau berperilaku salah
• NaiveMap berfungsi sebagai spesifikasi yang paling mendekati untuk iddqd, dan CI menjalankan model-based test ribuan kali untuk memberi tingkat kepercayaan tinggi bahwa implementasinya sesuai dengan spesifikasi
• cargo-anneal adalah alat yang sedang dikembangkan dan menarik perhatian karena memungkinkan proof soundness Lean ditempatkan di komentar dokumentasi di samping unsafe Rust
• iddqd memiliki invariant yang jelas dan cakupan yang terbatas tetapi tidak sepele, sehingga menjadi kandidat benchmark untuk alat verifikasi formal

Kesimpulan

• Unsafe generic Rust sangat sulit karena setiap invariant harus dipertahankan dengan mempertimbangkan implementasi trait apa pun, termasuk yang arbitrer dan adversarial
• Bug di iddqd menunjukkan bahwa implementasi Ord yang patologis bisa menipu map hingga menciptakan mutable alias pada memori yang sama
• Tidak ada satu teknik pun yang dapat menangkap semua bug, sehingga penalaran unsafe baris demi baris oleh manusia, example-based test, pathological test, randomized test, dan review adversarial oleh model frontier dipakai bersama-sama
• Oxide menilai tingkat ketelitian seperti ini layak untuk infrastruktur fondasional

[GN⁺]

Komentar Lobste.rs

• Kalau saya memahaminya dengan benar (sedang lihat di ponsel saat bepergian), ini tampaknya bisa diselesaikan dengan memakai tipe pembungkus dan HashSet/BTreeSet alih-alih HashMap/BTreeMap
  Tipe pembungkusnya sendiri tidak wajib, tetapi demi keamanan dan kemudahan pemeliharaan ke depan, itu pilihan yang baik
  Yang dibutuhkan hanya pembungkus berukuran 0 di sekitar objek, lalu implementasi PartialEq/Hash kustom yang hanya melihat field yang relevan. Jika ingin melakukan pencarian tanpa membangun nilai lengkap, Anda bisa membuat tipe kedua yang mengimplementasikan AsRef untuk tipe nilai
  Pendekatan ini adalah cara untuk memakai ulang antarmuka HashSet/BTreeSet yang ada apa adanya tanpa unsafe. Alih-alih membungkus tipe nilai/kunci, Anda juga bisa membuat pembungkus HashSet/BTreeSet baru yang menangani perilaku semacam ini

  • Di sini kuncinya adalah kombinasi arbitrer dari field dan subfield pada tipe record, dan itu diekspresikan dengan GAT. Selain itu, pola indeks integer/slab juga bisa digeneralisasi secara alami menjadi peta multi-indeks
    API Entry, akses/iterasi yang dapat diubah, dan sebagainya juga ada. Di dalam iddqd, mutabilitas ditangani dengan cukup hati-hati, dan di beberapa tempat nilai atomik dipakai untuk mengizinkan interior mutability. Penanganan semacam ini akan cukup sulit tanpa indireksi indeks

• Untuk memverifikasi iddqd secara formal, awalnya saya rasa saya akan mencoba model checker seperti Kani untuk membuktikan bahwa peta tidak merusak invarian internal. Tetapi saya penasaran dengan bagian yang mengatakan iddqd sedikit terlalu rumit untuk ditangani Kani, dan bahwa pembuktian yang diperlukan menjadi terlalu besar untuk ditangani alat tersebut
  Bisakah Anda berbagi lebih detail soal bagian ini? Saya penasaran apakah maksudnya kompleksitas komputasi algoritmenya mengalami degradasi ke kasus terburuk
  Secara umum ini menarik sebagai studi kasus metode formal, dan saya senang bagian ini dibahas. Kalau melihat kisah sukses alat verifikasi formal yang ada pada proyek berskala besar, orang bisa secara naif mengira setidaknya kebenaran struktur data bisa dibuktikan, tetapi kenyataannya tingkat kesulitannya berbeda-beda untuk tiap struktur data, dan bahkan dalam bahasa yang dianggap lebih ramah pembuktian daripada bahasa seperti Rust yang mengizinkan aliasing tanpa batas, hal itu tetap tidak mudah secara praktis
  Sedikit keluar topik, tapi saya juga penasaran bagaimana diagramnya dibuat. Apakah menulis skrip sekali pakai, karena itu terlihat seperti sesuatu yang dibuat khusus agar cocok dengan desain blog/situs Oxide dan bukan alat umum

  • Di bagian bawah tulisan tertulis “Diagrams courtesy Ben Leonard.”, dan Ben Leonard adalah desainer di Oxide. Jadi sepertinya kemungkinan besar itu diagram buatan tangan
  • Bahkan ketika mencoba membuktikan hal yang sangat mendasar terhadap implementasi trait yang konkret dan berfungsi baik, CBMC tetap berputar memakai CPU dan lebih dari 10 menit belum selesai
    Saya juga sempat mempersempit cakupannya. Misalnya, saya mengasumsikan hashbrown benar, tetapi itu pun tidak banyak membantu. Di titik itu saya nyaris menyerah. Untuk implementasi trait yang berfungsi baik, saya cukup yakin iddqd itu benar, dan yang benar-benar saya minati dari metode formal adalah pembuktian yang tetap berlaku bahkan untuk implementasi arbitrer yang salah
    Namun saya juga bukan orang yang paling mahir memakai Kani. Akan sangat bagus kalau Anda atau orang lain mau mencoba ini
    Untuk diagramnya, saya mula-mula membuat sketsa di Mermaid, lalu desainer kami yang luar biasa, Ben Leonard, menyempurnakannya secara manual menjadi diagram yang sesuai dengan palet warna dan tema kami

• Pola peta berbasis field yang mengindeks objek memakai salah satu field objek itu sebagai kunci adalah sesuatu yang selalu saya harap bisa dipakai dengan mudah juga di C#
  Dulu saya pernah mencoba membuat versi sederhana sendiri, tetapi antarmukanya tidak terlalu rapi jadi saya hentikan. Tulisan ini membuat saya ingin mencoba lagi

  • Ya, ini memang pola yang sangat berguna. Awalnya saya membuatnya untuk pekerjaan yang dibutuhkan di kantor, tetapi setelah itu saya memakainya di berbagai tempat, dari codebase produksi seperti cargo-nextest sampai proyek pribadi
    Memakai satu field sebagai kunci memang kasus penggunaan yang paling umum, tetapi iddqd cukup fleksibel untuk memakai kombinasi apa pun dari field, subfield, atau fungsi apa pun yang bisa dihitung dari field secara murni dan murah. Misalnya lihat ArtifactKey di https://docs.rs/iddqd/latest/iddqd/ (maaf kalau Anda tidak terbiasa dengan sintaks Rust)
    Saat merancang iddqd, saya sangat merasa bahwa pengguna harus bisa memanfaatkan seluruh kekuatan sistem tipe Rust. Tidak masalah seberapa banyak jalan memutar yang harus saya tempuh sebagai penulis library. Saya benar-benar ingin iddqd menjadi library yang menyenangkan untuk dipakai para pengguna, terutama rekan kerja saya