iddqd, ya da en zor türden unsafe Rust

• iddqd, değerden anahtarı ödünç alan bir Rust map kütüphanesidir; Oxide’ın Omicron kontrol düzleminde disk ve sled envanteri gibi büyük kayıtların bellek içi indekslerini tutar, bu yüzden doğruluk kritik önemdedir
• Standart BTreeMap, anahtar ve değeri ayrı sakladığı için aktarması zahmetlidir ya da yinelenen anahtarlar birbirinden sapabilir; buna karşılık IdOrdMap, kaydın içindeki bir alandan anahtarı çıkararak sorgu yapar
• unsafe Rust, derleyicinin kanıtlayamadığı güvenli programları ifade etmek için bir kaçış kapısıdır; jenerik kod kullanıcı tarafından sağlanan trait implementasyonlarını çağırdığında patolojik güvenli Rust’a bile dayanmak zorundadır
• iddqd içindeki mutable iteration, tüm indekslerin farklı olduğu değişmezine dayanarak ömürleri genişletir; patolojik bir Ord implementasyonu B-tree ile item set’i birbirinden saptırarak aynı öğe için yinelenen indeksler oluşturabiliyordu
• Düzeltme, anahtar ve indeksi birlikte karşılaştırıyor ve başarısız olursa kullanıcı kodunu çağırmayan doğrusal taramaya geri dönüyor; yeterli güven için Miri, model tabanlı testler, panic fault injection ve LLM tabanlı düşmanca inceleme birlikte kullanılmalı

---

iddqd’nin çözdüğü problem

• iddqd, anahtarı değerden ödünç alan map yapıları sunan bir Rust kütüphanesidir ve Oxide bunu Omicron kontrol düzleminde yaygın biçimde kullanır
• Omicron, Oxide rack’inin merkezinde compute ve storage gibi kaynakları provizyonlayan ve rack’in çalışmayı sürdürmesini sağlayan yazılımdır; iddqd hatalı çalışırsa kontrol düzlemi öngörülemez ve teşhisi zor biçimlerde yanlış davranabilir
• Rust standart kütüphanesindeki BTreeMap<Email, User> gibi bir yapı, anahtar olan email’i değerden ayrı saklar
• Anahtarı ve değeri birlikte geçirmek için get_key_value ile (email, user) almak gerekir; ayrıca fetch anında UserRecord gibi ayrı bir struct oluşturmak, kayıt türü çok olduğunda yönetmeyi zorlaştırır
• Email’i User içinde de kopyalarsanız, map’in anahtarı ile değerin içindeki email’in birbirinden farklı olma riski ortaya çıkar
• IdOrdMap, IdOrdItem trait’i aracılığıyla kayıttan anahtar çıkarmayı sağlar; anahtar tipi type Key<'a> = &'a Email örneğinde olduğu gibi değerden ödünç alınabilir
• Oxide’da bu desen, veritabanı sorgu sonuçları gibi büyük kayıtlar için çok uygundu ve kontrol düzlemi genelinde büyük kayıtların indekslenmesinde faydalı oldu

Ek özellikler

• iddqd, birden fazla alandan ödünç alınan karmaşık anahtarları birinci sınıf olarak destekler; böylece dynamic dispatch gibi dolaylı çözümler gerekmez
• BiHashMap ve TriHashMap, tek bir öğeyi sırasıyla iki veya üç ayrı anahtarla indeksler; böylece birden fazla map’i elle senkron tutma ihtiyacını ortadan kaldırır
• Serde implementasyonu, map yerine sequence olarak serileştirme yapar; böylece JSON içinde string olmayan anahtarlar da serileştirilebilir ve yinelenen anahtarlar reddedilir
• Geriye dönük uyumluluk için map biçiminde serileştirme de desteklenir

unsafe Rust’ın zorlaştığı yer

• Rust’ta temel risk tanımsız davranıştır (undefined behavior, UB); güvenli kod hiçbir şekilde UB üretemiyorsa sound, aksi durumda unsound kabul edilir
• Güvenli Rust içinde derleyici, UB içeren programları reddeder; ancak statik analizin sınırları nedeniyle UB içermeyen bazı programları da birlikte reddeder
• unsafe anahtar sözcüğü bu tür programları ifade etmek için bir kaçış kapısıdır; yazar, soundness sorumluluğunu üstlenir ve derleyiciden güven ister
• unsafe kodun uyması gereken Rust kuralları arasında veri yarışı olmaması, başlatılmamış veya serbest bırakılmış belleğin okunmaması, aynı bellek bölgesi için birden fazla &mut alias olmaması ve immutable verinin değiştirilmemesi bulunur
• Bu kuralları özellikle mutable aliasing nedeniyle akıl yürütmek zordur; bu yüzden genellikle unsafe’in güvenli soyutlamaların arkasında kapsüllenmesi gerekir

