iddqd, या unsafe Rust का सबसे कठिन प्रकार

• iddqd एक Rust map लाइब्रेरी है जो value से key उधार लेती है, और Oxide के Omicron control plane में disk और sled inventory जैसे बड़े records के in-memory index बनाए रखने के लिए इस्तेमाल होती है, जहाँ correctness बेहद महत्वपूर्ण है
• मानक BTreeMap key और value को अलग-अलग संग्रहीत करता है, इसलिए उन्हें साथ ले जाना असुविधाजनक हो सकता है या duplicate keys के mismatch होने का जोखिम रहता है, लेकिन IdOrdMap record के अंदर के field से key निकालकर lookup करता है
• unsafe Rust एक escape hatch है जो ऐसे सुरक्षित programs को व्यक्त करने देता है जिन्हें compiler साबित नहीं कर सकता, और जब generic code user-provided trait implementations को call करता है तो उसे pathological safe Rust तक झेलना पड़ता है
• iddqd में mutable iteration इस invariant पर निर्भर करती है कि सारे index अलग हैं, इसलिए यह lifetime extension करती है; लेकिन pathological Ord implementation B-tree और item set को असंगत बना सकती थी, जिससे एक ही item के duplicate index बन जाते थे
• fix में key और index दोनों की तुलना की जाती है, और failure पर user code को call किए बिना linear scan पर fallback किया जाता है; पर्याप्त भरोसा पाने के लिए Miri, model-based testing, panic fault injection, और LLM adversarial review को साथ में इस्तेमाल करना पड़ता है

---

वह समस्या जिसे iddqd हल करता है

• iddqd एक Rust लाइब्रेरी है जो ऐसे map उपलब्ध कराती है जिनमें key value से उधार ली जाती है, और Oxide इसे Omicron control plane में व्यापक रूप से इस्तेमाल करता है
• Omicron वह software है जो Oxide rack के केंद्र में compute और storage जैसे resources को provision करता है और rack को लगातार चालू रखता है; यदि iddqd गलत व्यवहार करे, तो control plane ऐसे तरीकों से गलत काम कर सकता है जिनकी भविष्यवाणी करना और diagnosis करना कठिन हो
• Rust standard library में BTreeMap<Email, User> जैसी संरचना key यानी email को value से अलग रखती है
• key और value को साथ पास करने के लिए get_key_value से (email, user) लाना पड़ता है, और यदि fetch के समय UserRecord जैसी अलग struct बनाई जाए, तो कई record types होने पर यह संभालना कठिन हो जाता है
• यदि email को User के अंदर भी duplicate किया जाए, तो map की key और value के भीतर का email अलग हो जाने का जोखिम बनता है
• IdOrdMap IdOrdItem trait के जरिए record से key निकालता है, और key type को type Key<'a> = &'a Email की तरह value से उधार लिया जा सकता है
• Oxide में यह pattern database query results जैसे बड़े records पर अच्छी तरह फिट हुआ, और पूरे control plane में बड़े records की indexing के लिए उपयोगी साबित हुआ

अतिरिक्त सुविधाएँ

• iddqd कई fields से उधार ली गई complex keys को first-class रूप में support करता है, इसलिए dynamic dispatch जैसे workaround की जरूरत नहीं पड़ती
• BiHashMap और TriHashMap एक item को क्रमशः दो या तीन keys से index करते हैं, जिससे कई maps को हाथ से बनाए रखने वाला आम pattern टल जाता है
• Serde implementation map की बजाय sequence के रूप में serialization करती है, ताकि JSON में non-string keys भी serialize हो सकें, और duplicate keys को reject किया जा सके
• backward compatibility के लिए map-shaped serialization भी support की जाती है

unsafe Rust कहाँ कठिन हो जाता है

• Rust में मूल जोखिम undefined behavior (UB) है; यदि safe code किसी भी तरह UB पैदा नहीं कर सकता तो वह sound है, और नहीं तो unsound
• safe Rust में compiler UB वाले programs को reject कर देता है, लेकिन static analysis की सीमाओं के कारण कुछ UB-रहित programs भी reject हो जाते हैं
• unsafe keyword ऐसे programs को व्यक्त करने का escape hatch है, जहाँ लेखक soundness की जिम्मेदारी लेता है और compiler से trust माँगता है
• unsafe code को जिन Rust नियमों का पालन करना होता है, उनमें data race निषिद्ध होना, uninitialized या freed memory को न पढ़ना, एक ही memory region पर कई &mut alias न बनाना, और immutable data को modify न करना शामिल है
• इन नियमों पर तर्क करना खासकर mutable aliasing की वजह से कठिन होता है, इसलिए आम तौर पर safe abstraction के पीछे unsafe को encapsulate करना पड़ता है

safe abstraction को सत्यापित करने के चरण

• split_at_mut mutable slice को दो हिस्सों में बाँटने वाली एक safe method है, लेकिन safe Rust मात्र से इस तरह का split व्यक्त नहीं किया जा सकता, इसलिए unsafe चाहिए
• split_at_mut की soundness इस तरह के आसपास के safe-code invariants पर निर्भर करती है: क्या उसे &mut [T] मिला, क्या mid <= slice.len() जाँचा गया, और क्या बाकी length सही तरह गिनी गई
• MyVec<T> का get इस शर्त पर निर्भर करता है कि len सही है और index range के भीतर है; इस शर्त को उसी module की बाकी सारी methods को बनाए रखना होता है
• जब generic unsafe code user-provided code को call करता है, तब कठिनाई सबसे अधिक होती है
• safe Rust code कितना भी pathological या adversarial लिखा गया हो, उसे unsafe code से UB नहीं करवाना चाहिए
• ExactSizeIterator के len() पर भरोसा करके capacity भर लिखने वाला collect_exact जैसा code सामान्यतः unsound होता है, क्योंकि यदि iterator झूठी length लौटाए तो code unallocated memory में लिख देगा
• std::io::Read भी ऐसा trait है जिसकी buggy implementation पढ़े गए bytes की संख्या गलत लौटा सकती है, और Rust RFC 2930 इसी समस्या पर चर्चा करता है
• iddqd एक generic data structure है जो user-provided trait implementations को call करता है, इसलिए यह इसी सबसे कठिन श्रेणी में आता है

iddqd की आंतरिक संरचना

• iddqd item list ItemSet को slot index रखने वाली tables के साथ जोड़ता है
• IdHashMap<T> ItemSet<T> और ItemIndex रखने वाली hashbrown::HashTable का उपयोग करता है
• ItemSet<T> में Vec<ItemSlot<T>> होता है, और ItemSlot<T> या तो Occupied(T) होता है या Vacant { next: ItemIndex }
• free_head हाल में मुक्त किए गए Vacant slot की ओर इशारा करता है, या उस sentinel की ओर जो बताता है कि कोई free slot नहीं है; free_head और Vacant slots मिलकर free chain बनाते हैं
• नया item insert करते समय free_head से reusable slot देखा जाता है; यदि हो, तो Vacant slot को Occupied से overwrite किया जाता है और free_head को अगले मान पर बढ़ा दिया जाता है
• यदि free slot न हो, तो अंत में नया Occupied slot push किया जाता है, फिर key ली जाती है, hash निकाला जाता है, और नया index hash table में दर्ज किया जाता है
• removal उल्टी दिशा में होती है: पहले hash table में key से index खोजकर हटाया जाता है, फिर संबंधित ItemSlot को Vacant बनाया जाता है और पुराने free_head को next से जोड़ दिया जाता है
• IdOrdMap hash table की जगह B-tree index का उपयोग करता है, और BiHashMap तथा TriHashMap क्रमशः दो और तीन hash tables रखते हैं

mutable iteration और lifetime extension

• IdOrdMap::iter_mut key order में items पर mutable iteration करता है
• Rust iterator में लौटाए गए values iterator खुद को borrow नहीं करने चाहिए; collect जैसे combinators iterator खत्म होने के बाद भी Vec<&mut T> जैसे values छोड़ सकते हैं
• इस व्यवहार के सुरक्षित होने के लिए iterator को वही value दो बार नहीं लौटानी चाहिए
• borrow checker सूची पर क्रमिक access तो देख सकता है, लेकिन यह नहीं जान सकता कि सारे index अलग हैं
• iddqd std::mem::transmute::<&mut T, &'a mut T> के जरिए lifetime extension का उपयोग करता है, और यह इस invariant पर निर्भर करता है कि self.iter द्वारा लौटाए गए सारे index अलग हों

pathological Ord implementation से बना bug

• पाँच items वाले IdOrdMap में, जहाँ keys 0 से 4 तक क्रम में हैं, यदि Entry API से key 0 lookup की जाए, तो OccupiedEntry भीतर index 0 सहेज लेता है
• इसके बाद यदि Key की Ord implementation बदलकर ऐसी कर दी जाए जो value की परवाह किए बिना हमेशा Equal लौटाए, तो OccupiedEntry::remove जब B-tree में फिर नीचे जाता है, तब वह केवल key comparison के आधार पर गलत item हटा सकता है
• उदाहरण के लिए, यदि B-tree में पहले (key = 2, index = 2) से तुलना हो, तो Equal की वजह से वही entry हट जाएगी, और OccupiedEntry के पास मौजूद index 0 के कारण item set में item 0 हट जाएगा
• इस स्थिति में B-tree में index 0 बना रहता है, लेकिन item set का slot 0 vacant हो जाता है, और item 2 item set में रहते हुए भी B-tree pointer खो देता है
• बाद में Ord फिर सामान्य व्यवहार करने लगे और key 1000 वाला item insert किया जाए, तो free_head slot 0 को फिर से reuse करेगा
• नतीजतन B-tree में एक ही slot की ओर इशारा करने वाले duplicate index बन जाते हैं, और IterMut एक ही memory के लिए कई &mut references बना सकता है, जिससे unsoundness पैदा होती है

fix का तरीका और performance trade-off

• B-tree में नीचे जाते समय अब सिर्फ key नहीं, बल्कि index equality भी जाँची जाती है
• जब known index वाली key खोजी जाती है, तब (key, index) दोनों की तुलना होती है; इसलिए pathological Ord अगर Equal लौटाए भी, तो (key = 2, index = 2) और target index 0 की तुलना index tie-breaker के कारण Less बनेगी
• इस search के सफल होने के लिए stored index का खोजे जा रहे index से वास्तव में मेल खाना जरूरी है
• tie-breaker गलत item matching को रोकता है, लेकिन यह हमेशा सही item मिल ही जाएगा, इसकी गारंटी नहीं देता
• B-tree key के आधार पर sorted है, और tie-breaker index की तुलना करता है, इसलिए दोनों order आम तौर पर स्वतंत्र होते हैं
• यदि tree search विफल हो जाए, तो user code को call किए बिना B-tree में उस index को हटाने के लिए linear scan किया जाता है
• यह fallback removal operation को logarithmic time की जगह linear time बना देता है, लेकिन यह केवल buggy user code होने पर ही पहुँचा जा सकता है, इसलिए इसे स्वीकार्य trade-off माना गया

validation की परतें

• क्योंकि iddqd को foundational data structure की तरह इस्तेमाल किया जाता है, इसलिए इसमें analytical review और कई प्रकार की empirical validation साथ में की जाती है
• हर unsafe block और unsafe pattern का एक से तीन Rust लेखक और reviewer विश्लेषण करते हैं
• हर unsafe block के ऊपर // SAFETY: comment में reasoning लिखी जाती है, और Clippy का undocumented_unsafe_blocks lint comment की मौजूदगी जाँचता है
• example-based tests map बनाकर operations चलाते हैं और फिर results जाँचते हैं; iddqd में internal unit tests और public API integration tests दोनों हैं
• यही tests doctest के रूप में भी मौजूद हैं, इसलिए वे documentation का काम भी करते हैं
• pathological tests buggy Ord और अन्य trait implementations प्रदान करते हैं
• CI में regular tests और pathological tests दोनों को Miri के तहत चलाया जाता है ताकि कई प्रकार के UB का पता लगाया जा सके
• duplicate index नहीं होने चाहिए जैसे invariants को Miri के बाहर सामान्य test environment में भी जाँचा जा सकता है

model-based testing और fault injection

• iddqd randomized testing की दो परतें इस्तेमाल करता है: सही oracle से तुलना करने वाली model-based testing, और उसके ऊपर fault injection
• model-based testing, या stateful property-based testing, किसी type instance पर random operation sequences चलाती है और result की तुलना ज्ञात रूप से सही oracle से करती है
• iddqd एक अक्षम लेकिन साफ-साफ सही NaiveMap oracle के आधार पर व्यापक model-based tests चलाता है
• fault injection user code में bugs को random तरीके से डालने की तकनीक है; iddqd में panic safety खास तौर पर एक प्रभावी axis साबित हुई
• यदि operation के बीच user code panic भी कर दे, तब भी map के invariants नहीं टूटने चाहिए
• हर map operation में random panic countdown जोड़ा जाता है, और हर user-code call पर countdown को 1 घटाया जाता है; 0 होने पर panic कराया जाता है, जिससे random panic-safety testing की जाती है
• इस तरीके ने iddqd में कई subtle bugs खोजे, जिनमें से कुछ unsoundness तक ले जाते थे
• model-based tests हर operation के बाद no-duplicate-index जैसे internal invariants भी verify करते हैं
• model-based tests Miri के तहत चलाने के लिए बहुत धीमे हैं, इसलिए soundness और correctness जिन invariants पर निर्भर हैं, उन्हें अलग से जाँचा जाता है

LLM adversarial review और formal techniques

