| 294 | /// Tests LeanShared + lean_mark_mt on complex Ix object graphs. |
| 295 | #[unsafe(no_mangle)] |
| 296 | pub extern "C" fn rs_mt_parallel_decode_names( |
| 297 | arr: LeanArray<LeanBorrowed<'_>>, |
| 298 | n_threads: usize, |
| 299 | ) -> LeanOwned { |
| 300 | let shared = LeanShared::new(arr.inner().to_owned_ref()); |
| 301 | |
| 302 | let handles: Vec<_> = (0..n_threads) |
| 303 | .map(|_| { |
| 304 | let shared_clone = shared.clone(); |
| 305 | thread::spawn(move || { |
| 306 | let borrowed_arr = shared_clone.borrow().as_array(); |
| 307 | let mut count: u64 = 0; |
| 308 | for elem in borrowed_arr.iter() { |
| 309 | let _name = LeanIxName(elem).decode(); |
| 310 | count += 1; |
| 311 | } |
| 312 | count |
| 313 | }) |
| 314 | }) |
| 315 | .collect(); |
| 316 | |
| 317 | let total: u64 = handles.into_iter().map(|h| h.join().unwrap()).sum(); |
| 318 | LeanNat::from_nat(&Nat::from(total)).into() |
| 319 | } |
| 320 | |
| 321 | /// Mark an array of Ix.Exprs as MT, decode in parallel from N threads. |
| 322 | /// Each thread decodes all exprs and counts nodes. |