mimalloc

[waywardmonkeys]

In #6020, the suggestion of using mimalloc was raised.

That seems potentially interesting to me, so I have a couple of questions about getting started:

• How would you like to integrate the mimalloc source code? Via a git submodule or copy the sources into the Z3 repository or allow it optionally using an externally provided copy?
• Related to the last, should it be optional with a bunch of #ifdef's or just make the leap and use mimalloc directly and fully within the memory manager?
• Should this be restricted to the memory manager code or also get used directly within the small object allocator?
• Is there interest in cleaning up some of the allocation APIs once mimalloc is used, like using global new / delete operators, rather than some of the existing alloc / dealloc things?
• What's the best way of measuring performance differences (other than perhaps time ./test-z3 -a)?
• Are features in the code like PROFILE_MEMORY or the location of allocations (file name and line number) used much (or at all)?

[NikolajBjorner]

• How would you like to integrate the mimalloc source code? Via a git submodule or copy the sources into the Z3 repository or allow it optionally using an externally provided copy?

I thought copying a snapshot and put it as subdirectory under util.

• Related to the last, should it be optional with a bunch of #ifdef's or just make the leap and use mimalloc directly and fully within the memory manager?

leap

• Should this be restricted to the memory manager code or also get used directly within the small object allocator?

We tried using mimalloc as replacement for small object allocator a couple of years ago.
It didn't present any measurable improvement, but neither degradation as I recall. It is lower risk to not touch this. We would have to benchmark.

• Is there interest in cleaning up some of the allocation APIs once mimalloc is used, like using global new / delete operators, rather than some of the existing alloc / dealloc things?

lower priority. I see the issue of why using these obscure names.

• What's the best way of measuring performance differences (other than perhaps time ./test-z3 -a)?

I run against SMTLIB benchmarks on benchmarking infrastructure.

• Are features in the code like PROFILE_MEMORY or the location of allocations (file name and line number) used much (or at all)?

I don't use these for a while. I use general memory profiling tools. They have been used on occasion to chase bugs. It isn't important.