RFC: thread initialization FFI

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Currently, thread-level initialization does not have C interfaces. This makes spawning or initializing lean threads infeasible in the FFI environment. I wonder if some or all of the following functions can be exposed:

namespace lean {
  void initialize_thread();
  void finalize_thread();
  
  typedef void (*thread_finalizer)(void *); // NOLINT
  void register_post_thread_finalizer(thread_finalizer fn, void * p);
  void register_thread_finalizer(thread_finalizer fn, void * p);
  void run_thread_finalizers();
  void run_post_thread_finalizers();
  void delete_thread_finalizer_manager();
  bool in_thread_finalization();
  void reset_thread_local();
}

Steps to Reproduce

N/A

Versions

N/A

Additional Information

Let us say we want to run test cases for lean API bindings in Rust. Then, we actually need to provide a way to at least initialize the thread-local heaps. Otherwise, it can be really hard to test such functions in parallel.

Another way to workaround this is to only expose APIs to spawn a lean task/thread. If one wants to run anything in a foreign language (assuming lean_initialize is called), the user spawns a thread/task to run it; but this method itself is heavy and less customizable.

As a motivating example, let's consider we want to write a unit test for the rust ffi wrappers that create a lean closure (or any heap object) on rust side:

 #[test]
    fn type_with_allocations() {
        initialize_local_heap();
        for x in 0..10 {
            for y in 0xFFFFFFE0..0xFFFFFFFF {
                for z in 0..64 {
                    let closure = lean_closure! {
                        [x : usize, y : usize] | z : usize | -> usize {
                        (x * y) ^ z
                    }}; // this closure is just a wrapper around `*mut lean_object`.
                    let res: usize = closure.invoke(1 << z);
                    assert_eq!(res, (x * y) ^ (1 << z))
                }
            }
        }
    }

In order to make the test case functional, we need to initialize the thread local heap via some function (here we call it initialize_local_heap. The only capable exposed functions are lean_initialize_runtime_module and lean_initialize. However, both functions are program-level function that touches global variables. Without exposed thread-level APIs, it is hard to set up the memory resource outside Lean. Although one can split the tests into individual programs or try to manage the tests from lean, it is not that handy.

I copied a link to a previous FFI wrapper created by someone else as another example, where they wrote an experimental binding between lean and the async runtime in Rust. So, even in the case we are not creating executables from FFI, the FFI function being called from lean may spawn threads. Here they used lean_initialize_runtime_module as thread-level initialization, which was wrong, but it shows that we need proper API to do such things.

https://github.com/LemonHX/lean4-rs/blob/d2064357140a31fab564058d83b95b5bb04940be/src/async_tokio.rs#L22

Start by locating the existing thread-level initialization and finalization entry points corresponding to the listed C++ functions, then compare them with lean_initialize_runtime_module and lean_initialize. Review the referenced async_tokio.rs example to understand the FFI use case. Done means agreeing on a supported thread-level API and validating it from a foreign-language binding.