Güvenli soyutlama doğrulamasının aşamaları

• split_at_mut, mutable slice’ı iki parçaya ayıran güvenli bir metottur; ancak güvenli Rust ile bu tür bir bölme ifade edilemediği için unsafe gerekir
• split_at_mut’ın soundness’ı, &mut [T] alınıp alınmadığına, mid <= slice.len() kontrolünün yapılıp yapılmadığına ve kalan uzunluğun doğru hesaplanmasına dair çevresindeki güvenli kod değişmezlerine dayanır
• MyVec<T> içindeki get, len alanının doğru olmasına ve aralığın içinde kalmasına bağlıdır; bu koşul aynı modüldeki diğer tüm metotlar tarafından korunmalıdır
• Kullanıcı tarafından sağlanan kodu çağıran jenerik unsafe kod en zor kategoridir
• Güvenli Rust kodu ne kadar patolojik ya da düşmanca yazılmış olursa olsun, unsafe kodun UB üretmesine yol açmamalıdır
• ExactSizeIterator içindeki len() değerine güvenip capacity kadar yazan collect_exact benzeri kod, iterator sahte bir uzunluk döndürürse ayrılmamış belleğe yazacağı için genellikle unsound’dur
• std::io::Read de okunan bayt sayısını yanlış döndürebilen bug’lı implementasyonlara açık bir trait’tir; Rust RFC 2930 bu problemi ele alır
• iddqd, kullanıcı tarafından sağlanan trait implementasyonlarını çağıran jenerik bir veri yapısı olduğu için bu en zor sınıfa girer

iddqd’nin iç yapısı

• iddqd, bir öğe listesi olan ItemSet ile slot indekslerini tutan bir tabloyu birleştirir
• IdHashMap<T>, ItemSet<T> ile ItemIndex tutan bir hashbrown::HashTable kullanır
• ItemSet<T>, Vec<ItemSlot<T>> içerir ve ItemSlot<T>, Occupied(T) ya da Vacant { next: ItemIndex } biçimindedir
• free_head, en son boşaltılmış Vacant slot’u ya da boş slot olmadığını gösteren sentinel değeri işaret eder; free_head ile Vacant slot’lar birlikte free chain’i oluşturur
• Yeni öğe eklenirken önce free_head üzerinden yeniden kullanılabilir slot olup olmadığı kontrol edilir; varsa Vacant slot Occupied ile üzerine yazılır ve free_head bir sonraki değere taşınır
• Boş slot yoksa sona yeni bir Occupied slot push edilir; ardından anahtar alınır, hash hesaplanır ve yeni indeks hash table’a kaydedilir
• Silme işlemi bunun tersidir: hash table’da anahtarla indeks bulunup kaldırılır, ardından ilgili ItemSlot Vacant yapılır ve önceki free_head değeri next olarak bağlanır
• IdOrdMap, hash table yerine B-tree indeksi kullanır; BiHashMap ve TriHashMap ise sırasıyla iki ve üç hash table tutar

mutable iteration ve ömür genişletme

• IdOrdMap::iter_mut, öğeler üzerinde anahtar sırasına göre mutable iteration yapar
• Rust iterator’lerinde döndürülen değer, iterator’ün kendisini ödünç almamalıdır; collect gibi birleştiriciler, iterator yok olduktan sonra bile Vec<&mut T> gibi değerler bırakabilir
• Bunun güvenli olması için iterator aynı değeri iki kez döndürmemelidir
• Borrow checker, yalnızca listeye ardışık erişimi görür; tüm indekslerin farklı olduğunu kendiliğinden bilemez
• iddqd, std::mem::transmute::<&mut T, &'a mut T> ile lifetime extension kullanır; bu da self.iter tarafından döndürülen indekslerin hepsinin farklı olduğu değişmezine dayanır

Patolojik Ord implementasyonunun yarattığı hata

