That 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.
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=...