• current-generation frontier models ने map को corrupt करने वाली कई pathological user-code implementations खोज निकालीं
• एक notable case में LLM ने ऐसा path तैयार किया जिसमें custom allocator panic करता है और unwind के दौरान map invariants टूट जाते हैं
• यह मौजूदा panic-safety tests द्वारा कवर किए गए Ord implementation जैसे सामान्य user-code panics से अलग तरह की panic-safety समस्या थी
• LLM plausible लेकिन गलत soundness claims भी बना सकता है, इसलिए Miri को oracle बनाकर red-green TDD एक रक्षा तंत्र बनता है
• soundness bug के मामले में पहले Miri के तहत UB दिखाने वाला test बनाया जाता है, फिर fix के बाद यही test पास होता है या नहीं, यह दोबारा जाँचा जाता है
• Kani जैसे model checker से map invariants साबित करने का तरीका iddqd के लिए बहुत जटिल हो जाता है, क्योंकि आवश्यक proofs इतने बड़े हो जाते हैं कि tool उन्हें संभाल नहीं पाता
• Creusot यह साबित करने में मदद कर सकता है कि Rust code panic और अन्य errors से मुक्त है, लेकिन user code के panic करने या गलत व्यवहार करने पर भी जो invariants बने रहने चाहिए, उन्हें यह अभी साबित नहीं कर सकता
• NaiveMap iddqd के सबसे निकट specification की भूमिका निभाता है, और CI में model-based tests को हजारों बार चलाकर implementation के specification से मेल खाने पर उच्च भरोसा पाया जाता है
• cargo-anneal एक विकसित हो रहा tool है जो unsafe Rust के बगल में doc comments में Lean soundness proof रखने की सुविधा दे सकता है, इसलिए यह रुचि का विषय है
• iddqd के पास स्पष्ट invariants और सीमित लेकिन तुच्छ न होने वाला scope है, इसलिए यह formal verification tools के benchmark candidate के रूप में उपयुक्त है

निष्कर्ष

• unsafe generic Rust अत्यंत कठिन है, क्योंकि हर invariant को बनाए रखने के लिए arbitrary trait implementations और adversarial implementations तक को ध्यान में रखना पड़ता है
• iddqd का bug दिखाता है कि pathological Ord implementation map को धोखा देकर एक ही memory पर mutable alias बना सकती है
• कोई एक तकनीक सभी bugs नहीं पकड़ सकती, इसलिए इंसानी line-by-line unsafe reasoning, example-based tests, pathological tests, randomized tests, और frontier-model adversarial review को साथ में उपयोग किया जाता है
• Oxide का मानना है कि foundational infrastructure में इस स्तर की सख्ती उचित है

[GN⁺]

Lobste.rs की राय

• अगर मैं सही समझ रहा हूँ (मैं सफर में था इसलिए फोन पर देखा), तो यह wrapper type और HashMap/BTreeMap की जगह HashSet/BTreeSet इस्तेमाल करके हल होता हुआ लगता है
  wrapper type बिल्कुल ज़रूरी नहीं है, लेकिन safety और आगे के maintenance को देखते हुए यह अच्छा विकल्प है
  ज़रूरत सिर्फ ऑब्जेक्ट को लपेटने वाले 0-size wrapper की है, और उसमें ऐसा custom PartialEq/Hash implementation डालना है जो सिर्फ उन fields को देखे जिनमें दिलचस्पी है। पूरे value को बनाए बिना search करने के लिए value type के लिए AsRef implement करने वाला दूसरा type बनाया जा सकता है
  यह unsafe के बिना मौजूदा HashSet/BTreeSet interface को ज्यों का त्यों reuse करने का तरीका है। value/key type को wrap करने के बजाय, ऐसा व्यवहार उपलब्ध कराने वाला नया HashSet/BTreeSet wrapper भी बनाया जा सकता है

  • यहाँ key, record type के fields और subfields के मनचाहे संयोजन से बना है, और इसे GAT से व्यक्त किया गया है। साथ ही integer index/slab pattern को multi-index map में भी स्वाभाविक रूप से generalize किया जाता है
    इसमें Entry API, mutable access/iteration जैसी चीज़ें भी हैं। iddqd के भीतर mutability को काफ़ी सावधानी से संभाला जाता है, और कुछ जगहों पर interior mutability की अनुमति देने के लिए atomic values का उपयोग किया जाता है। index indirection के बिना इसे संभालना काफ़ी कठिन होता