• Anahtarları 0’dan 4’e kadar sıralı beş öğe içeren bir IdOrdMap’te, Entry API ile anahtar 0 sorgulandığında OccupiedEntry dahili olarak indeks 0’ı saklar
• Daha sonra Key türünün Ord implementasyonu, değerden bağımsız olarak her zaman Equal döndürecek şekilde değiştirilirse, OccupiedEntry::remove B-tree içinde yeniden inerken yalnızca anahtar karşılaştırmasıyla yanlış öğeyi kaldırabilir
• Örneğin B-tree’de önce (key = 2, index = 2) karşılaştırılırsa, Equal sonucu nedeniyle bu entry silinir; buna karşın OccupiedEntry elindeki indeks 0 nedeniyle item set’te öğe 0’ı siler
• Bu durumda B-tree içinde indeks 0 kalır, fakat item set içindeki slot 0 boşalmış olur; öğe 2 ise item set’te kalır ama artık B-tree işaretçisi yoktur
• Sonrasında Ord yeniden normal çalışmaya döner ve anahtar 1000 olan bir öğe eklenirse, free_head tarafından gösterilen slot 0 yeniden kullanılır
• Sonuç olarak B-tree içinde aynı slot’u gösteren yinelenen indeksler oluşur ve IterMut aynı belleğe birden fazla &mut referans üretebildiği için yapı unsound hale gelir

Düzeltme yaklaşımı ve performans ödünleşimi

• B-tree içinde aşağı inerken artık yalnızca anahtar değil, indeks eşitliği de birlikte doğrulanır
• Bilinen indekse sahip bir anahtar aranırken (key, index) birlikte karşılaştırılır; böylece patolojik Ord, Equal döndürse bile (key = 2, index = 2) ile aranan indeks 0 karşılaştırıldığında indeks tie-breaker nedeniyle sonuç Less olur
• Bu aramanın başarılı olması için saklanan indeksin gerçekten aranan indeksle aynı olması gerekir
• Tie-breaker, yanlış öğe eşleşmesini engeller; ancak doğru öğeyi her zaman bulmayı garanti etmez
• B-tree anahtara göre sıralıdır, tie-breaker ise indeksi karşılaştırır; bu iki sıralama genel olarak birbirinden bağımsızdır
• Tree search başarısız olursa, kullanıcı kodunu çağırmayan doğrusal tarama ile ilgili indeks B-tree’den kaldırılır
• Bu fallback, silme işlemini logaritmik zaman yerine doğrusal zamana çevirir; ancak yalnızca hatalı kullanıcı kodu varken ulaşılabildiği için kabul edilebilir bir ödünleşim sayılır

Doğrulama katmanları

• iddqd, temel veri yapısı olarak kullanıldığı için analitik inceleme ile çeşitli ampirik doğrulama yöntemlerini birlikte kullanır
• Tüm unsafe bloklar ve unsafe kalıplar, bir ila üç Rust geliştiricisi ve gözden geçireni tarafından analiz edilir
• Her unsafe bloğun üzerinde // SAFETY: yorumu ile gerekçelendirme bırakılır ve Clippy’nin undocumented_unsafe_blocks lint’i bu yorumların varlığını denetler
• Örnek tabanlı testler, map oluşturup işlemler yaptıktan sonra sonucu doğrular; iddqd, hem iç unit test’lere hem de herkese açık API integration test’lerine sahiptir
• Bu testler doctest olarak da bulunur ve aynı zamanda dokümantasyon işlevi görür
• Patolojik testler, bug’lı Ord ve başka trait implementasyonları sağlar
• CI ortamında hem normal testler hem de patolojik testler Miri altında çalıştırılarak çeşitli UB türleri saptanır
• Yinelenen indeks olmaması gibi değişmezler, Miri dışındaki normal test ortamlarında da doğrulanabilir

Model tabanlı testler ve fault injection

• iddqd, iki katmanlı randomized testing kullanır: doğru kabul edilen bir oracle ile karşılaştıran model-based testing ve bunun üzerinde fault injection
• Model tabanlı test veya stateful property-based testing, rastgele işlem dizilerini bir tip örneğine uygular ve sonuçları doğru olduğu bilinen oracle ile karşılaştırır
• iddqd, verimsiz ama açıkça doğru olan NaiveMap oracle karşısında kapsamlı model tabanlı testler yürütür
• Fault injection, kullanıcı koduna rastgele hata ekleme yöntemidir; iddqd için özellikle panic safety bu eksende çok etkili oldu
• Kullanıcı kodu işlemin ortasında panic etse bile map’in değişmezleri bozulmamalıdır
• Her map işlemine rastgele bir panic countdown eklenir; kullanıcı kodu her çağrıldığında sayaç 1 azaltılır ve 0 olduğunda panic tetiklenerek rastgele panic safety testi yapılır
• Bu yöntem, iddqd içinde birkaç incelikli hatayı ortaya çıkardı ve bunların bazıları unsoundness’a yol açıyordu
• Model tabanlı testler, her işlemden sonra no-duplicate-index gibi dahili değişmezleri de doğrular
• Model tabanlı testler, Miri altında çalıştırmak için fazla yavaştır; bu yüzden soundness ve correctness’ın dayandığı değişmezler ayrıca doğrulanır

