4 ms·
> It's a good candidate for formal proof of correctness - not too big, and critical to system operation. Unfortunately, having actually looked for production s
by Jweb_Guru 11y ago
> It's a good candidate for formal proof of correctness - not too big, and critical to system operation.
Unfortunately, having actually looked for production strength proofs of correctness for production allocators (as opposed to toys), I wasn't able to find any. Given how high-value of a target they are for formal verification, we may be underestimating the complexity of doing so.
- Animats 11y agoSuccesses have been claimed.[1] It's discouraging to me how little progress there's been in proof of correctness in the last 35 years. I used to work on that stuff. C set the field back by decades. [1] https://books.google.com/books?id=yvJqCQAAQBAJ&pg=PA364&lpg=PA364&dq=proof+of+correctness+of+allocator+-register&source=bl&ots=6pb3WuMRxe&sig=D-ak6RzvT7fKwWZL5S4sKFycJcM&hl=en&sa=X&ei=adVnVd7rKsLaoAT04IOADw&ved=0CB4Q6AEwAA#v=onepage&q=proof%20of%20correctness%20of%20allocator%20-register&f=false https://books.google.com/books?id=yvJqCQAAQBAJ&pg=PA364&lpg=...
- Jweb_Guru 11y agoThat was one of the "toy" implementations I mentioned. The algorithm they described is going to be nowhere near the performance of a modern multithreaded allocator like jemalloc (which is correspondingly far more complex). Which is not to say things like that are not encouraging, only that I was hoping someone would have proven something people actually use correct.