Lean.CompactedRegion memory management

Stream: lean4

[Joachim Breitner]

Is the following understanding of pickle correct?
The Lean.CompactedRegion returned from unpickle can be used to free the region, using Lean.CompactedRegion.free.
As long as this is not called explicitly, the compact region stays around.
Dropping the last reference to the Lean.CompactedRegion object does not free the region. In particular, if I don’t plan to free the region, I don’t need to keep the Lean.CompactedRegion value around.
Freeing the region (explicitly) is dangerous if there still is some reference to values in it, as they will now point to unmapped or even unrelated memory.

[Sebastian Ullrich]

Yes!

[Joachim Breitner]

Thanks! So mathlib4#7305 isn’t bogus :-)

I’m reading through the module loading code, and unless I am mistake, it only uses mmap if it can manage to import the .olean at the same position it was when it was serialized? Ah, it uses a random base base address when creating the .olean. That’s kinda amusing :-)

[Joachim Breitner]

Did you consider to only have relative pointers in data structures, so that compacted regions would be relocatable? But guess if this scheme works, then why bother.

[Sebastian Ullrich]

Yes, collisions are not a concern in 64 bit address space. Doing additional pointer calculations just for that doesn't sound pretty.