One-bit Perceus

Stream: lean4

[Gabriel Barreto]

I don't know if this is the best place to ask this, but I know Lean uses the Perceus algorithm for implementing "functional-but-in-place". Perceus, however, is full refcounting, and no tracing. Refcounting has the issue of memory fragmentation and less locality. I wonder if instead, a one-bit refcounting Perceus is possible (the set bit means "we know this has unique reference"), to get all the benefit of FBIP with minimum overhead, and rely on a copying GC for the garbage that is not able to be freed by the refcounter, with the added benefit of compactification

[Gabriel Barreto]

The one-bit counter could be pointer tagged I think

[Leonardo de Moura]

Refcounting has the issue of memory fragmentation and less locality.

We have a special allocator too which uses free list sharding. https://www.microsoft.com/en-us/research/uploads/prod/2019/06/mimalloc-tr-v1.pdf
We believe it addresses these issues.

[Gabriel Barreto]

Thanks! I'm gonna read this and see if I understand it

[Gabriel Barreto]

I noticed too that in Perceus mutations can only happen for (saturated) constructors of the same size. Could it be extended to allow mutation of smaller values inside a bigger space? Say, when you pop an array. This would introduce what the GHC people call "slop", but I don't know if this would mess up the deallocator

[Sebastian Ullrich]

I'm not sure if that makes much sense for constant-sized types. But the Lean runtime does that for arrays, which have a size and capacity.

[Gabriel Barreto]

The idea would be to immediately reclaim a memory space, but this, of course, introduces fragmentation, or slop. This might be an overoptimization though, it might be better to just allocate a new space for the new value