mit-plv / bedrock2

A work-in-progress language and compiler for verified low-level programming
http://adam.chlipala.net/papers/LightbulbPLDI21/
MIT License
297 stars 45 forks source link

Crit-bit Trees: Lookup, Insert, Delete #399

Closed vfukala closed 9 months ago

vfukala commented 9 months ago

This PR focuses on the verified implementation of crit-bit trees, which is part of the repository as a LiveVerif example.

This PR is a partial rewrite of the previous implementation. The new implementation should be more maintainable and extensible. Further, this PR

samuelgruetter commented 9 months ago

This looks great :tada: My only concern is why cbt_insert has a suspicious * fun _ => True }> m' in the postcondition. This line was already merged, and I think I already asked this question. IIRC, it was for the case where you need to allocate two new nodes, and allocating the first one succeeds, but allocating the second one fails? Then, you'd want to free the first, but you can't because to free something, you need an allocator, but you only have an allocator_failed_below 12. Does that sound right? This is not specific to critbit trees, but should be solved in the malloc library -- though I don't quite know how yet...

vfukala commented 9 months ago

This looks great 🎉 My only concern is why cbt_insert has a suspicious * fun _ => True }> m' in the postcondition. This line was already merged, and I think I already asked this question. IIRC, it was for the case where you need to allocate two new nodes, and allocating the first one succeeds, but allocating the second one fails? Then, you'd want to free the first, but you can't because to free something, you need an allocator, but you only have an allocator_failed_below 12. Does that sound right? This is not specific to critbit trees, but should be solved in the malloc library -- though I don't quite know how yet...

Thanks for looking at this and yes, all that sounds right!

~How much do you think is fixing this worth? At bottom, I think the issue is that the way the allocator is currently used doesn't properly capture the fact that we actually request 12+12 bytes of memory at once (as a single transaction that should ideally either completely succeed or completely fail).~

~One way of going around this would be to instead just call Malloc(24) to allocate both nodes in cbt_insert. How does that sound to you?~ (Nevermind, the above doesn't work because we need to be able to later free the two nodes independently. We need one freeable predicate for each of the two nodes.)