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

ostd/sync/rcu/non_null/
either.rs
