Skip to content

Conversation

@SchrodingerZhu
Copy link
Contributor

@SchrodingerZhu SchrodingerZhu commented Aug 18, 2023

@digama0 So, parking_lot still requires std, which is annoying. This PR provides a potential fix.

However, I suggest we should completely remove the *_locked things. It is hardly useful to provide such locked routines. Users cannot call it multiple times, even if it is locked. Users still struggle to maintain the status to check if Lean is already initialized. Also, the user may initialize their own pieces between lean_initialize and io_mark_end_initialization, where exclusivity is required during the whole time, but these *_locked things simply release the lock after the first function call.

// Why not just mark `lean_initialize_runtime_module` as `MT-unsafe` and let users use their own lock?
pub(crate) fn initialize_runtime_module_for_tests() {
        let _guard = LEAN_INIT_MUTEX.lock();
        if !INITIALIZED.load(std::sync::atomic::Ordering::SeqCst) {
            unsafe {
                lean_initialize_runtime_module();
            }
            INITIALIZED.store(true, std::sync::atomic::Ordering::SeqCst);
        }
    }

As in this low-level lean-sys, I think just providing the unsafe initialization routine is fine.

@SchrodingerZhu SchrodingerZhu changed the title remove std dep from init DO NOT MERGE: remove std dep from init Aug 18, 2023
@SchrodingerZhu SchrodingerZhu changed the title DO NOT MERGE: remove std dep from init Remove locked routines Aug 22, 2023
@SchrodingerZhu
Copy link
Contributor Author

@digama0 I change this PR to remove *_locked initializations. I also found a problem in previous tests where initialization can be called multiple times. At least for small_allocator, such repeated initialization means that previously allocated pages are leaked.

@SchrodingerZhu SchrodingerZhu marked this pull request as draft August 23, 2023 00:52
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant