iddqd, or the hardest kind of unsafe Rust
75 points by sunshowers
75 points by sunshowers
If I’m understanding this correctly (on my phone and on the go), this is solvable via a wrapper type and using HashSet/BTreeSet instead of HashMap/BTreeMap. (You don’t even need a wrapper type, but it’s a good call for safety/posterity).
All you need is a zero-size wrapper around the object that has a custom PartialEq/Hash impl that only looks at the field you care about. You can create a second type impl’ing AsRef for the value type to perform searches without a full value.
That’s to reuse the existing HashSet/BTreeSet interface as-is with no unsafe. Instead of wrapping the value/key type you can instead create a new HashSet/BtreeSet wrapper that does that for you.
Note that the key is an arbitrary composition of fields and subfields of the record type, expressed via a GAT. Also, the integer index/slab pattern generalizes nicely to multi-index maps.
There's lots of other things present too, like the Entry API and mutable access/iteration. There's careful handling of mutability within iddqd (in some places we use an atomic to allow interior mutability) that would be quite hard to do without the index indirection.
Oxide Computers seems like a pretty cool company, I've been following along for some time. I also greatly appreciate Doom references.
I'm not that well-versed in the Rust ecosystem, but @sunshowers posts are always a fun read regardless. :) And now I'm thinking on all the times that iddqd would have been really handy.
To formally verify iddqd, one’s first thought would be to use a model checker like Kani to establish that the maps don’t violate internal invariants. But iddqd is unfortunately a bit too complicated for Kani to handle, and the required proofs blow up beyond what is feasible for the tool.
Could you share more details about this? Is the point the computational complexity in the algorithms used degenerates into worst-case behavior?
This is an interesting case study overall for formal methods, I'm glad you covered that. One might naively think that existing formal verification tools would be able to at least prove the correctness of data structures (given successes at other large-scale projects), but turns out, not all data structures are equal, and doing proofs even in Rust (which I think is considered to be more amenable to proofs compared to languages which allow for unrestricted aliasing), is actually not that easy in practice.
Bit off-topic but I'm curious, how did you make the diagrams? Did you script something one-off? Seems like something special purpose to match the design of the Oxide blog/website, not something more generic.
Could you share more details about this? Is the point the computational complexity in the algorithms used degenerates into worst-case behavior?
Even trying to prove something basic against a concrete, well-behaved trait implementation just didn't complete within 10+ minutes with CBMC spinning its CPU. I tried restricting the scope (e.g. assuming hashbrown is correct) but that didn't go too far either. At that point I kind of gave up -- I'm pretty confident that iddqd is correct for well-behaved trait impls, and what I was really interested in with formal methods was proofs that hold over arbitrary, poorly-behaved ones.
I'm not the most competent at Kani, though; I'd love it if you or someone else had a go at this.
Bit off-topic but I'm curious, how did you make the diagrams? Did you script something one-off?
I made some sketches in Mermaid, then our extraordinary designer Ben Leonard turned those into diagrams by hand with our color palette and general theme.
Curious on if you had looked into Verus by any chance as well.
I did not, no.
I am very interested in collaborating with formal verification tool builders here, though I would like to aspire to proving the hardest part of the problem (adversarial trait impls + panics in user code). The existing validation makes me quite confident that iddqd is correct for both well-behaved user code and certain kinds of poorly-behaved user code. (There's a bunch I didn't talk about in the post, such as each operation that can panic being tagged with the state the map is left in afterwards, which is either Atomic or StepAtomic.) Thinking of formal methods as a tool in the toolbox, the main value they can add is proofs over kinds of adversarial trait impls that I haven't thought about.
Bit off-topic but I'm curious, how did you make the diagrams? Did you script something one-off? Seems like something special purpose to match the design of the Oxide blog/website, not something more generic.
The bottom of the post says "Diagrams courtesy Ben Leonard.", Ben Leonard being a designer at Oxide. So I think potentially handmade?
This pattern (a map of objects indexed by one of their fields as the key) is something I wish I had access to in C# all the time. I tried writing a simple one myself but it wasn't a super clean interface and I let it go. This article makes me want to take another crack at it though.
Yeah, it's a super useful pattern. I built it for needs we have at work but have ended up using it for all kinds of personal projects, from production codebases like cargo-nextest to things that are just for me.
Worth noting that while using just one of the fields as the key is the most common use case, iddqd is flexible enough that any combination of fields, subfields, or even pure/cheaply calculable functions of fields can be used. For example, search for ArtifactKey in https://docs.rs/iddqd/latest/iddqd/ (with apologies for the Rust syntax if you're not familiar with it). When designing iddqd I felt quite strongly that consumers should have the full power of the Rust type system available to them, no matter how many hoops I had to jump through as the library author. I very much want iddqd to be a pleasure for consumers (my coworkers!) to use.
Funnily enough, the first time I remember finding myself wanting this pattern, the TriHashMap would have actually been exactly what I was looking for.