Performance fix for removing elements from doubly linked lists#59
Performance fix for removing elements from doubly linked lists#59mmottl wants to merge 1 commit intojanestreet:masterfrom
Conversation
|
Markus, it might be more natural to pick these PRs back up once we have 4.04 in-house and can test the performance improvements. By then, it should also be easier to run tests externally. Do you mind holding off on these? |
|
Actually, the above fix is not related at all to the GADT-improvement. It should work with older OCaml versions and also offers the largest performance improvement by far. I don't have plans for other patches anytime in the near future anyway. It should be quite easy to rebase the already submitted ones for later releases based on 4.04. |
|
Ah, that's an excellent point. Sorry for the confusion. @rnml, can you take a look at this PR? |
|
I'm working to get this into core_kernel now |
|
Closing, as the changes have made it into a release. |
4 participants
While implementing the GADT-improvement for doubly linked lists I came across this apparently highly significant performance bug. Removing elements from doubly linked lists basically allocates a lot of stuff needlessly: list headers that are never needed, which again require allocation of union-find data structures.
I have tested the patch below, which only changes three lines of code, and seen performance improvements for realistic, if not to say frequent, use cases close to 100% - not just for the removal operation, for the whole benchmark! E.g.
insert_firsta couple of million elements into a doubly linked list and then remove them again (removed in reverse order, as tested).Note that this change makes the GADT-improvement relatively more valuable (almost twice as much), too.
The reason why the patch should be safe is that the dummy header is never used in active lists. This makes any union find comparison between the dummy header and active headers fail as required. There is no place in the code where two previously removed elements with dummy headers could interact without being tested against a live header. Hence there should not be any semantic difference.