LLM tabanlı düşmanca inceleme ve biçimsel yöntemler

• Güncel nesil frontier modeller, map’i bozan çeşitli patolojik kullanıcı kodu implementasyonları bulabildi
• Dikkat çekici bir vakada LLM, custom allocator panic edip unwind olduğunda map değişmezlerinin bozulduğu bir yolu kurguladı
• Bu, mevcut panic safety testlerinin ele aldığı Ord implementasyonu gibi genel kullanıcı kodu panic’lerinden farklı bir panic safety problemiydi
• LLM’ler kulağa makul gelen ama yanlış soundness iddiaları da üretebilir; bu yüzden Miri’yi oracle olarak kullanan red-green TDD savunma mekanizması olur
• Soundness hatalarında önce Miri altında UB gösteren bir test yazılır, sonra düzeltmeden sonra aynı testin geçtiği yeniden doğrulanır
• Kani gibi bir model checker ile map değişmezlerini kanıtlama yaklaşımında, iddqd yeterince karmaşık olduğu için gerekli proof’lar aracın kaldırabileceğinden fazla büyür
• Creusot, Rust kodunun panic ve diğer hatalardan arınmış olduğunu kanıtlamada yardımcı olabilir; ancak kullanıcı kodu panic etse ya da yanlış davransa bile korunması gereken değişmezleri şu aşamada kanıtlayamaz
• NaiveMap, iddqd için en yakın specification işlevini görür ve CI’da model tabanlı testlerin binlerce kez çalıştırılması, implementasyonun specification ile uyumlu olduğuna dair yüksek güven sağlar
• cargo-anneal, unsafe Rust yanındaki doc comment içine Lean soundness proof’ları yerleştirmeyi amaçlayan geliştirme aşamasındaki bir araç olarak ilgi çekicidir
• iddqd, açık değişmezleri ve sınırlı ama önemsiz olmayan kapsamı sayesinde biçimsel doğrulama araçları için iyi bir benchmark adayıdır

Sonuç

• unsafe jenerik Rust, rastgele trait implementasyonlarını ve hatta düşmanca implementasyonları hesaba katıp her değişmezi korumak zorunda olduğu için son derece zordur
• iddqd hatası, patolojik bir Ord implementasyonunun map’i kandırarak aynı bellek üzerinde mutable alias oluşturabildiğini gösteriyor
• Tek bir teknik tüm hataları yakalayamadığı için, insanların satır satır unsafe muhakemesi, örnek tabanlı testler, patolojik testler, randomized testler ve frontier model tabanlı düşmanca inceleme birlikte kullanılır
• Oxide, temel altyapıda bu düzeyde bir titizliğin haklı olduğunu düşünüyor

[GN⁺]

Lobste.rs görüşleri

• Doğru anladıysam (yoldayım, telefondan baktım), bu iş sarmalayıcı tip kullanıp HashMap/BTreeMap yerine HashSet/BTreeSet kullanılarak çözülebilir gibi görünüyor
  Sarmalayıcı tip kesinlikle gerekli değil ama güvenlik ve sonraki bakım açısından iyi bir tercih olur
  Gereken tek şey nesneyi saran 0 boyutlu bir sarmalayıcı; ardından sadece ilgilenilen alanlara bakan özel bir PartialEq/Hash implementasyonu eklenebilir. Tüm değeri oluşturmadan arama yapmak için, değer tipi için AsRef uygulayan ikinci bir tip oluşturulabilir
  Bu yaklaşım, unsafe kullanmadan mevcut HashSet/BTreeSet arayüzünü aynen yeniden kullanmanın bir yolu. Değer/anahtar tipini sarmalamak yerine, bu davranışı sağlayan yeni bir HashSet/BTreeSet sarmalayıcısı da yapılabilir

  • Burada anahtar, kayıt tipinin alanları ve alt alanlarının keyfi birleşiminden oluşuyor ve GAT ile ifade ediliyor. Ayrıca tamsayı indeks/slab deseni çoklu indeksli map’e de doğal biçimde genelleniyor
    Entry API’si, değiştirilebilir erişim/yineleme gibi şeyler de var. iddqd içinde değiştirilebilirlik oldukça dikkatli ele alınıyor ve bazı yerlerde içsel değiştirilebilirliğe izin vermek için atomik değerler kullanılıyor. Böyle bir işlem indeks dolaylı başvurusu olmadan epey zor olurdu

