From 78058c5921c3dd61d84ca3174efc7848c0942780 Mon Sep 17 00:00:00 2001 From: Schrodinger ZHU Yifan Date: Fri, 18 Aug 2023 11:30:31 -0400 Subject: [PATCH 1/2] remote std dep from init --- Cargo.toml | 2 +- src/alloc.rs | 9 +++----- src/init.rs | 65 ++++++++++++++++++++++++++++++++++++++++++++++++++-- 3 files changed, 67 insertions(+), 9 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 04e6366..2970d26 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -20,7 +20,7 @@ default = ["small_allocator", "static"] libc = { version = "0.2", default-features = false } memoffset = "0.7" static_assertions = "1.1.0" -parking_lot = "0.12" +lock_api = "0.4.10" [dev-dependencies] rand = "0.8" diff --git a/src/alloc.rs b/src/alloc.rs index ed3f16d..3f9802d 100644 --- a/src/alloc.rs +++ b/src/alloc.rs @@ -1,4 +1,3 @@ -use crate::lean_get_slot_idx; use crate::lean_inc_heartbeat; use crate::LEAN_OBJECT_SIZE_DELTA; use core::alloc::GlobalAlloc; @@ -27,7 +26,7 @@ unsafe impl GlobalAlloc for LeanAlloc { #[cfg(feature = "small_allocator")] if alignment == LEAN_OBJECT_SIZE_DELTA && size <= crate::LEAN_MAX_SMALL_OBJECT_SIZE as usize { - let slot_idx = lean_get_slot_idx(size as _); + let slot_idx = crate::lean_get_slot_idx(size as _); return crate::lean_alloc_small(size as _, slot_idx).cast(); } @@ -55,14 +54,12 @@ unsafe impl GlobalAlloc for LeanAlloc { #[cfg(test)] mod test { - use crate::lean_initialize_locked; + use crate::test::initialize_runtime_module_for_tests; extern crate std; #[test] fn various_sized_allocations() { - unsafe { - lean_initialize_locked(); - } + initialize_runtime_module_for_tests(); use core::alloc::GlobalAlloc; let alloc = super::LeanAlloc; for size in [ diff --git a/src/init.rs b/src/init.rs index 6f23f27..0a6c6a5 100644 --- a/src/init.rs +++ b/src/init.rs @@ -1,7 +1,35 @@ /*! Utilities for initializing Lean's runtime */ -use parking_lot::Mutex; + +pub struct LibcMutex { + mutex: libc::pthread_mutex_t, +} + +unsafe impl lock_api::RawMutex for LibcMutex { + const INIT: Self = Self { + mutex: libc::PTHREAD_MUTEX_INITIALIZER, + }; + + type GuardMarker = lock_api::GuardNoSend; + + fn lock(&self) { + unsafe { + libc::pthread_mutex_lock(&self.mutex as *const _ as *mut _); + } + } + + fn try_lock(&self) -> bool { + unsafe { libc::pthread_mutex_trylock(&self.mutex as *const _ as *mut _) == 0 } + } + + unsafe fn unlock(&self) { + libc::pthread_mutex_unlock(&self.mutex as *const _ as *mut _); + } +} + +pub type Mutex = lock_api::Mutex; +pub type MutexGuard<'a, T> = lock_api::MutexGuard<'a, LibcMutex, T>; /// A convenience mutex, since [`lean_initialize_runtime_module`] and [`lean_initialize`] are *not* thread-safe. /// @@ -19,7 +47,7 @@ use parking_lot::Mutex; /// let big_nat = unsafe { lean_uint64_to_nat(u64::MAX) }; /// assert!(!lean_is_scalar(big_nat)); /// ``` -pub static LEAN_INIT_MUTEX: Mutex<()> = Mutex::new(()); +pub static LEAN_INIT_MUTEX: Mutex = Mutex::new(false); /// A helper function to call [`lean_initialize_runtime_module`] while holding the [`LEAN_INIT_MUTEX`]. /// @@ -56,3 +84,36 @@ extern "C" { pub fn lean_initialize_runtime_module(); pub fn lean_initialize(); } + +#[cfg(test)] +pub(crate) mod test { + use crate::{lean_initialize_runtime_module, LEAN_INIT_MUTEX}; + extern crate std; + + #[test] + fn basic_mutex() { + let mutex = std::sync::Mutex::new(0); + std::thread::scope(|s| { + for i in 0..20 { + let mutex = &mutex; + s.spawn(move || { + let mut guard = mutex.lock().unwrap(); + *guard += i; + }); + } + }); + std::assert_eq!(mutex.into_inner().unwrap(), 190); + } + + static INITIALIZED: std::sync::atomic::AtomicBool = std::sync::atomic::AtomicBool::new(false); + + 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); + } + } +} From 7837b60772e78c4c2706e0fcf552fdfef4981e64 Mon Sep 17 00:00:00 2001 From: Schrodinger ZHU Yifan Date: Mon, 21 Aug 2023 21:52:32 -0400 Subject: [PATCH 2/2] remove locked routines --- Cargo.toml | 1 - src/init.rs | 103 +++------------------------------------------------- src/nat.rs | 2 +- 3 files changed, 6 insertions(+), 100 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 2970d26..7c3dedf 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -20,7 +20,6 @@ default = ["small_allocator", "static"] libc = { version = "0.2", default-features = false } memoffset = "0.7" static_assertions = "1.1.0" -lock_api = "0.4.10" [dev-dependencies] rand = "0.8" diff --git a/src/init.rs b/src/init.rs index 0a6c6a5..e482172 100644 --- a/src/init.rs +++ b/src/init.rs @@ -2,84 +2,6 @@ Utilities for initializing Lean's runtime */ -pub struct LibcMutex { - mutex: libc::pthread_mutex_t, -} - -unsafe impl lock_api::RawMutex for LibcMutex { - const INIT: Self = Self { - mutex: libc::PTHREAD_MUTEX_INITIALIZER, - }; - - type GuardMarker = lock_api::GuardNoSend; - - fn lock(&self) { - unsafe { - libc::pthread_mutex_lock(&self.mutex as *const _ as *mut _); - } - } - - fn try_lock(&self) -> bool { - unsafe { libc::pthread_mutex_trylock(&self.mutex as *const _ as *mut _) == 0 } - } - - unsafe fn unlock(&self) { - libc::pthread_mutex_unlock(&self.mutex as *const _ as *mut _); - } -} - -pub type Mutex = lock_api::Mutex; -pub type MutexGuard<'a, T> = lock_api::MutexGuard<'a, LibcMutex, T>; - -/// A convenience mutex, since [`lean_initialize_runtime_module`] and [`lean_initialize`] are *not* thread-safe. -/// -/// It is convention to hold this when initializing Lean's runtime, or Lean modules, to make sure only one thread at a time is doing so. -/// This is used in this library to safely implement tests, but it is the user's responsibility to uphold thread-safety when using this API. -/// -/// # Examples -/// ```rust -/// # use lean_sys::*; -/// unsafe { -/// let guard = LEAN_INIT_MUTEX.lock(); -/// lean_initialize_runtime_module(); -/// // LEAN_INIT_MUTEX is unlocked here when `guard` goes out of scope -/// } -/// let big_nat = unsafe { lean_uint64_to_nat(u64::MAX) }; -/// assert!(!lean_is_scalar(big_nat)); -/// ``` -pub static LEAN_INIT_MUTEX: Mutex = Mutex::new(false); - -/// A helper function to call [`lean_initialize_runtime_module`] while holding the [`LEAN_INIT_MUTEX`]. -/// -/// This is equivalent to writing -/// ```rust -/// # use lean_sys::*; -/// unsafe { -/// let guard = LEAN_INIT_MUTEX.lock(); -/// lean_initialize_runtime_module(); -/// } -/// ``` -//TODO: is this safe? -pub unsafe fn lean_initialize_runtime_module_locked() { - let _guard = LEAN_INIT_MUTEX.lock(); - lean_initialize_runtime_module(); -} - -/// A helper function to call [`lean_initialize`] while holding the [`LEAN_INIT_MUTEX`]./// -/// This is equivalent to writing -/// ```rust -/// # use lean_sys::*; -/// unsafe { -/// let guard = LEAN_INIT_MUTEX.lock(); -/// lean_initialize(); -/// } -/// ``` -//TODO: is this safe? -pub unsafe fn lean_initialize_locked() { - let _guard = LEAN_INIT_MUTEX.lock(); - lean_initialize(); -} - extern "C" { pub fn lean_initialize_runtime_module(); pub fn lean_initialize(); @@ -87,33 +9,18 @@ extern "C" { #[cfg(test)] pub(crate) mod test { - use crate::{lean_initialize_runtime_module, LEAN_INIT_MUTEX}; + use crate::lean_initialize_runtime_module; extern crate std; - #[test] - fn basic_mutex() { - let mutex = std::sync::Mutex::new(0); - std::thread::scope(|s| { - for i in 0..20 { - let mutex = &mutex; - s.spawn(move || { - let mut guard = mutex.lock().unwrap(); - *guard += i; - }); - } - }); - std::assert_eq!(mutex.into_inner().unwrap(), 190); - } - - static INITIALIZED: std::sync::atomic::AtomicBool = std::sync::atomic::AtomicBool::new(false); + static INITIALIZED: std::sync::Mutex = std::sync::Mutex::new(false); pub(crate) fn initialize_runtime_module_for_tests() { - let _guard = LEAN_INIT_MUTEX.lock(); - if !INITIALIZED.load(std::sync::atomic::Ordering::SeqCst) { + let mut guard = INITIALIZED.lock().unwrap(); + if !*guard { unsafe { lean_initialize_runtime_module(); } - INITIALIZED.store(true, std::sync::atomic::Ordering::SeqCst); + *guard = true; } } } diff --git a/src/nat.rs b/src/nat.rs index 0de3cd1..dadeb02 100644 --- a/src/nat.rs +++ b/src/nat.rs @@ -213,8 +213,8 @@ mod test { #[test] fn big_nat_multiplication_commutes_test() { let mut rng = rand_xoshiro::Xoshiro256PlusPlus::seed_from_u64(0x568478687); + crate::test::initialize_runtime_module_for_tests(); unsafe { - lean_initialize_runtime_module_locked(); let mut vec = std::vec::Vec::with_capacity(100); for _ in 0..10 { for _ in 0..100 {