diff --git a/releases/rust/db_esdk/dafny_runtime_rust/Cargo.toml b/releases/rust/db_esdk/dafny_runtime_rust/Cargo.toml index 7680fd5d6..1259d4bc1 100644 --- a/releases/rust/db_esdk/dafny_runtime_rust/Cargo.toml +++ b/releases/rust/db_esdk/dafny_runtime_rust/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "dafny-runtime" -version = "0.3.0" +version = "0.3.1" edition = "2021" keywords = ["dafny"] license = "ISC AND (Apache-2.0 OR ISC)" diff --git a/releases/rust/db_esdk/dafny_runtime_rust/src/lib.rs b/releases/rust/db_esdk/dafny_runtime_rust/src/lib.rs index f422c8de1..fd8a07db7 100644 --- a/releases/rust/db_esdk/dafny_runtime_rust/src/lib.rs +++ b/releases/rust/db_esdk/dafny_runtime_rust/src/lib.rs @@ -3304,10 +3304,11 @@ impl Object { // SAFETY: Not guaranteed unfortunately. But looking at the sources of from_raw as of today 10/24/2024 // it will will correctly rebuilt the Rc let rebuilt = ::std::hint::black_box(unsafe { Rc::from_raw(pt) }); - let previous_strong_count = ::std::hint::black_box(Rc::strong_count(&rebuilt)); + let _previous_strong_count = ::std::hint::black_box(Rc::strong_count(&rebuilt)); ::std::hint::black_box(increment_strong_count(pt)); - let new_strong_count = ::std::hint::black_box(Rc::strong_count(&rebuilt)); - assert_eq!(new_strong_count, previous_strong_count + 1); // Will panic if not + let _new_strong_count = ::std::hint::black_box(Rc::strong_count(&rebuilt)); + #[cfg(not(feature = "sync"))] + assert_eq!(_new_strong_count, _previous_strong_count + 1); // Will panic if not. Asserted only in sequential mode Object(Some(rebuilt)) } } diff --git a/releases/rust/db_esdk/dafny_runtime_rust/src/tests/mod.rs b/releases/rust/db_esdk/dafny_runtime_rust/src/tests/mod.rs index bf75fc6e2..6bcc6e5d1 100644 --- a/releases/rust/db_esdk/dafny_runtime_rust/src/tests/mod.rs +++ b/releases/rust/db_esdk/dafny_runtime_rust/src/tests/mod.rs @@ -4,6 +4,8 @@ #[cfg(test)] mod tests { use crate::*; + #[cfg(feature = "sync")] + use std::thread; #[test] fn test_int() { @@ -40,22 +42,22 @@ mod tests { let b_copy_3 = b.clone(); let a_copy_4 = a.clone(); let b_copy_4 = b.clone(); - let handle_ab = std::thread::spawn(move || { + let handle_ab = thread::spawn(move || { let a_plus_b = a_copy_1.concat(&b_copy_1); let a_plus_b_vec = a_plus_b.to_array(); a_plus_b_vec }); - let handle_ba = std::thread::spawn(move || { + let handle_ba = thread::spawn(move || { let b_plus_a = b_copy_2.concat(&a_copy_2); let b_plus_a_vec = b_plus_a.to_array(); b_plus_a_vec }); - let handle_ab_2 = std::thread::spawn(move || { + let handle_ab_2 = thread::spawn(move || { let a_plus_b = a_copy_3.concat(&b_copy_3); let a_plus_b_vec = a_plus_b.to_array(); a_plus_b_vec }); - let handle_ba_2 = std::thread::spawn(move || { + let handle_ba_2 = thread::spawn(move || { let b_plus_a = b_copy_4.concat(&a_copy_4); let b_plus_a_vec = b_plus_a.to_array(); b_plus_a_vec @@ -1293,9 +1295,30 @@ mod tests { let c3 = c; assert_eq!(c3, c2); } - /*impl GeneralTrait for Rc { - fn _clone(&self) -> Box { - Box::new(self.as_ref().clone()) + + #[cfg(feature = "sync")] + #[test] + fn test_object_share_async() { + let obj = ClassWrapper::constructor_object(53); + let objClone = obj.clone(); + + let handle: thread::JoinHandle = thread::spawn(move || { + // Thread code here + let mut result: *const ClassWrapper = objClone.as_ref(); + for _i in 0..10000 { + let obj2 = Object::from_ref(objClone.as_ref()); + result = obj2.as_ref() as *const ClassWrapper; + } + result as i32 + }); + let mut result: *const ClassWrapper = obj.as_ref(); + for _i in 0..10000 { + let obj2 = Object::from_ref(obj.as_ref()); + result = obj2.as_ref() as *const ClassWrapper; } - }*/ + + // Wait for thread to finish + assert_eq!(handle.join().unwrap(), result as i32); + assert_eq!(result as i32, obj.as_ref() as *const ClassWrapper as i32); + } }