Integrating with reference counting in C++

Stream: lean4

[Christian Pehle]

I have a slightly vague question: I'm trying to build a foreign function interface for a substantial C++ library based on the example here: https://github.com/leanprover/lean4/tree/master/tests/compiler/foreign and the lean-llvm project that I've found. The C++ library itself uses reference counting to keep track of allocated objects and ideally I would like to find a way to integrate that with the reference counting mechanism in Lean, is that something that is easily possible in the moment or would that require modifications to Lean itself?

[Joe Hendrix]

@Christian Pehle It's pretty straightforward. There is not -- as far as I know -- a way to reuse the existing reference count, but register_external_object_class, alloc_external and external_class/external_data should provide you with the functionality you need.
Folks at Galois wrote Lean 4 LLVM bindings that use these classes if you want example code.

[Christian Pehle]

Yes, I've seen these examples (also the Galois ones). I have now some initial code that seems to work. Is the annotation @& documented somewhere? What I understood from reading the source code is that on the C side this requires a b_lean_obj_arg as opposed to a lean_object. I get a segmentation fault if I invoke two different functions on the same object, but not if I invoke either one of them, I suspect this is because I'm misunderstanding the semantics.

[Mac]

If I am not mistaken @& parameter means 'pass-by-reference' instead of 'pass-by-value'. That is, when an object to a non -@& parameter is a copy owned by the function and thus it should free it (decrement its reference counter) when it is done with it. I @& is instead owned by the caller and thus the callee should not free it (unless it makes a new copy of the object by increment its reference counter).

[Joe Hendrix]

@Christian Pehle If I recall correctly, @& are used for "borrowed references". The semantics are described in this paper. Essentially, the caller does not increment the reference count when passing it into the function, so if you store the object anywhere, you need to increment the reference count

[Christian Pehle]

@Joe Hendrix, @Mac thanks, I've also found https://github.com/leanprover/lean4/blob/995136d46b7dc42c6175ef7f62d9e0e501e1eaf5/src/include/lean/lean.h#L128-L158, I still haven't quite wrapped my head around how this interacts with the reference counting of the C++ library. I guess @$ basically controls whether or when? the finalise function is called.

[Sebastian Ullrich]

external_object will keep the memory management separate, so you will have one Lean and one C++ reference counter. You store ownership of the C++ value in the external_object and release it in finalise, it really doesn't matter if that is a unique or shared C++ pointer or other resource.

[Christian Pehle]

Sebastian Ullrich said:

external_object will keep the memory management separate, so you will have one Lean and one C++ reference counter. You store ownership of the C++ value in the external_object and release it in finalise, it really doesn't matter if that is a unique or shared C++ pointer or other resource.

Just to clarify finalise is called when the Lean reference count goes to zero? I think I've figured out a way to keep the C++ invariants intact, by basically constructing/deconstructing an intrusive ptr, my initial motivation was to somehow shift / merge the reference counting work entirely with the one done by Lean, since you seem to be doing some intelligent tracking / elimination of reference count operations.

[Joe Hendrix]

Yes, finalize is called when the Lean external object goes to zero.

The approach I've taken with objects having a reference count is just to treat the Lean object as holding a single reference to the external reference regardless of how many Lean references there are to the Lean object.
This should typically be ok unless the external object is inspecting it's own reference count and doing destructive updates when it thinks it's reference count is one.