• अगर iddqd का formal verification करना हो, तो शुरुआत में मैं शायद Kani जैसे model checker से यह साबित करने की कोशिश करता कि map अपने internal invariants को नहीं तोड़ता। लेकिन यह बात दिलचस्प लगी कि iddqd, Kani के संभालने के लिए थोड़ा जटिल है, और ज़रूरी proofs इतने बड़े हो जाते हैं कि tool उन्हें व्यावहारिक रूप से संभाल नहीं पाता
  क्या आप इस हिस्से के बारे में थोड़ा और साझा कर सकते हैं? क्या आपका मतलब है कि algorithmic complexity worst case में degrade हो जाती है?
  कुल मिलाकर यह formal methods का एक दिलचस्प case study है, और अच्छा लगा कि आपने इस हिस्से को छुआ। मौजूदा formal verification tools को देखकर, खासकर बड़े प्रोजेक्ट्स में उनकी success stories के आधार पर, कोई भोलेपन में सोच सकता है कि कम-से-कम data structure correctness जैसी चीज़ें तो साबित की जा सकती होंगी; लेकिन वास्तव में data structure के हिसाब से कठिनाई बहुत अलग-अलग होती है, और यह काम उन भाषाओं में भी व्यावहारिक रूप से आसान नहीं है जिन्हें Rust जैसी unrestricted aliasing वाली भाषाओं की तुलना में proof-friendly माना जाता है
  थोड़ा off-topic है, लेकिन यह भी जानना चाहूँगा कि diagrams कैसे बनाए गए। क्या आपने कोई one-off script लिखी थी, या वे Oxide ब्लॉग/वेबसाइट design के हिसाब से specially crafted चीज़ें हैं? वे किसी general-purpose tool की output जैसी नहीं लगतीं

  • लेख के नीचे “Diagrams courtesy Ben Leonard.” लिखा है, और Ben Leonard Oxide के designer हैं। इसलिए लगता है कि ये शायद hand-made diagrams हैं
  • किसी ठोस और सही ढंग से काम करने वाले trait implementation के लिए भी बहुत बुनियादी बात साबित करने की कोशिश की, लेकिन CBMC बस CPU चलाता रहा और 10 मिनट से ज़्यादा बीत जाने पर भी खत्म नहीं हुआ
    मैंने scope कम करने की भी कोशिश की। उदाहरण के लिए hashbrown को सही मान लिया, लेकिन उससे भी बहुत फ़र्क नहीं पड़ा। उस बिंदु पर मैं लगभग हार मान चुका था। ठीक से काम करने वाले trait implementations के लिए मुझे काफ़ी भरोसा है कि iddqd सही है, और formal methods में मेरी असली दिलचस्पी तो उस proof में थी जो मनमाने, गलत तरीके से काम करने वाले implementations के लिए भी लागू हो
    हालाँकि मैं Kani का सबसे अच्छा उपयोगकर्ता नहीं हूँ। अगर आप या कोई और इसे आज़माए, तो मुझे सच में अच्छा लगेगा
    diagrams के लिए पहले Mermaid में sketch बनाया गया, फिर शानदार designer Ben Leonard ने उसे हमारे color palette और theme के अनुसार हाथ से polish किया

• किसी object को उसके अपने ही किसी field को key बनाकर index करने वाला field-based map pattern, C# में भी ऐसा है जिसे मैं हमेशा उपलब्ध देखना चाहूँगा
  मैंने पहले खुद इसका एक simple version बनाने की कोशिश की थी, लेकिन interface बहुत साफ़ नहीं लग रहा था, इसलिए छोड़ दिया। यह लेख देखकर फिर से कोशिश करने का मन हो रहा है

  • हाँ, यह सच में बहुत उपयोगी pattern है। मैंने इसे कंपनी के काम की ज़रूरत के कारण बनाया था, लेकिन बाद में cargo-nextest जैसे production codebase से लेकर personal projects तक हर तरह की जगहों पर इसका उपयोग किया
    सिर्फ एक field को key की तरह इस्तेमाल करना सबसे आम use case है, लेकिन iddqd इतना flexible है कि field, subfield, या field से pure और सस्ते तरीके से compute होने वाले function के किसी भी combination को इस्तेमाल किया जा सकता है। उदाहरण के लिए https://docs.rs/iddqd/latest/iddqd/ में ArtifactKey खोज सकते हैं (अगर आप Rust syntax से परिचित नहीं हैं तो क्षमा करें)
    iddqd design करते समय मेरे मन में यह बहुत मज़बूत विचार था कि users को Rust type system की पूरी ताकत इस्तेमाल करने में सक्षम होना चाहिए, चाहे library author के रूप में मुझे कितने भी workarounds क्यों न करने पड़ें। मैं सच में चाहता था कि iddqd, users के लिए, खासकर मेरे सहकर्मियों के लिए, एक आनंददायक library बने