• iddqd için biçimsel doğrulama yapacak olsam, ilk olarak Kani gibi bir model denetleyici ile map’in iç değişmezleri bozmadığını kanıtlamaya çalışırdım. Ama iddqd’nin Kani’nin ele alması için biraz fazla karmaşık olduğu ve gereken kanıtların aracın kaldırabileceğinden fazla büyüdüğü kısmı merak ettim
  Bunu biraz daha ayrıntılı paylaşabilir misiniz? Algoritmanın hesaplama karmaşıklığının en kötü durumda dejenere olduğu anlamına mı geliyor diye merak ediyorum
  Genel olarak bu, biçimsel yöntemler için ilginç bir vaka çalışması ve bu konuya değinmenize sevindim. Mevcut biçimsel doğrulama araçlarının, büyük projelerdeki başarı örneklerine bakınca, en azından veri yapısının doğruluğunu kanıtlayabileceğini naifçe düşünebiliriz; ama pratikte veri yapısına göre zorluk çok değişiyor ve Rust gibi sınırsız aliasing’e izin veren dillere kıyasla kanıtlamaya daha elverişli sayılan dillerde bile bunun iş ortamında kolay olmadığı ortaya çıkıyor
  Konudan biraz sapıyor ama diyagramları nasıl yaptığınızı da merak ettim. Tek seferlik bir betik mi yazdınız, yoksa Oxide blog/web sitesi tasarımına uyarlanmış özel üretimler gibi görünüyor; genel amaçlı bir araç gibi durmuyor

  • Yazının altında “Diagrams courtesy Ben Leonard.” yazıyor ve Ben Leonard Oxide’ın tasarımcısı. O yüzden muhtemelen elle hazırlanmış diyagramlar olma ihtimali yüksek görünüyor
  • Somut ve düzgün çalışan trait implementasyonlarını hedef alıp çok temel bir şeyi kanıtlamaya çalışsam bile, CBMC CPU’yu kullanıp 10 dakikadan fazla çalıştıktan sonra bile bitmedi
    Kapsamı daraltmayı da denedim. Örneğin hashbrown’un doğru olduğunu varsaydım ama bu da pek ilerleme sağlamadı. O noktada neredeyse vazgeçtim. Düzgün çalışan trait implementasyonları için iddqd’nin doğru olduğundan oldukça eminim ve biçimsel yöntemlerde benim asıl ilgimi çeken şey, keyfi ve hatalı çalışan implementasyonlar için de geçerli bir kanıttı
    Ama Kani’yi en iyi kullanan kişi ben değilim. Siz ya da başka biri bunu denese gerçekten harika olur
    Diyagramları önce Mermaid ile taslak olarak yaptım, sonra da harika tasarımcımız Ben Leonard bunları bizim renk paletimize ve temamıza uygun el yapımı diyagramlara dönüştürdü

• Bir nesneyi, o nesnenin alanlarından birini anahtar olarak kullanıp indeksleyen alan tabanlı map deseni, C#’ta da her zaman kullanabilmeyi istediğim bir şey
  Bir zamanlar kendim basit bir sürüm yapmaya çalışmıştım ama arayüzü çok temiz olmamıştı, ben de bırakmıştım. Bu yazı bana tekrar deneme isteği verdi

  • Evet, gerçekten çok faydalı bir desen. İş yerinde ihtiyaç duyduğum bir şey yüzünden yaptım ama sonrasında cargo-nextest gibi prodüksiyon kod tabanlarından kişisel projelere kadar her yerde kullanır oldum
    Tek bir alanı anahtar olarak kullanmak en yaygın kullanım olsa da, iddqd yeterince esnek; alanların, alt alanların veya bir alandan saf ve ucuz biçimde hesaplanabilen fonksiyonların herhangi bir birleşimi kullanılabiliyor. Örneğin https://docs.rs/iddqd/latest/iddqd/ içinde ArtifactKey aratabilirsiniz (Rust sözdizimine aşina değilseniz kusura bakmayın)
    iddqd’yi tasarlarken, kullanıcıların Rust tip sisteminin tüm gücünü kullanabilmesi gerektiğini güçlü biçimde hissediyordum; bunun için kütüphane yazarı olarak benim ne kadar dolambaçlı yol izlemem gerekirse gereksin. iddqd’nin kullanıcılar, özellikle de iş arkadaşlarım için kullanımı keyifli bir kütüphane olmasını gerçekten istedim