Force GC to run

Stream: metaprogramming / tactics

[Leni Aniva]

Is there a way to force Lean's GC to run to avoid out of memory problems?

[Henrik Böving]

Lean does not have a garbage collector. The system is based on ref counting and frees memory when the compiler thinks the right time for freeing memory is. In particular the reference counting is guaranteed to be garbage free by construction.

[Sebastian Ullrich]

(do make sure you're on 4.24.1/4.25.2/4.26.0-rc2 or above!)

[Gavin Zhao]

Sebastian Ullrich said:

(do make sure you're on 4.24.1/4.25.2/4.26.0-rc2 or above!)

Just curious what's the context for these versions? Some critical bugs fixed or major ref counting improvements?

[Henrik Böving]

We identified and fixed a few major and minor memleaks in those patches

[Leni Aniva]

Could there be any memory leaks regarding Lean strings? I have a test case where elaborating thousands of expressions leads to OOM and std::bad_alloc

[Henrik Böving]

I did also fix two memory leaks in the string subsystem in those versions yes

[Henrik Böving]

But in these patch versions we know all major memory leaks and I think at least most minor ones to be absent according to lsan

[Leni Aniva]

If I run the elaborator many times do I need to manually clear out any caches?

[Sebastian Ullrich]

As long as you don't run importModules many times, there shouldn't be anything to do. If you can find a reproducer of any suspect behavior, we would certainly be interested in that though.

[Leni Aniva]

Sebastian Ullrich said:

As long as you don't run importModules many times, there shouldn't be anything to do. If you can find a reproducer of any suspect behavior, we would certainly be interested in that though.

I managed to repro the behaviour here: https://codeberg.org/aniva/lean4-reverse-ffi

The failure is at iteration > 80000, and I could not get it below say 10 iterations.

Iteration 79000
Iteration 80000
Iteration 81000
libc++abi: terminating due to uncaught exception of type std::bad_alloc: std::bad_alloc

I also tried creating the STRef's per iteration to eliminate any cache problems, but the issue persists.

[Sebastian Ullrich]

Ah, FFI does add complexity. Could you try downloading an fsanitize build from our CI and build the C file using -fsanitize=address as well to get started?

[Henrik Böving]

The most obvious thing that jumps out at me is that you are using the IO and BaseIO API in a wrong way in the C code. With IO RealWorld removed there is no need to pass along real world parameters and there is also no need to do things like unwrapping the result of an st_mk_ref, it is directly the lean object without boxing.

[Leni Aniva]

Henrik Böving said:

The most obvious thing that jumps out at me is that you are using the IO and BaseIO API in a wrong way in the C code. With IO RealWorld removed there is no need to pass along real world parameters and there is also no need to do things like unwrapping the result of an st_mk_ref, it is directly the lean object without boxing.

ah I didnt know that was removed.

cat $(lean --print-prefix)/include/lean/lean.h | grep st_mk_
LEAN_EXPORT lean_obj_res lean_st_mk_ref(lean_obj_arg, lean_obj_arg);

It seems like st_mk_ref still takes a world argument here? I'm on 4.25.2. If I pass in just one arg to this function there would be a compilation error. If I remove the unwrap after lean_st_mk_ref the program crashes on iteration 0.

[Leni Aniva]

Sebastian Ullrich said:

Ah, FFI does add complexity. Could you try downloading an fsanitize build from our CI and build the C file using -fsanitize=address as well to get started?

Is there a way to do it with elan?

[Henrik Böving]

Oh the IO realworld removal is a 4.26 feature, my bad

[Sebastian Ullrich]

Leni Aniva said:

Sebastian Ullrich said:

Ah, FFI does add complexity. Could you try downloading an fsanitize build from our CI and build the C file using -fsanitize=address as well to get started?

Is there a way to do it with elan?

No. And it is only available on recent master, so it would require the changes Henrik mentioned first

[Leni Aniva]

Sebastian Ullrich said:

Leni Aniva said:

Sebastian Ullrich said:

Ah, FFI does add complexity. Could you try downloading an fsanitize build from our CI and build the C file using -fsanitize=address as well to get started?

Is there a way to do it with elan?

No. And it is only available on recent master, so it would require the changes Henrik mentioned first

is there any instructions on how to do this? I couldn't find it in contributing.md

[Sebastian Ullrich]

To be completely transparent, I don't think this has been tried before by anyone in combination with FFI so I can only provide guesses for now. But if we do suspect a true memory leak, the sanitizer is the most promising approach in my experience.

[Sebastian Ullrich]

I guess I was a bit too pessimistic about elan: when you've downloaded the toolchain, you can certainly add it via elan toolchain link

[Leni Aniva]

Sebastian Ullrich said:

To be completely transparent, I don't think this has been tried before by anyone in combination with FFI so I can only provide guesses for now. But if we do suspect a true memory leak, the sanitizer is the most promising approach in my experience.

where can I find the nightly fsanitize builds?

[Sebastian Ullrich]

Argh my bad, we do not actually upload an artifact for the sanitized build right now. So you would have to build Lean from source, using cmake --preset sanitize. This may be better/necessary in any way because it allows you to ensure Lean and your C code are built with the same compiler and sanitizer version

[Sebastian Ullrich]

If you could make the C changes to make the code compatible with master, I can look into sanitizer part as well, though likely not in the next few days

[Leni Aniva]

Sebastian Ullrich said:

If you could make the C changes to make the code compatible with master, I can look into sanitizer part as well, though likely not in the next few days

I'll see what I can find on 4.25.2 for now. Has there been any significant modification about memory since 4.25.2?

[Sebastian Ullrich]

We've identified and fixed additional small leaks found by the sainitizer but no indication elaboration of usual Lean files was affected so far

[Leni Aniva]

Sebastian Ullrich said:

Argh my bad, we do not actually upload an artifact for the sanitized build right now. So you would have to build Lean from source, using cmake --preset sanitize. This may be better/necessary in any way because it allows you to ensure Lean and your C code are built with the same compiler and sanitizer version

I got this error after

cmake --preset sanitize
make -C build/sanitize
elan toolchain link sanitize build/sanitize/stage1
elan default sanitize

/home/aniva/Projects/contrib/formalization/lean4/src/runtime/compact.cpp:400:66: runtime error: addition of unsigned offset to 0x776b21dee858 overflowed to 0x776b21de4ae0
SUMMARY: UndefinedBehaviorSanitizer: undefined-behavior /home/aniva/Projects/contrib/formalization/lean4/src/runtime/compact.cpp:400:66
✖ [6/7] Building mystery:shared
trace: .> cc -shared -o /home/aniva/Projects/contrib/formalization/lean4-reverse-ffi/.lake/build/lib/libmystery.so /home/aniva/Projects/contrib/formalization/lean4-reverse-ffi/.lake/build/ir/Mystery/Basic.c.o.export /home/aniva/Projects/contrib/formalization/lean4-reverse-ffi/.lake/build/ir/Mystery.c.o.export -L /home/aniva/Projects/contrib/formalization/lean4/build/sanitize/stage1/lib/lean -lstdc++ -Wl,--as-needed -lLake_shared -Wl,--no-as-needed -fsanitize=address,undefined -fsanitize-link-c++-runtime /usr/lib/libgmp.so -L/usr/lib -luv -lm -ldl -pthread
info: stderr:
cc: error: unrecognized command-line option ‘-fsanitize-link-c++-runtime’
error: external command 'cc' exited with code 1
Some required targets logged failures:
- mystery:shared
error: build failed

[Sebastian Ullrich]

Ah, that's pretty far already! It does sound like this isn't the same C compiler cmake chose for Lean. You can check that using

cmake -LA build/sanitize/stage1 | grep CMAKE_C_COMPILER:

[Sebastian Ullrich]

Note that the ub warning in your output is fixed by https://github.com/leanprover/lean4/commit/72573928b1bc73eb80aa54477333039028fb4366#diff-3c4090168b45d2755473a9a29bb956bdf0b9fe2dd98f3e4d77170b8dd7c5c4cbR400. You might need to backport that and the subsequent diff if they obscure the actual leak analysis.

[Leni Aniva]

Sebastian Ullrich said:

Ah, that's pretty far already! It does sound like this isn't the same C compiler cmake chose for Lean. You can check that using

cmake -LA build/sanitize/stage1 | grep CMAKE_C_COMPILER:

I'll take a look at this later when I have more time. The equivalent code in Lean doesn't crash:

https://codeberg.org/aniva/lean4-reverse-ffi/src/branch/main/Main.lean

[Leni Aniva]

Sebastian Ullrich said:

If you could make the C changes to make the code compatible with master, I can look into sanitizer part as well, though likely not in the next few days

I updated the example to v4.26.0. It now crashes on iteration 114k instead of 81k.

[Leni Aniva]

Sebastian Ullrich said:

If you could make the C changes to make the code compatible with master, I can look into sanitizer part as well, though likely not in the next few days

I updated the example to v4.26.0. It now crashes on iteration 114k instead of 81k.

[Sebastian Ullrich]

And were you able to make progress on the sanitized build as well?

[Leni Aniva]

Sebastian Ullrich said:

And were you able to make progress on the sanitized build as well?

no sorry I have been pretty busy