Expose thread management routines to FFI?

Stream: lean4

[Schrodinger ZHU Yifan]

@Mario Carneiro Sorry to bring up this again. I did not mention that in the group chat, so I am writing this to share my concerns.

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.

[Henrik Böving]

The thread API isnt meant for public consumption. A task is completely different from a thread. Tasks are scheduled on a thread pool and do not get preempted by other tasks in their execution. So if you have 8 tasks running and they are just all doing say a heavy computation all of the other tasks will starve.

I didn't try this yet but the task API is linked into lean via @extern, is it not already callable from FFI? If it isnt then we probably should make it so.

(That said I believe that the behavior of the current task implementation is not a very nice concurrency primitive at all but that's just my opinion)

[Mario Carneiro]

this is about threads, not tasks

[Mario Carneiro]

the issue is that there are some thread locals that can't be initialized from a thread which was not created by lean (and these thread locals are necessary for the lean allocator to work, so you can't call any lean code on the thread otherwise)

[Mario Carneiro]

currently lean_initialize() is exposed but not lean_thread_initialize()

[Henrik Böving]

But why would the FFI want to spawn a lean thread in the first place if tasks are supposed to be the primitive?

[Mario Carneiro]

it's not spawning a lean thread

[Mario Carneiro]

it's running lean code on a pre-existing thread (which was spawned by not-lean)

[Mario Carneiro]

Also, I don't think lean has jurisdiction over what a "primitive" is when interacting over FFI. If you are e.g. linking to curl, you can't just tell it not to use threads

[Mario Carneiro]

I'm pretty sure the current set of exposed functions was just a historical accident of what was actually used in FFI projects thus far. I mean, initialize is exposed but finalize isn't, this makes no sense

[Mario Carneiro]

lean4#2464

[Schrodinger ZHU Yifan]

For instance,

 #[test]
    fn type_with_allocations() {
        initialize_thread_local_runtime();
        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 a  wrapper around `*mut lean_object`.
                    let res: usize = closure.invoke(1 << z);
                    assert_eq!(res, (x * y) ^ (1 << z))
                }
            }
        }
    }

One may want to write test cases in Rust involving allocations in lean routines. In order for this to work, the thread-local heap (local pages) must be initialized.