ostd/sync/rcu/non_null/
either.rs

1// SPDX-License-Identifier: MPL-2.0
2use vstd::{
3    bits,
4    prelude::*,
5    raw_ptr::group_raw_ptr_axioms,
6    std_specs::{nonzero::*, ops::BitOrSpec},
7};
8use vstd_extra::{prelude::*, sum::Sum};
9
10use super::{NonNullPtr, NonNullPtrRef};
11use crate::util::Either;
12use core::num::NonZeroUsize;
13use core::{marker::PhantomData, ptr::NonNull};
14
15verus! {
16
17broadcast use {group_nonull_axioms, group_nonzero_axioms, group_raw_ptr_axioms};
18// If both `L` and `R` have at least one alignment bit (i.e., their alignments are at least 2), we
19// can use the alignment bit to indicate whether a pointer is `L` or `R`, so it's possible to
20// implement `NonNullPtr` for `Either<L, R>`.
21
22unsafe impl<L: NonNullPtr, R: NonNullPtr> NonNullPtr for Either<L, R> {
23    type Target = PhantomData<Self>;
24
25    // type Ref<'a>
26    //     = Either<L::Ref<'a>, R::Ref<'a>>
27    // where
28    //     Self: 'a;
29    type Permission = Sum<L::Permission, R::Permission>;
30
31    #[verifier::external_body]
32    const ALIGN_BITS: u32 = min(L::ALIGN_BITS, R::ALIGN_BITS).checked_sub(1).expect(
33        "`L` and `R` alignments should be at least 2 to pack `Either` into one pointer",
34    );
35
36    #[verifier::spinoff_prover]
37    fn into_raw(self) -> (ret: (NonNull<Self::Target>, Tracked<Self::Permission>)) {
38        proof_decl!{
39           let ghost align_bits = Self::ALIGN_BITS;
40           let ghost l_align_bits = L::ALIGN_BITS;
41           let ghost r_align_bits = R::ALIGN_BITS;
42           let ghost tag = 1usize << align_bits;
43        }
44        proof! {
45            L::lemma_align_bits_range();
46            R::lemma_align_bits_range();
47            Self::lemma_align_bits_range();
48            vstd::bits::lemma_usize_pow2_no_overflow(align_bits as nat);
49            vstd::bits::lemma_usize_pow2_no_overflow(l_align_bits as nat);
50            vstd::bits::lemma_usize_pow2_no_overflow(r_align_bits as nat);
51            vstd::bits::lemma_usize_shl_is_mul(1, align_bits as usize);
52            vstd::bits::lemma_usize_shl_is_mul(1, l_align_bits as usize);
53            vstd::bits::lemma_usize_shl_is_mul(1, r_align_bits as usize);
54        }
55        match self {
56            Self::Left(left) => {
57                // left.into_raw().cast(),
58                let (left, Tracked(perm)) = left.into_raw();
59                proof! {
60                    let left_addr = left.cast::<Self::Target>().view_ptr_mut().addr();
61                    let extra_bits: u32 = (l_align_bits - align_bits) as u32;
62                    let scale = 1usize << extra_bits;
63                    vstd::bits::lemma_usize_pow2_no_overflow(extra_bits as nat);
64                    vstd::bits::lemma_usize_shl_is_mul(1, extra_bits as usize);
65                    vstd::arithmetic::power2::lemma_pow2_adds(align_bits as nat, extra_bits as nat);
66                    assert(left_addr % tag == 0) by {
67                        let big = 1usize << l_align_bits;
68                        let q = left_addr / big;
69                        vstd::arithmetic::div_mod::lemma_fundamental_div_mod(left_addr as int, big as int);
70                        assert(left_addr == q * scale * tag) by (nonlinear_arith)
71                        requires
72                            left_addr == q * big,
73                            big == tag * scale,
74                        ;
75                        vstd::arithmetic::div_mod::lemma_mod_multiples_basic(q * scale, tag as int);
76                    };
77                    lemma_aligned_addr_clears_tag_bit(left_addr, tag, align_bits, l_align_bits);
78                }
79                (left.cast(), Tracked(Sum::Left(perm)))
80            },
81            Self::Right(right) => {
82                /* right
83                .into_raw()
84                .map_addr(|addr| addr | (1 << Self::ALIGN_BITS))
85                .cast(), */
86                let (right, Tracked(perm)) = right.into_raw();
87                let right_tagged = right.map_addr_v(
88                    |addr: NonZeroUsize| -> (ret: NonZeroUsize)
89                        ensures
90                            ret@ == addr@ | (1usize << Self::ALIGN_BITS),
91                        {
92                            proof {
93                                let tag = 1usize << Self::ALIGN_BITS;
94                                let a = addr@;
95                                assert(a | tag != 0) by (bit_vector)
96                                    requires
97                                        a != 0,
98                                ;
99                            }
100                            addr | 1usize << Self::ALIGN_BITS
101                        },
102                );
103                proof! {
104                    let addr = right.addr_spec()@;
105                    let tagged_addr = right_tagged.addr_spec()@;
106                    assert(tagged_addr & tag == tag) by (bit_vector)
107                    requires
108                        tagged_addr == addr | tag,
109                        tag == 1usize << align_bits,
110                        1 <= r_align_bits < usize::BITS,
111                        align_bits < r_align_bits,
112                        addr % (1usize << r_align_bits) == 0,
113                        addr != 0,
114                    ;
115                    let extra_bits: u32 = (r_align_bits - align_bits) as u32;
116                    let scale = 1usize << extra_bits;
117                    vstd::bits::lemma_usize_pow2_no_overflow(extra_bits as nat);
118                    vstd::bits::lemma_usize_shl_is_mul(1, extra_bits as usize);
119                    vstd::arithmetic::power2::lemma_pow2_adds(align_bits as nat, extra_bits as nat);
120                    assert(tagged_addr == addr + tag) by (bit_vector)
121                    requires
122                        tagged_addr == addr | tag,
123                        tag == 1usize << align_bits,
124                        1 <= r_align_bits < usize::BITS,
125                        align_bits < r_align_bits,
126                        addr % (1usize << r_align_bits) == 0,
127                        addr != 0,
128                    ;
129                    assert(addr % tag == 0) by {
130                        let big = 1usize << r_align_bits;
131                        let q = addr / big;
132                        vstd::arithmetic::div_mod::lemma_fundamental_div_mod(addr as int, big as int);
133                        assert(addr == q * scale * tag) by (nonlinear_arith)
134                        requires
135                            addr == q * big,
136                            big == tag * scale,
137                        ;
138                        vstd::arithmetic::div_mod::lemma_mod_multiples_basic(q * scale, tag as int);
139                    }
140                    lemma_aligned_addr_clears_tag_bit(addr, tag, align_bits, r_align_bits);
141                    assert(tagged_addr & !tag == addr) by (bit_vector)
142                    requires
143                        tagged_addr == addr | tag,
144                        addr & tag == 0,
145                    ;
146                    assert(tagged_addr % (1usize << align_bits) == 0) by {
147                        vstd::arithmetic::div_mod::lemma_mod_add_multiples_vanish(addr as int, tag as int);
148                    }
149                }
150                (right_tagged.cast(), Tracked(Sum::Right(perm)))
151            },
152        }
153    }
154
155    unsafe fn from_raw(
156        ptr: NonNull<Self::Target>,
157        Tracked(perm): Tracked<Self::Permission>,
158    ) -> Self {
159        proof! {
160            Self::lemma_align_bits_range();
161        }
162        proof_decl! {
163            let ghost align_bits = Self::ALIGN_BITS;
164            let ghost tag = 1usize << Self::ALIGN_BITS;
165            let ghost ptr_addr = ptr.view_ptr_mut()@.addr;
166        }
167        proof! {
168            assert(tag > 0) by (bit_vector)
169            requires
170                tag == 1usize << align_bits,
171                align_bits < usize::BITS,
172            ;
173            match perm {
174                Sum::Left(_) => {
175                    assert((ptr_addr & !tag) == ptr_addr) by (bit_vector)
176                    requires
177                        ptr_addr & tag == 0,
178                    ;
179                },
180                Sum::Right(_) => {
181                    assert((ptr_addr & tag) < ptr_addr) by (bit_vector)
182                    requires
183                        ptr_addr & tag == tag,
184                        (ptr_addr & !tag) != 0,
185                    ;
186                },
187            }
188        }
189        // SAFETY: The caller ensures that the pointer comes from `Self::into_raw`, which
190        // guarantees that `real_ptr` is a non-null pointer.
191        let (is_right, real_ptr) = unsafe { remove_bits(ptr, 1 << Self::ALIGN_BITS) };
192
193        if is_right == 0 {
194            // SAFETY: `Self::into_raw` guarantees that `real_ptr` comes from `L::into_raw`. Other
195            // safety requirements are upheld by the caller.
196            Either::Left(unsafe { L::from_raw(real_ptr.cast(), Tracked(perm.tracked_take_left())) })
197        } else {
198            // SAFETY: `Self::into_raw` guarantees that `real_ptr` comes from `R::into_raw`. Other
199            // safety requirements are upheld by the caller.
200            Either::Right(
201                unsafe { R::from_raw(real_ptr.cast(), Tracked(perm.tracked_take_right())) },
202            )
203        }
204    }
205
206    open spec fn ptr_perm_match(ptr: *mut Self::Target, perm: Self::Permission) -> bool {
207        let tag = 1usize << Self::ALIGN_BITS;
208        match perm {
209            Sum::Left(left) => {
210                &&& ptr.addr() & tag == 0
211                &&& L::ptr_perm_match(ptr.cast(), left)
212            },
213            Sum::Right(right) => {
214                let untagged_ptr = ptr.with_addr((ptr.addr() & !tag));
215                let right_nonnull = nonnull_from_ptr_mut_spec(untagged_ptr);
216                &&& ptr.addr() & tag == tag
217                &&& (ptr.addr() & !tag) != 0
218                &&& R::ptr_perm_match(right_nonnull.cast().view_ptr_mut(), right)
219            },
220        }
221    }
222
223    open spec fn rel_perm(self, perm: Self::Permission) -> bool {
224        match (self, perm) {
225            (Either::Left(left), Sum::Left(left_perm)) => left.rel_perm(left_perm),
226            (Either::Right(right), Sum::Right(right_perm)) => right.rel_perm(right_perm),
227            _ => false,
228        }
229    }
230
231    axiom fn lemma_align_bits_range()
232        ensures
233            Self::ALIGN_BITS == if L::ALIGN_BITS < R::ALIGN_BITS {
234                L::ALIGN_BITS - 1
235            } else {
236                R::ALIGN_BITS - 1
237            },
238    ;
239}
240
241unsafe impl<'a, L: NonNullPtrRef<'a>, R: NonNullPtrRef<'a>> NonNullPtrRef<'a> for Either<L, R> {
242    type Ref = Either<L::Ref, R::Ref>;
243
244    type RefPermission = Sum<L::RefPermission, R::RefPermission>;
245
246    open spec fn ref_perm_view_permission(perm: Self::RefPermission) -> Self::Permission {
247        match perm {
248            Sum::Left(left) => Sum::Left(L::ref_perm_view_permission(left)),
249            Sum::Right(right) => Sum::Right(R::ref_perm_view_permission(right)),
250        }
251    }
252
253    open spec fn ref_rel_perm(r: Self::Ref, perm: Self::RefPermission) -> bool {
254        true
255    }
256
257    proof fn lemma_ref_perm_inv_impl_perm_inv(perm: Self::RefPermission) {
258        match perm {
259            Sum::Left(left) => L::lemma_ref_perm_inv_impl_perm_inv(left),
260            Sum::Right(right) => R::lemma_ref_perm_inv_impl_perm_inv(right),
261        }
262    }
263
264    proof fn borrow_ref_perm(tracked perm: &Self::RefPermission) -> (tracked ret:
265        Self::RefPermission) {
266        if perm is Left {
267            Sum::Left(L::borrow_ref_perm(perm.tracked_borrow_left()))
268        } else {
269            Sum::Right(R::borrow_ref_perm(perm.tracked_borrow_right()))
270        }
271    }
272
273    proof fn borrow_perm_as_ref_perm(tracked perm: &'a Self::Permission) -> (tracked ret:
274        Self::RefPermission) {
275        if perm is Left {
276            Sum::Left(L::borrow_perm_as_ref_perm(perm.tracked_borrow_left()))
277        } else {
278            Sum::Right(R::borrow_perm_as_ref_perm(perm.tracked_borrow_right()))
279        }
280    }
281
282    unsafe fn raw_as_ref(
283        raw: NonNull<Self::Target>,
284        Tracked(perm): Tracked<Self::RefPermission>,
285    ) -> Self::Ref {
286        proof_decl! {
287            let ghost align_bits = Self::ALIGN_BITS;
288            let ghost tag = 1usize << align_bits;
289            let ghost raw_addr = raw.view_ptr_mut()@.addr;
290        }
291        proof! {
292            Self::lemma_align_bits_range();
293            if perm is Left {
294                assert((raw_addr & !tag) == raw_addr) by (bit_vector)
295                    requires
296                        raw_addr & tag == 0,
297                    ;
298            } else {
299                assert((raw_addr & tag) < raw_addr) by (bit_vector)
300                requires
301                    raw_addr & tag == tag,
302                    (raw_addr & !tag) != 0,
303                ;
304            }
305        }
306        // SAFETY: The caller ensures that the pointer comes from `Self::into_raw`, which
307        // guarantees that `real_ptr` is a non-null pointer.
308        let (is_right, real_ptr) = unsafe { remove_bits(raw, 1 << Self::ALIGN_BITS) };
309
310        if is_right == 0 {
311            proof!{
312                if perm is Right {
313                    assert(tag != 0) by (bit_vector)
314                    requires
315                        tag == 1usize << align_bits,
316                        align_bits < usize::BITS,
317                    ;
318                    assert(false);
319                }
320            }
321            // SAFETY: `Self::into_raw` guarantees that `real_ptr` comes from `L::into_raw`. Other
322            // safety requirements are upheld by the caller.
323            Either::Left(
324                unsafe { L::raw_as_ref(real_ptr.cast(), Tracked(perm.tracked_take_left())) },
325            )
326        } else {
327            // SAFETY: `Self::into_raw` guarantees that `real_ptr` comes from `R::into_raw`. Other
328            // safety requirements are upheld by the caller.
329            Either::Right(
330                unsafe { R::raw_as_ref(real_ptr.cast(), Tracked(perm.tracked_take_right())) },
331            )
332        }
333    }
334
335    #[verifier::spinoff_prover]
336    fn ref_as_raw(ptr_ref: Self::Ref) -> (NonNull<Self::Target>, Tracked<Self::RefPermission>) {
337        proof!{
338            Self::lemma_align_bits_range();
339        }
340        proof_decl!{
341            let ghost align_bits = Self::ALIGN_BITS;
342            let ghost tag = 1usize << align_bits;
343            let ghost l_align_bits = L::ALIGN_BITS;
344            let ghost r_align_bits = R::ALIGN_BITS;
345        }
346        proof!{
347            L::lemma_align_bits_range();
348            R::lemma_align_bits_range();
349            vstd::bits::lemma_usize_pow2_no_overflow(align_bits as nat);
350            vstd::bits::lemma_usize_pow2_no_overflow(l_align_bits as nat);
351            vstd::bits::lemma_usize_pow2_no_overflow(r_align_bits as nat);
352            vstd::bits::lemma_usize_shl_is_mul(1, align_bits as usize);
353            vstd::bits::lemma_usize_shl_is_mul(1, l_align_bits as usize);
354            vstd::bits::lemma_usize_shl_is_mul(1, r_align_bits as usize);
355        }
356        match ptr_ref {
357            Either::Left(left) => {
358                // L::ref_as_raw(left).cast()
359                let (ptr, Tracked(perm)) = L::ref_as_raw(left);
360                proof! {
361                    let ghost ptr_addr = ptr.view_ptr_mut().addr();
362                    L::lemma_ref_perm_inv_impl_perm_inv(perm);
363                    let extra_bits: u32 = (l_align_bits - align_bits) as u32;
364                    let scale = 1usize << extra_bits;
365                    vstd::bits::lemma_usize_pow2_no_overflow(extra_bits as nat);
366                    vstd::bits::lemma_usize_shl_is_mul(1, extra_bits as usize);
367                    vstd::arithmetic::power2::lemma_pow2_adds(align_bits as nat, extra_bits as nat);
368                    assert(ptr_addr % tag == 0) by {
369                        let big = 1usize << l_align_bits;
370                        let q = ptr_addr / big;
371                        vstd::arithmetic::div_mod::lemma_fundamental_div_mod(ptr_addr as int, big as int);
372                        assert(ptr_addr == (q * scale) * tag) by (nonlinear_arith)
373                        requires
374                            ptr_addr == q * big,
375                            big == tag * scale,
376                        ;
377                        vstd::arithmetic::div_mod::lemma_mod_multiples_basic(q * scale, tag as int);
378                    };
379                    assert(ptr_addr & tag == 0) by (bit_vector)
380                    requires
381                        ptr_addr % (1usize << l_align_bits) == 0,
382                        tag == 1usize << align_bits,
383                        align_bits < l_align_bits < usize::BITS,
384                    ;
385                }
386                (ptr.cast(), Tracked(Sum::Left(perm)))
387            },
388            Either::Right(right) => {
389                /* R::ref_as_raw(right)
390                .map_addr(|addr| addr | (1 << Self::ALIGN_BITS))
391                .cast() */
392                let (ptr, Tracked(perm)) = R::ref_as_raw(right);
393                proof! {
394                    Self::lemma_align_bits_range();
395                }
396                let tagged_ptr = ptr.map_addr_v(
397                    |addr: NonZeroUsize| -> (ret: NonZeroUsize)
398                        ensures
399                            ret@ == addr@ | (1usize << Self::ALIGN_BITS),
400                        {
401                            proof {
402                                let tag = 1usize << Self::ALIGN_BITS;
403                                let a = addr@;
404                                assert(a | tag != 0) by (bit_vector)
405                                    requires
406                                        a != 0,
407                                ;
408                            }
409                            addr | 1usize << Self::ALIGN_BITS
410                        },
411                );
412                proof! {
413                    let ghost ptr_addr = ptr.view_ptr_mut().addr();
414                    let ghost tagged_addr = tagged_ptr.view_ptr_mut().addr();
415                    R::lemma_ref_perm_inv_impl_perm_inv(perm);
416                    assert(tagged_addr & tag == tag) by (bit_vector)
417                    requires
418                        tagged_addr == ptr_addr | tag,
419                        tag == 1usize << align_bits,
420                        align_bits < r_align_bits < usize::BITS,
421                        ptr_addr % (1usize << r_align_bits) == 0,
422                        ptr_addr != 0,
423                    ;
424                    assert(ptr_addr & tag == 0) by (bit_vector)
425                    requires
426                        ptr_addr % (1usize << r_align_bits) == 0,
427                        tag == 1usize << align_bits,
428                        align_bits < r_align_bits < usize::BITS,
429                    ;
430                    assert(tagged_addr & !tag == ptr_addr) by (bit_vector)
431                    requires
432                        tagged_addr == ptr_addr | tag,
433                        ptr_addr & tag == 0,
434                    ;
435                    let extra_bits: u32 = (r_align_bits - align_bits) as u32;
436                    let scale = 1usize << extra_bits;
437                    vstd::bits::lemma_usize_pow2_no_overflow(extra_bits as nat);
438                    vstd::bits::lemma_usize_shl_is_mul(1, extra_bits as usize);
439                    vstd::arithmetic::power2::lemma_pow2_adds(align_bits as nat, extra_bits as nat);
440                    assert(tagged_addr == ptr_addr + tag) by (bit_vector)
441                    requires
442                        tagged_addr == ptr_addr | tag,
443                        ptr_addr & tag == 0,
444                    ;
445                    assert(ptr_addr % tag == 0) by {
446                        let big = 1usize << r_align_bits;
447                        let q = ptr_addr / big;
448                        vstd::arithmetic::div_mod::lemma_fundamental_div_mod(ptr_addr as int, big as int);
449                        assert(ptr_addr == (q * scale) * tag) by (nonlinear_arith)
450                        requires
451                            ptr_addr == q * big,
452                            big == tag * scale,
453                        ;
454                        vstd::arithmetic::div_mod::lemma_mod_multiples_basic(q * scale, tag as int);
455                    };
456                    assert(tagged_addr % tag == 0) by {
457                        vstd::arithmetic::div_mod::lemma_mod_add_multiples_vanish(ptr_addr as int, tag as int);
458                    }
459                }
460                (tagged_ptr.cast(), Tracked(Sum::Right(perm)))
461            },
462        }
463    }
464}
465
466} // verus!
467// A `min` implementation for use in constant evaluation.
468#[verus_verify(dual_spec)]
469const fn min(a: u32, b: u32) -> u32 {
470    if a < b { a } else { b }
471}
472
473verus! {
474
475/// # Safety
476///
477/// The caller must ensure that removing the bits from the non-null pointer will result in another
478/// non-null pointer.
479// FIXEME: fix when verus attribute syntax supports closure postconditions.
480#[verus_spec(ret =>
481    requires
482        (ptr.view_ptr_mut().addr() & bits) < ptr.view_ptr_mut().addr(),
483        (ptr.view_ptr_mut().addr() & !bits) != 0,
484    ensures
485        ret.0 == (ptr.view_ptr_mut().addr() & bits),
486        ret.1.view_ptr_mut() == ptr.view_ptr_mut().with_addr((ptr.view_ptr_mut().addr() & !bits) as usize),
487)]
488unsafe fn remove_bits<T>(ptr: NonNull<T>, bits: usize) -> (usize, NonNull<T>) {
489    use core::num::NonZeroUsize;
490
491    let removed_bits = ptr.addr_v().get() & bits;
492    let result_ptr = ptr.map_addr_v(
493        |addr| -> (ret: NonZeroUsize)
494            requires
495                addr@ & !bits != 0,
496            ensures
497                ret@ == addr@ & !bits,
498            {
499                // SAFETY: The safety is upheld by the caller.
500                unsafe { NonZeroUsize::new_unchecked(addr.get() & !bits) }
501            },
502    );
503    (removed_bits, result_ptr)
504}
505
506#[verifier::spinoff_prover]
507proof fn lemma_aligned_addr_clears_tag_bit(
508    addr: usize,
509    tag: usize,
510    align_bits: u32,
511    ptr_align_bits: u32,
512)
513    requires
514        addr % (1usize << ptr_align_bits) == 0,
515        tag == 1usize << align_bits,
516        align_bits < ptr_align_bits < usize::BITS,
517    ensures
518        addr & tag == 0,
519{
520    assert(addr & (1usize << align_bits) == 0) by (bit_vector)
521        requires
522            addr % (1usize << ptr_align_bits) == 0,
523            0u32 < ptr_align_bits,
524            align_bits < ptr_align_bits,
525            ptr_align_bits <= 63u32,
526    ;
527    assert(addr & tag == 0) by (bit_vector)
528        requires
529            addr & (1usize << align_bits) == 0,
530            tag == 1usize << align_bits,
531            align_bits < 64u32,
532    ;
533}
534
535} // verus!
536#[cfg(ktest)]
537mod test {
538    use alloc::{boxed::Box, sync::Arc};
539
540    use super::*;
541    use crate::{prelude::ktest, sync::RcuOption};
542
543    type Either32 = Either<Arc<u32>, Box<u32>>;
544    type Either16 = Either<Arc<u32>, Box<u16>>;
545
546    #[ktest]
547    fn alignment() {
548        assert_eq!(<Either32 as NonNullPtr>::ALIGN_BITS, 1);
549        assert_eq!(<Either16 as NonNullPtr>::ALIGN_BITS, 0);
550    }
551
552    #[ktest]
553    fn left_pointer() {
554        let val: Either16 = Either::Left(Arc::new(123));
555
556        let ptr = NonNullPtr::into_raw(val);
557        assert_eq!(ptr.addr().get() & 1, 0);
558
559        let ref_ = unsafe { <Either16 as NonNullPtr>::raw_as_ref(ptr) };
560        assert!(matches!(ref_, Either::Left(ref r) if ***r == 123));
561
562        let ptr2 = <Either16 as NonNullPtr>::ref_as_raw(ref_);
563        assert_eq!(ptr, ptr2);
564
565        let val = unsafe { <Either16 as NonNullPtr>::from_raw(ptr) };
566        assert!(matches!(val, Either::Left(ref r) if **r == 123));
567        drop(val);
568    }
569
570    #[ktest]
571    fn right_pointer() {
572        let val: Either16 = Either::Right(Box::new(456));
573
574        let ptr = NonNullPtr::into_raw(val);
575        assert_eq!(ptr.addr().get() & 1, 1);
576
577        let ref_ = unsafe { <Either16 as NonNullPtr>::raw_as_ref(ptr) };
578        assert!(matches!(ref_, Either::Right(ref r) if ***r == 456));
579
580        let ptr2 = <Either16 as NonNullPtr>::ref_as_raw(ref_);
581        assert_eq!(ptr, ptr2);
582
583        let val = unsafe { <Either16 as NonNullPtr>::from_raw(ptr) };
584        assert!(matches!(val, Either::Right(ref r) if **r == 456));
585        drop(val);
586    }
587
588    #[ktest]
589    fn rcu_store_load() {
590        let rcu: RcuOption<Either32> = RcuOption::new_none();
591        assert!(rcu.read().get().is_none());
592
593        rcu.update(Some(Either::Left(Arc::new(888))));
594        assert!(matches!(rcu.read().get().unwrap(), Either::Left(r) if **r == 888));
595
596        rcu.update(Some(Either::Right(Box::new(999))));
597        assert!(matches!(rcu.read().get().unwrap(), Either::Right(r) if **r == 999));
598    }
599}
ostd/sync/rcu/non_null/either.rs

ostd/sync/rcu/non_null/
either.rs
