Skip to content

Excessive allocations during map join #1967

@sim642

Description

@sim642

I reported this originally just on Zulip, so I was confused when I started looking for this non-existent issue on GitHub.


When I turned hashconsing off, then that disappeared and a lot of time was spent on Ocaml GC internals instead.

So I tried looking into the large amount of garbage using Memtrace and found out that the branch of base analysis was doing over 90% of the allocations. The issue there seems to be the refinement via ambiguous pointers which was implemented in #1659.

The problem is that this joins base domain maps which will lead to a lot of allocations for the join of each of the values. But in that particular case, each joinee only differs from the original in 1-2 variable keys, so the entire operation should not depend on the size of the map. This could possibly be implemented more efficiently by joining some partial maps or so. Seems like we never benchmarked this precision improvement.

This would also be a problem for #1531. The idea there was to make the writing of ambiguous pointers more intuitive (a join over all the cases) but it also introduces joins on the entire maps. So perhaps it's not a good idea to be so naive.

This is particularly wasteful because usually the refining of ambiguous pointers means nothing is refined. And the joins are a roundabout way to refine the original state in various ways and join them back together into the original state...

Metadata

Metadata

Assignees

No one assigned

    Type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions