ostd/sync/
rwmutex.rs

1// SPDX-License-Identifier: MPL-2.0
2#[cfg(feature = "irc11")]
3use vstd::thread_view::Objective;
4use vstd::{
5    atomic_ghost::*,
6    cell::{self, CellId, pcell::*},
7    prelude::*,
8    resource::Loc,
9    std_specs::fmt::{DebugSpec, DebugSpecImpl},
10};
11use vstd_extra::{
12    resource::ghost_resource::{count_auth::*, count_ghost::*, csum::*, excl::*},
13    sum::*,
14};
15
16use core::{
17    cell::UnsafeCell,
18    fmt,
19    ops::{Deref, DerefMut},
20    sync::atomic::{
21        // AtomicUsize,
22        Ordering::{AcqRel, Acquire, Relaxed, Release},
23    },
24};
25
26use super::WaitQueue;
27
28verus! {
29
30type NoPerm<T> = EmptyCount<PointsTo<T>>;
31
32type HalfPerm<T> = Count<PointsTo<T>>;
33
34type ReadPerm<T> = (HalfPerm<T>, OneLeftKnowledge<HalfPerm<T>, NoPerm<T>, 3>);
35
36tracked struct RwPerms<T> {
37    core_token: SumResource<HalfPerm<T>, NoPerm<T>, 3>,
38    read_retract_token: TokenResource<MAX_READER_MASK>,
39    upread_retract_token: Option<UniqueToken>,
40    upreader_guard_token: Option<OneLeftOwner<HalfPerm<T>, NoPerm<T>, 3>>,
41    read_guard_token: CountResource<ReadPerm<T>, MAX_READER>,
42}
43
44#[cfg(feature = "irc11")]
45unsafe impl<T> Objective for RwPerms<T> {
46
47}
48
49ghost struct RwId {
50    core_token_id: Loc,
51    frac_id: Loc,
52    read_retract_token_id: Loc,
53    upread_retract_token_id: Loc,
54    read_guard_token_id: Loc,
55}
56
57#[verifier::reject_recursive_types(T)]
58struct_with_invariants! {
59/// A mutex that provides data access to either one writer or many readers.
60///
61/// # Overview
62///
63/// This mutex allows for multiple readers, or at most one writer to access
64/// at any point in time. The writer of this mutex has exclusive access to
65/// modify the underlying data, while the readers are allowed shared and
66/// read-only access.
67///
68/// The writing and reading portions cannot be active simultaneously, when
69/// one portion is in progress, the other portion will sleep. This is
70/// suitable for scenarios where the mutex is expected to be held for a
71/// period of time, which can avoid wasting CPU resources.
72///
73/// This implementation provides the upgradeable read mutex (`upread mutex`).
74/// The `upread mutex` can be upgraded to write mutex atomically, useful in
75/// scenarios where a decision to write is made after reading.
76///
77/// The type parameter `T` represents the data that this mutex is protecting.
78/// It is necessary for `T` to satisfy [`Send`] to be shared across tasks and
79/// [`Sync`] to permit concurrent access via readers. The [`Deref`] method (and
80/// [`DerefMut`] for the writer) is implemented for the RAII guards returned
81/// by the locking methods, which allows for the access to the protected data
82/// while the mutex is held.
83///
84/// # Usage
85///
86/// The mutex can be used in scenarios where data needs to be read frequently
87/// but written to occasionally.
88///
89/// Use `upread mutex` in scenarios where related checking is performed before
90/// modification to effectively avoid deadlocks and improve efficiency.
91///
92/// # Safety
93///
94/// Avoid using `RwMutex` in an interrupt context, as it may result in sleeping
95/// and never being awakened.
96///
97/// # Examples
98///
99/// ```
100/// use ostd::sync::RwMutex;
101///
102/// let mutex = RwMutex::new(5)
103///
104/// // many read mutexes can be held at once
105/// {
106///     let r1 = mutex.read();
107///     let r2 = mutex.read();
108///     assert_eq!(*r1, 5);
109///     assert_eq!(*r2, 5);
110///
111///     // Upgradeable read mutex can share access to data with read mutexes
112///     let r3 = mutex.upread();
113///     assert_eq!(*r3, 5);
114///     drop(r1);
115///     drop(r2);
116///     // read mutexes are dropped at this point
117///
118///     // An upread mutex can only be upgraded successfully after all the
119///     // read mutexes are released, otherwise it will spin-wait.
120///     let mut w1 = r3.upgrade();
121///     *w1 += 1;
122///     assert_eq!(*w1, 6);
123/// }   // upread mutex are dropped at this point
124///
125/// {
126///     // Only one write mutex can be held at a time
127///     let mut w2 = mutex.write();
128///     *w2 += 1;
129///     assert_eq!(*w2, 7);
130/// }   // write mutex is dropped at this point
131/// ```
132pub struct RwMutex<T /*: ?Sized*/> {
133    /// The internal representation of the mutex state is as follows:
134    /// - **Bit 63:** Writer mutex.
135    /// - **Bit 62:** Upgradeable reader mutex.
136    /// - **Bit 61:** Indicates if an upgradeable reader is being upgraded.
137    /// - **Bits 60-0:** Reader mutex count.
138    lock: AtomicUsize<_, RwPerms<T>, _>,
139    /// Threads that fail to acquire the mutex will sleep on this waitqueue.
140    queue: WaitQueue,
141    // val: UnsafeCell<T>,
142    val: PCell<T>,
143    ghost_id: Ghost<RwId>,
144}
145
146closed spec fn wf(self) -> bool {
147    invariant on lock with (val, ghost_id) is (v: usize, g: RwPerms<T>) {
148        let has_writer_bit: bool = (v & WRITER) != 0;
149        let has_upgrade_bit: bool = (v & UPGRADEABLE_READER) != 0;
150        let has_max_reader_bit: bool = (v & MAX_READER) != 0;
151        let total_reader_bits: int = (v & MAX_READER_MASK) as int;
152        let reader_bits: int = if has_max_reader_bit {
153            MAX_READER as int
154        } else {
155            (v & READER_MASK) as int
156        };
157
158        let active_writer: bool = g.core_token.is_right();
159        let active_upgrade_guard: bool = !active_writer && g.upreader_guard_token is None;
160        let active_read_guards: int = if g.read_guard_token.is_resource_vacant() {
161            0
162        } else {
163            MAX_READER - g.read_guard_token.frac()
164        };
165        let pending_failed_upread_attempt: bool = g.upread_retract_token is None;
166        let failed_reader_attempts: int = MAX_READER_MASK - g.read_retract_token.frac();
167
168        &&& if g.core_token.is_left() {
169            let resource = g.read_guard_token.resource();
170            let read_half_cell_perm = resource.0;
171            let mode_knowledge = resource.1;
172            &&& !g.read_guard_token.is_resource_vacant()
173            &&& mode_knowledge.id() == ghost_id@.core_token_id
174            &&& read_half_cell_perm.id() == ghost_id@.frac_id
175            &&& read_half_cell_perm.resource().id() == val.id()
176            &&& read_half_cell_perm.frac() == 1
177        } else {
178            &&& g.upreader_guard_token is None
179            &&& g.read_guard_token.is_resource_vacant()
180        }
181        &&& has_upgrade_bit <==> (active_upgrade_guard || pending_failed_upread_attempt)
182        &&& !(active_upgrade_guard && pending_failed_upread_attempt)
183        &&& total_reader_bits == active_read_guards + failed_reader_attempts
184        &&& active_writer <==> has_writer_bit
185        &&& 0 <= active_read_guards <= reader_bits <= total_reader_bits
186        &&& !(active_writer && (active_read_guards + if active_upgrade_guard { 1int } else { 0 }) > 0)
187        &&& g.core_token.id() == ghost_id@.core_token_id
188        &&& g.core_token.wf()
189        &&& g.core_token.is_left() ==> {
190            &&& !g.core_token.is_resource_owner()
191            &&& g.core_token.frac() == 1
192        }
193        &&& g.core_token.is_right() ==> {
194            let empty = g.core_token.resource_right();
195            &&& empty.id() == ghost_id@.frac_id
196            &&& g.core_token.frac() == 2
197            &&& g.core_token.has_resource()
198        }
199        &&& g.read_retract_token.wf()
200        &&& g.read_retract_token.id() == ghost_id@.read_retract_token_id
201        &&& g.upread_retract_token is Some ==> {
202            let token = g.upread_retract_token->0;
203            &&& token.wf()
204            &&& token.id() == ghost_id@.upread_retract_token_id
205        }
206        &&& g.upreader_guard_token is Some ==> {
207            let token = g.upreader_guard_token->0;
208            wf_upgradeable_guard_token(ghost_id@.core_token_id, ghost_id@.frac_id, val.id(), token)
209        }
210        &&& g.read_guard_token.wf()
211        &&& g.read_guard_token.id() == ghost_id@.read_guard_token_id
212    }
213}
214}
215
216const READER: usize = 1;
217
218const WRITER: usize = 1 << (usize::BITS - 1);
219
220const UPGRADEABLE_READER: usize = 1 << (usize::BITS - 2);
221
222const BEING_UPGRADED: usize = 1 << (usize::BITS - 3);
223
224/// This bit is reserved as an overflow sentinel.
225/// For more details, see comments on the `MAX_READER` constant
226/// in the [`super::rwlock`] module.
227const MAX_READER: usize = 1 << (usize::BITS - 4);
228
229const READER_MASK: usize = usize::MAX >> 4;
230
231const MAX_READER_MASK: usize = usize::MAX >> 3;
232
233pub closed spec fn no_max_reader_overflow(v: usize) -> bool {
234    v & MAX_READER_MASK < MAX_READER_MASK
235}
236
237impl<T> RwMutex<T> {
238    pub closed spec fn cell_id(self) -> cell::CellId {
239        self.val.id()
240    }
241
242    pub closed spec fn core_token_id(self) -> Loc {
243        self.ghost_id@.core_token_id
244    }
245
246    pub closed spec fn frac_id(self) -> Loc {
247        self.ghost_id@.frac_id
248    }
249
250    pub closed spec fn upread_retract_token_id(self) -> Loc {
251        self.ghost_id@.upread_retract_token_id
252    }
253
254    pub closed spec fn read_guard_token_id(self) -> Loc {
255        self.ghost_id@.read_guard_token_id
256    }
257
258    #[verifier::type_invariant]
259    pub closed spec fn type_inv(self) -> bool {
260        self.wf()
261    }
262}
263
264closed spec fn wf_upgradeable_guard_token<T>(
265    core_token_id: Loc,
266    frac_id: Loc,
267    cell_id: CellId,
268    token: OneLeftOwner<HalfPerm<T>, NoPerm<T>, 3>,
269) -> bool {
270    let half_cell_perm = token.resource();
271    &&& token.id() == core_token_id
272    &&& half_cell_perm.id() == frac_id
273    &&& half_cell_perm.resource().id() == cell_id
274    &&& token.has_resource()
275    &&& half_cell_perm.frac() == 1
276    &&& half_cell_perm.has_authority()
277    &&& token.wf()
278}
279
280impl<T> RwMutex<T> {
281    /// Creates a new read-write mutex with an initial value.
282    pub const fn new(val: T) -> Self {
283        let (val, Tracked(perm)) = PCell::new(val);
284
285        proof {
286            lemma_consts_properties();
287        }
288        let tracked mut frac_perm = Count::<PointsTo<T>>::alloc(perm);
289        let tracked read_half_cell_perm = frac_perm.split(1int);
290        let ghost frac_id = frac_perm.id();
291        let tracked mut core_token = SumResource::alloc_left(frac_perm);
292        let tracked read_retract_token = TokenResource::<MAX_READER_MASK>::alloc(());
293        let tracked upread_retract_token = UniqueToken::alloc(());
294        let tracked upreader_guard_token = core_token.split_one_left_owner();
295        let tracked left_token = core_token.split_one_left_knowledge();
296        let tracked read_guard_token = CountResource::<ReadPerm<T>, MAX_READER>::alloc(
297            (read_half_cell_perm, left_token),
298        );
299        let ghost ghost_id = RwId {
300            frac_id,
301            core_token_id: core_token.id(),
302            upread_retract_token_id: upread_retract_token.id(),
303            read_retract_token_id: read_retract_token.id(),
304            read_guard_token_id: read_guard_token.id(),
305        };
306        let tracked perms = RwPerms {
307            core_token,
308            read_retract_token,
309            upread_retract_token: Some(upread_retract_token),
310            upreader_guard_token: Some(upreader_guard_token),
311            read_guard_token,
312        };
313
314        Self {
315            lock: AtomicUsize::new(Ghost((val, Ghost(ghost_id))), 0, Tracked(perms)),
316            queue: WaitQueue::new(),
317            // val: UnsafeCell::new(val),
318            val,
319            ghost_id: Ghost(ghost_id),
320        }
321    }
322}
323
324#[verus_verify]
325impl<T  /*: ?Sized*/ > RwMutex<T> {
326    /// Acquires a read mutex and sleep until it can be acquired.
327    ///
328    /// The calling thread will sleep until there are no writers or upgrading
329    /// upreaders present. The implementation of [`WaitQueue`] guarantees the
330    /// order in which other concurrent readers or writers waiting simultaneously
331    /// will acquire the mutex.
332    #[track_caller]
333    pub fn read(&self) -> RwMutexReadGuard<'_, T> {
334        self.queue.wait_until(|| self.try_read())
335    }
336
337    /// Acquires a write mutex and sleep until it can be acquired.
338    ///
339    /// The calling thread will sleep until there are no writers, upreaders,
340    /// or readers present. The implementation of [`WaitQueue`] guarantees the
341    /// order in which other concurrent readers or writers waiting simultaneously
342    /// will acquire the mutex.
343    #[track_caller]
344    pub fn write(&self) -> RwMutexWriteGuard<'_, T> {
345        self.queue.wait_until(|| self.try_write())
346    }
347
348    /// Acquires a upread mutex and sleep until it can be acquired.
349    ///
350    /// The calling thread will sleep until there are no writers or upreaders present.
351    /// The implementation of [`WaitQueue`] guarantees the order in which other concurrent
352    /// readers or writers waiting simultaneously will acquire the mutex.
353    ///
354    /// Upreader will not block new readers until it tries to upgrade. Upreader
355    /// and reader do not differ before invoking the upgrade method. However,
356    /// only one upreader can exist at any time to avoid deadlock in the
357    /// upgrade method.
358    #[track_caller]
359    pub fn upread(&self) -> RwMutexUpgradeableGuard<'_, T> {
360        self.queue.wait_until(|| self.try_upread())
361    }
362
363    /// Attempts to acquire a read mutex.
364    ///
365    /// This function will never sleep and will return immediately.
366    #[verus_spec]
367    pub fn try_read(&self) -> Option<RwMutexReadGuard<'_, T>> {
368        proof_decl! {
369            let tracked mut read_token: Option<Count<ReadPerm<T>, MAX_READER>> = None;
370            let tracked mut retract_read_token: Option<Token<MAX_READER_MASK>> = None;
371        }
372        proof! {
373            use_type_invariant(self);
374            lemma_consts_properties();
375        }
376
377        let lock =
378            atomic_with_ghost!(
379            self.lock => fetch_add(READER);
380            update prev -> next;
381            ghost g => {
382                let prev_usize = prev as usize;
383                let next_usize = next as usize;
384                assume(no_max_reader_overflow(prev_usize));
385                lemma_consts_properties_value(prev_usize);
386                lemma_consts_properties_prev_next(prev_usize, next_usize);
387                if prev_usize & (WRITER | BEING_UPGRADED | MAX_READER) == 0 {
388                    read_token = Some(g.read_guard_token.split_one());
389                } else {
390                    retract_read_token = Some(g.read_retract_token.split_one());
391                }
392            }
393        );
394
395        if lock & (WRITER | BEING_UPGRADED | MAX_READER) == 0 {
396            Some(
397                RwMutexReadGuard {
398                    inner: self,
399                    tracked_token: Tracked(read_token.tracked_unwrap()),
400                },
401            )
402        } else {
403            atomic_with_ghost!(
404                self.lock => fetch_sub(READER);
405                update prev -> next;
406                ghost g => {
407                    let prev_usize = prev as usize;
408                    let next_usize = next as usize;
409                    lemma_consts_properties_value(next_usize);
410                    lemma_consts_properties_prev_next(prev_usize, next_usize);
411                    g.read_retract_token.combine(retract_read_token.tracked_unwrap());
412                }
413            );
414            None
415        }
416    }
417
418    /// Attempts to acquire a write mutex.
419    ///
420    /// This function will never sleep and will return immediately.
421    pub fn try_write(&self) -> Option<RwMutexWriteGuard<'_, T>> {
422        proof_decl! {
423            let tracked mut guard_perm: Option<PointsTo<T>> = None;
424            let tracked mut guard_token: Option<OneRightKnowledge<HalfPerm<T>, NoPerm<T>, 3>> = None;
425        }
426        proof! {
427            use_type_invariant(self);
428            lemma_consts_properties();
429        }
430
431        if atomic_with_ghost!(
432            self.lock => compare_exchange(0, WRITER);
433            update prev -> next;
434            returning res;
435            ghost g => {
436                let prev_usize = prev as usize;
437                let next_usize = next as usize;
438                if res is Ok {
439                    let tracked read_resource = g.read_guard_token.take_resource();
440                    let tracked (read_half_cell_perm, left_token) = read_resource;
441                    g.core_token.join_one_left_knowledge(left_token);
442                    let tracked upreader_guard_token = g.upreader_guard_token.tracked_take();
443                    g.core_token.join_one_left_owner(upreader_guard_token);
444                    let tracked mut pointsto = g.core_token.take_resource_left();
445                    pointsto.combine(read_half_cell_perm);
446                    let tracked (pointsto, empty) = pointsto.take_resource();
447                    guard_perm = Some(pointsto);
448                    g.core_token.change_to_right(empty);
449                    guard_token = Some(g.core_token.split_one_right_knowledge());
450                } else {
451                    lemma_consts_properties_prev_next(prev_usize, next_usize);
452                }
453            }
454        ).is_ok() {
455            Some(
456                RwMutexWriteGuard {
457                    inner: self,
458                    tracked_perm: Tracked(guard_perm.tracked_unwrap()),
459                    tracked_token: Tracked(guard_token.tracked_unwrap()),
460                },
461            )
462        } else {
463            None
464        }
465    }
466
467    /// Attempts to acquire a upread mutex.
468    ///
469    /// This function will never sleep and will return immediately.
470    pub fn try_upread(&self) -> Option<RwMutexUpgradeableGuard<'_, T>> {
471        proof_decl! {
472            let tracked mut upgrade_guard_token: Option<OneLeftOwner<HalfPerm<T>, NoPerm<T>, 3>> = None;
473            let tracked mut retract_upgrade_token: Option<UniqueToken> = None;
474        }
475        proof! {
476            use_type_invariant(self);
477            lemma_consts_properties();
478        }
479
480        let lock =
481            atomic_with_ghost!(
482            self.lock => fetch_or(UPGRADEABLE_READER);
483            update prev -> next;
484            ghost g => {
485                lemma_consts_properties_value(prev);
486                lemma_consts_properties_prev_next(prev, next);
487                if prev & (WRITER | UPGRADEABLE_READER) == 0 {
488                    upgrade_guard_token = Some(g.upreader_guard_token.tracked_take());
489                } else if prev & (WRITER | UPGRADEABLE_READER) == WRITER {
490                    retract_upgrade_token = Some(g.upread_retract_token.tracked_take());
491                }
492            }
493        )
494            & (WRITER | UPGRADEABLE_READER);
495
496        if lock == 0 {
497            return Some(
498                RwMutexUpgradeableGuard {
499                    inner: self,
500                    tracked_token: Tracked(upgrade_guard_token.tracked_unwrap()),
501                },
502            );
503        } else if lock == WRITER {
504            atomic_with_ghost!(
505                self.lock => fetch_sub(UPGRADEABLE_READER);
506                update prev -> next;
507                ghost g => {
508                    let prev_usize = prev as usize;
509                    let next_usize = next as usize;
510                    lemma_consts_properties_value(prev_usize);
511                    lemma_consts_properties_prev_next(prev_usize, next_usize);
512                    if g.upread_retract_token is Some {
513                        let tracked mut token = retract_upgrade_token.tracked_unwrap();
514                        token.validate_with_other(g.upread_retract_token.tracked_borrow());
515                    } else {
516                        g.upread_retract_token = retract_upgrade_token;
517                    }
518                }
519            );
520        }
521        None
522    }/* /// Returns a mutable reference to the underlying data.
523    ///
524    /// This method is zero-cost: By holding a mutable reference to the lock, the compiler has
525    /// already statically guaranteed that access to the data is exclusive.
526    pub fn get_mut(&mut self) -> &mut T {
527        self.val.get_mut()
528    } */
529
530}
531
532/* impl<T: /*: ?Sized +*/ fmt::Debug> fmt::Debug for RwMutex<T> {
533    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
534        fmt::Debug::fmt(&self.val, f)
535    }
536} */
537
538// There can be more than one readers to get the `T`'s immutable reference,
539// so `T` must be `Sync` to guarantee the sharing safety.
540#[verifier::external]
541unsafe impl<T:   /*: ?Sized +*/ Send> Send for RwMutex<T> {
542
543}
544
545#[verifier::external]
546unsafe impl<T:   /*: ?Sized +*/ Send + Sync> Sync for RwMutex<T> {
547
548}
549
550impl<T  /*: ?Sized*/ > !Send for RwMutexWriteGuard<'_, T> {
551
552}
553
554#[verifier::external]
555unsafe impl<T:   /*: ?Sized +*/ Sync> Sync for RwMutexWriteGuard<'_, T> {
556
557}
558
559impl<T  /*: ?Sized*/ > !Send for RwMutexReadGuard<'_, T> {
560
561}
562
563#[verifier::external]
564unsafe impl<T:   /*: ?Sized +*/ Sync> Sync for RwMutexReadGuard<'_, T> {
565
566}
567
568impl<T  /*: ?Sized*/ > !Send for RwMutexUpgradeableGuard<'_, T> {
569
570}
571
572#[verifier::external]
573unsafe impl<T:   /*: ?Sized +*/ Sync> Sync for RwMutexUpgradeableGuard<'_, T> {
574
575}
576
577/// A guard that provides immutable data access.
578#[verifier::reject_recursive_types(T)]
579#[clippy::has_significant_drop]
580#[must_use]
581pub struct RwMutexReadGuard<'a, T  /*: ?Sized*/ > {
582    inner: &'a RwMutex<T>,
583    tracked_token: Tracked<Count<ReadPerm<T>, MAX_READER>>,
584}
585
586impl<'a, T> RwMutexReadGuard<'a, T> {
587    #[verifier::type_invariant]
588    pub closed spec fn type_inv(self) -> bool {
589        let resource = self.tracked_token@.resource();
590        let read_half_cell_perm = resource.0;
591        let mode_knowledge = resource.1;
592        &&& self.inner.core_token_id() == mode_knowledge.id()
593        &&& self.inner.frac_id() == read_half_cell_perm.id()
594        &&& self.inner.cell_id() == read_half_cell_perm.resource().id()
595        &&& self.tracked_token@.id() == self.inner.read_guard_token_id()
596        &&& read_half_cell_perm.frac() == 1
597        &&& self.tracked_token@.frac() == 1
598    }
599
600    pub closed spec fn value(self) -> T {
601        *self.tracked_token@.resource().0.resource().value()
602    }
603
604    pub open spec fn view(self) -> T {
605        self.value()
606    }
607}
608
609impl<T  /*: ?Sized*/ > Deref for RwMutexReadGuard<'_, T> {
610    type Target = T;
611
612    #[verus_spec(returns self.view())]
613    fn deref(&self) -> &T {
614        proof! {
615            use_type_invariant(self);
616        }
617        // unsafe { &*self.inner.val.get() }
618        self.inner.val.borrow(
619            Tracked(self.tracked_token.borrow().tracked_borrow().0.tracked_borrow()),
620        )
621    }
622}
623
624impl<T: fmt::Debug> DebugSpecImpl for RwMutexReadGuard<'_, T> {
625    open spec fn fmt_req(&self, f: &fmt::Formatter<'_>) -> bool {
626        self.view().fmt_req(f)
627    }
628}
629
630impl<T: fmt::Debug> fmt::Debug for RwMutexReadGuard<'_, T> {
631    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
632        fmt::Debug::fmt(&**self, f)
633    }
634}
635
636impl<T  /* : ?Sized */ > RwMutexReadGuard<'_, T> {
637    fn drop(self) {
638        // When there are no readers, wake up a waiting writer.
639        proof! {
640            use_type_invariant(&self);
641            use_type_invariant(self.inner);
642            lemma_consts_properties();
643        }
644        proof_decl! {
645            let tracked token = self.tracked_token.get();
646        }
647        if atomic_with_ghost!(
648            self.inner.lock => fetch_sub(READER);
649            update prev -> next;
650            ghost g => {
651                let prev_usize = prev as usize;
652                let next_usize = next as usize;
653                assume(no_max_reader_overflow(prev_usize));
654                lemma_consts_properties_value(next_usize);
655                lemma_consts_properties_prev_next(prev_usize, next_usize);
656                g.core_token.validate_with_one_left_knowledge(&token.tracked_borrow().1);
657                g.read_guard_token.combine(token);
658            }
659        )
660            == READER {
661            self.inner.queue.wake_one();
662        }
663    }
664}
665
666/// A guard that provides mutable data access.
667#[clippy::has_significant_drop]
668#[must_use]
669#[verifier::reject_recursive_types(T)]
670pub struct RwMutexWriteGuard<'a, T  /*: ?Sized*/ > {
671    inner: &'a RwMutex<T>,
672    tracked_perm: Tracked<PointsTo<T>>,
673    tracked_token: Tracked<OneRightKnowledge<HalfPerm<T>, NoPerm<T>, 3>>,
674}
675
676impl<'a, T> RwMutexWriteGuard<'a, T> {
677    #[verifier::type_invariant]
678    spec fn type_inv(self) -> bool {
679        &&& self.inner.cell_id() == self.tracked_perm@.id()
680        &&& self.inner.core_token_id() == self.tracked_token@.id()
681    }
682
683    pub closed spec fn value(self) -> T {
684        *self.tracked_perm@.value()
685    }
686
687    pub open spec fn view(self) -> T {
688        self.value()
689    }
690}
691
692impl<T  /*: ?Sized*/ > Deref for RwMutexWriteGuard<'_, T> {
693    type Target = T;
694
695    #[verus_spec(returns self.view())]
696    fn deref(&self) -> &T {
697        proof! {
698            use_type_invariant(self);
699        }
700        // unsafe { &*self.inner.val.get() }
701        self.inner.val.borrow(Tracked(self.tracked_perm.borrow()))
702    }
703}
704
705impl<T: fmt::Debug> DebugSpecImpl for RwMutexWriteGuard<'_, T> {
706    open spec fn fmt_req(&self, f: &fmt::Formatter<'_>) -> bool {
707        self.view().fmt_req(f)
708    }
709}
710
711impl<T: fmt::Debug> fmt::Debug for RwMutexWriteGuard<'_, T> {
712    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
713        fmt::Debug::fmt(&**self, f)
714    }
715}
716
717impl<'a, T  /*: ?Sized*/ > RwMutexWriteGuard<'a, T> {
718    /// Atomically downgrades a write guard to an upgradeable reader guard.
719    ///
720    /// This method always succeeds because the lock is exclusively held by the writer.
721    #[verifier::exec_allows_no_decreases_clause]
722    pub fn downgrade(mut self) -> RwMutexUpgradeableGuard<'a, T> {
723        loop {
724            self =
725            match self.try_downgrade() {
726                Ok(guard) => return guard,
727                Err(e) => e,
728            };
729        }
730    }
731
732    /// This is not exposed as a public method to prevent intermediate lock states from affecting the
733    /// downgrade process.
734    fn try_downgrade(self) -> Result<RwMutexUpgradeableGuard<'a, T>, Self> {
735        proof! {
736            use_type_invariant(&self);
737            use_type_invariant(self.inner);
738            lemma_consts_properties();
739        }
740        proof_decl! {
741            let tracked perm = self.tracked_perm.get();
742            let tracked token = self.tracked_token.get();
743            let tracked mut upgrade_guard_token: Option<OneLeftOwner<HalfPerm<T>, NoPerm<T>, 3>> = None;
744            let tracked mut err_perm: Option<PointsTo<T>> = None;
745            let tracked mut err_write_guard_token: Option<OneRightKnowledge<HalfPerm<T>, NoPerm<T>, 3>> = None;
746        }
747        let inner = self.inner;
748        let res =
749            atomic_with_ghost!(
750            self.inner.lock => compare_exchange(WRITER, UPGRADEABLE_READER);
751            update prev -> next;
752            returning res;
753            ghost g => {
754                lemma_consts_properties_prev_next(prev, next);
755                if res is Ok {
756                    g.core_token.validate_with_one_right_knowledge(&token);
757                    g.core_token.join_one_right_knowledge(token);
758                    let tracked empty = g.core_token.take_resource_right();
759                    let tracked mut full = empty.put_resource(perm);
760                    let tracked read_half_cell_perm = full.split(1int);
761                    g.core_token.change_to_left(full);
762                    upgrade_guard_token = Some(g.core_token.split_one_left_owner());
763                    let tracked left_token = g.core_token.split_one_left_knowledge();
764                    g.read_guard_token.put_resource((read_half_cell_perm, left_token));
765                } else {
766                    err_perm = Some(perm);
767                    err_write_guard_token = Some(token);
768                }
769            }
770        );
771
772        if res.is_ok() {
773            // drop(self);
774            atomic_with_ghost! {
775                self.inner.lock => fetch_and(!WRITER);
776                update prev -> next;
777                ghost g => {
778                    let prev_usize = prev as usize;
779                    let next_usize = next as usize;
780                    let tracked mut guard_token = upgrade_guard_token.tracked_unwrap();
781                    g.core_token.validate_with_one_left_owner(&guard_token);
782                    if g.upreader_guard_token is Some {
783                        guard_token.validate_with_one_left_owner(
784                            g.upreader_guard_token.tracked_borrow(),
785                        );
786                        assert(false);
787                    }
788                    upgrade_guard_token = Some(guard_token);
789                    lemma_consts_properties_value(prev_usize);
790                    lemma_consts_properties_prev_next(prev_usize, next_usize);
791                    lemma_consts_properties_value(next_usize);
792                }
793            };
794            self.inner.queue.wake_all();
795            Ok(
796                RwMutexUpgradeableGuard {
797                    inner,
798                    tracked_token: Tracked(upgrade_guard_token.tracked_unwrap()),
799                },
800            )
801        } else {
802            Err(
803                RwMutexWriteGuard {
804                    inner,
805                    tracked_perm: Tracked(err_perm.tracked_unwrap()),
806                    tracked_token: Tracked(err_write_guard_token.tracked_unwrap()),
807                },
808            )
809        }
810    }
811
812    pub fn drop(self) {
813        proof! {
814            use_type_invariant(&self);
815            use_type_invariant(self.inner);
816            lemma_consts_properties();
817        }
818        proof_decl! {
819            let tracked perm = self.tracked_perm.get();
820            let tracked token = self.tracked_token.get();
821        }
822        atomic_with_ghost! {
823            self.inner.lock => fetch_and(!WRITER);
824            update prev -> next;
825            ghost g => {
826                let prev_usize = prev as usize;
827                let next_usize = next as usize;
828                lemma_consts_properties_prev_next(prev_usize, next_usize);
829                lemma_consts_properties_value(next_usize);
830                g.core_token.validate_with_one_right_knowledge(&token);
831                g.core_token.join_one_right_knowledge(token);
832                let tracked empty = g.core_token.take_resource_right();
833                let tracked mut full = empty.put_resource(perm);
834                let tracked read_half_cell_perm = full.split(1int);
835                g.core_token.change_to_left(full);
836                let tracked upreader_guard_token = g.core_token.split_one_left_owner();
837                g.upreader_guard_token = Some(upreader_guard_token);
838                let tracked left_token = g.core_token.split_one_left_knowledge();
839                g.read_guard_token.put_resource((read_half_cell_perm, left_token));
840            }
841        };
842        // When the current writer releases, wake up all the sleeping threads.
843        // All awakened threads may include readers and writers.
844        // Thanks to the `wait_until` method, either all readers
845        // continue to execute or one writer continues to execute.
846        self.inner.queue.wake_all();
847    }
848}
849
850#[verus_verify]
851impl<T  /*: ?Sized*/ > DerefMut for RwMutexWriteGuard<'_, T> {
852    #[verus_spec(ret =>
853        ensures
854            final(self).view() == *final(ret),
855            old(self).view() == *ret,
856    )]
857    fn deref_mut(&mut self) -> (ret: &mut Self::Target) {
858        proof! {
859            use_type_invariant(&*self);
860        }
861        //unsafe { &mut *self.inner.val.get() }
862        self.inner.val.borrow_mut(Tracked(&mut *self.tracked_perm))
863    }
864}
865
866/// A guard that provides immutable data access but can be atomically
867/// upgraded to [`RwMutexWriteGuard`].
868#[verifier::reject_recursive_types(T)]
869pub struct RwMutexUpgradeableGuard<'a, T  /*: ?Sized*/ > {
870    inner: &'a RwMutex<T>,
871    tracked_token: Tracked<OneLeftOwner<HalfPerm<T>, NoPerm<T>, 3>>,
872}
873
874impl<'a, T  /*: ?Sized*/ > RwMutexUpgradeableGuard<'a, T> {
875    #[verifier::type_invariant]
876    pub closed spec fn type_inv(self) -> bool {
877        wf_upgradeable_guard_token(
878            self.inner.core_token_id(),
879            self.inner.frac_id(),
880            self.inner.cell_id(),
881            self.tracked_token@,
882        )
883    }
884
885    pub closed spec fn value(self) -> T {
886        *self.tracked_token@.resource().resource().value()
887    }
888
889    pub open spec fn view(self) -> T {
890        self.value()
891    }
892}
893
894#[verus_verify]
895impl<'a, T> RwMutexUpgradeableGuard<'a, T> {
896    /// Upgrades this upread guard to a write guard atomically.
897    ///
898    /// After calling this method, subsequent readers will be blocked
899    /// while previous readers remain unaffected.
900    ///
901    /// The calling thread will not sleep, but spin to wait for the existing
902    /// reader to be released. There are two main reasons.
903    /// - First, it needs to sleep in an extra waiting queue and needs extra wake-up logic and overhead.
904    /// - Second, upgrading method usually requires a high response time (because the mutex is being used now).
905    #[verifier::exec_allows_no_decreases_clause]
906    pub fn upgrade(mut self) -> RwMutexWriteGuard<'a, T> {
907        proof! {
908            use_type_invariant(&self);
909            use_type_invariant(&self.inner);
910            lemma_consts_properties();
911        }
912        atomic_with_ghost!(
913            self.inner.lock => fetch_or(BEING_UPGRADED);
914            update prev -> next;
915            ghost g => {
916                lemma_consts_properties_prev_next(prev, next);
917            }
918        );
919        loop {
920            self =
921            match self.try_upgrade() {
922                Ok(guard) => return guard,
923                Err(e) => e,
924            };
925        }
926    }
927
928    // [FIXED] BUG FOUND BY FV: deadlock. https://github.com/asterinas/asterinas/pull/3007
929    /// Attempts to upgrade this upread guard to a write guard atomically.
930    ///
931    /// This function will return immediately.
932    ///
933    /// This function is not exposed publicly because the `BEING_UPGRADED` bit
934    /// is set only in [`Self::upgrade`].
935    #[verus_spec]
936    fn try_upgrade(self) -> Result<RwMutexWriteGuard<'a, T>, Self> {
937        proof! {
938            use_type_invariant(&self);
939            use_type_invariant(self.inner);
940            lemma_consts_properties();
941        }
942        proof_decl! {
943            let tracked upread_guard_token = self.tracked_token.get();
944            let tracked mut write_perm: Option<PointsTo<T>> = None;
945            let tracked mut err_upread_guard_token: Option<OneLeftOwner<HalfPerm<T>, NoPerm<T>, 3>> = None;
946            let tracked mut retract_upgrade_token: Option<UniqueToken> = None;
947            let tracked mut write_guard_token: Option<OneRightKnowledge<HalfPerm<T>, NoPerm<T>, 3>> = None;
948        }
949
950        let res =
951            atomic_with_ghost!(
952            self.inner.lock => compare_exchange(UPGRADEABLE_READER | BEING_UPGRADED, WRITER | UPGRADEABLE_READER);
953            update prev -> next;
954            returning res;
955            ghost g => {
956                lemma_consts_properties_prev_next(prev, next);
957                if res is Ok {
958                    g.core_token.validate_with_one_left_owner(&upread_guard_token);
959                    if g.upreader_guard_token is Some {
960                        upread_guard_token.validate_with_one_left_owner(g.upreader_guard_token.tracked_borrow());
961                    }
962                    g.core_token.join_one_left_owner(upread_guard_token);
963                    let tracked read_resource = g.read_guard_token.take_resource();
964                    let tracked (read_half_cell_perm, left_token) = read_resource;
965                    g.core_token.join_one_left_knowledge(left_token);
966                    let tracked mut pointsto = g.core_token.take_resource_left();
967                    pointsto.combine(read_half_cell_perm);
968                    let tracked (pointsto, empty) = pointsto.take_resource();
969                    write_perm = Some(pointsto);
970                    g.core_token.change_to_right(empty);
971                    write_guard_token = Some(g.core_token.split_one_right_knowledge());
972                    retract_upgrade_token = Some(g.upread_retract_token.tracked_take());
973                } else {
974                    err_upread_guard_token = Some(upread_guard_token);
975                }
976            }
977        );
978
979        if res.is_ok() {
980            let inner = self.inner;
981            atomic_with_ghost!(
982                inner.lock => fetch_sub(UPGRADEABLE_READER);
983                update prev -> next;
984                ghost g => {
985                    let prev_usize = prev as usize;
986                    let next_usize = next as usize;
987                    lemma_consts_properties_value(prev_usize);
988                    lemma_consts_properties_prev_next(prev_usize, next_usize);
989                    let tracked mut token = retract_upgrade_token.tracked_unwrap();
990                    if g.upread_retract_token is Some {
991                        token.validate_with_other(g.upread_retract_token.tracked_borrow());
992                    }
993                    g.upread_retract_token = Some(token);
994                }
995            );
996            Ok(
997                RwMutexWriteGuard {
998                    inner,
999                    tracked_perm: Tracked(write_perm.tracked_unwrap()),
1000                    tracked_token: Tracked(write_guard_token.tracked_unwrap()),
1001                },
1002            )
1003        } else {
1004            Err(
1005                RwMutexUpgradeableGuard {
1006                    inner: self.inner,
1007                    tracked_token: Tracked(err_upread_guard_token.tracked_unwrap()),
1008                },
1009            )
1010        }
1011    }
1012
1013    #[verus_spec]
1014    pub fn drop(self) {
1015        proof! {
1016            use_type_invariant(&self);
1017            use_type_invariant(self.inner);
1018            lemma_consts_properties();
1019        }
1020        proof_decl! {
1021            let tracked guard_token = self.tracked_token.get();
1022        }
1023        let res =
1024            atomic_with_ghost!(
1025            self.inner.lock => fetch_sub(UPGRADEABLE_READER);
1026            update prev -> next;
1027            ghost g => {
1028                let prev_usize = prev as usize;
1029                let next_usize = next as usize;
1030                lemma_consts_properties_value(prev_usize);
1031                lemma_consts_properties_prev_next(prev_usize, next_usize);
1032                g.core_token.validate_with_one_left_owner(&guard_token);
1033                if g.upreader_guard_token is Some {
1034                    guard_token.validate_with_one_left_owner(g.upreader_guard_token.tracked_borrow());
1035                    assert(false);
1036                } else {
1037                    g.upreader_guard_token = Some(guard_token);
1038                }
1039            }
1040        );
1041        if res == UPGRADEABLE_READER {
1042            self.inner.queue.wake_all();
1043        }
1044    }
1045}
1046
1047impl<T  /*: ?Sized*/ > Deref for RwMutexUpgradeableGuard<'_, T> {
1048    type Target = T;
1049
1050    #[verus_spec(returns self.view())]
1051    fn deref(&self) -> &T {
1052        proof! {
1053            use_type_invariant(self);
1054        }
1055        // unsafe { &*self.inner.val.get() }
1056        self.inner.val.borrow(
1057            Tracked(self.tracked_token.borrow().tracked_borrow().tracked_borrow()),
1058        )
1059    }
1060}
1061
1062impl<T: fmt::Debug> DebugSpecImpl for RwMutexUpgradeableGuard<'_, T> {
1063    open spec fn fmt_req(&self, f: &fmt::Formatter<'_>) -> bool {
1064        self.view().fmt_req(f)
1065    }
1066}
1067
1068impl<T: fmt::Debug> fmt::Debug for RwMutexUpgradeableGuard<'_, T> {
1069    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
1070        fmt::Debug::fmt(&**self, f)
1071    }
1072}
1073
1074#[verifier::bit_vector]
1075proof fn lemma_consts_properties()
1076    ensures
1077        0 & WRITER == 0,
1078        0 & UPGRADEABLE_READER == 0,
1079        0 & BEING_UPGRADED == 0,
1080        0 & READER_MASK == 0,
1081        0 & MAX_READER_MASK == 0,
1082        0 & MAX_READER == 0,
1083        0 & READER == 0,
1084        WRITER == 0x8000_0000_0000_0000,
1085        UPGRADEABLE_READER == 0x4000_0000_0000_0000,
1086        BEING_UPGRADED == 0x2000_0000_0000_0000,
1087        READER_MASK == 0x0FFF_FFFF_FFFF_FFFF,
1088        MAX_READER_MASK == 0x1FFF_FFFF_FFFF_FFFF,
1089        MAX_READER == 0x1000_0000_0000_0000,
1090        WRITER & WRITER == WRITER,
1091        WRITER & !WRITER == 0,
1092        WRITER & BEING_UPGRADED == 0,
1093        WRITER & READER_MASK == 0,
1094        WRITER & MAX_READER_MASK == 0,
1095        WRITER & MAX_READER == 0,
1096        WRITER & UPGRADEABLE_READER == 0,
1097        BEING_UPGRADED & WRITER == 0,
1098        BEING_UPGRADED & UPGRADEABLE_READER == 0,
1099        UPGRADEABLE_READER & BEING_UPGRADED == 0,
1100        UPGRADEABLE_READER & READER_MASK == 0,
1101        UPGRADEABLE_READER & MAX_READER_MASK == 0,
1102        UPGRADEABLE_READER & MAX_READER == 0,
1103        BEING_UPGRADED & READER_MASK == 0,
1104        BEING_UPGRADED & MAX_READER_MASK == 0,
1105        BEING_UPGRADED & MAX_READER == 0,
1106        (UPGRADEABLE_READER | BEING_UPGRADED) & WRITER == 0,
1107        (UPGRADEABLE_READER | BEING_UPGRADED) & UPGRADEABLE_READER == UPGRADEABLE_READER,
1108        (UPGRADEABLE_READER | BEING_UPGRADED) & BEING_UPGRADED == BEING_UPGRADED,
1109        (UPGRADEABLE_READER | BEING_UPGRADED) & READER_MASK == 0,
1110        (UPGRADEABLE_READER | BEING_UPGRADED) & MAX_READER_MASK == 0,
1111        (UPGRADEABLE_READER | BEING_UPGRADED) & MAX_READER == 0,
1112        (WRITER | UPGRADEABLE_READER) & WRITER == WRITER,
1113        (WRITER | UPGRADEABLE_READER) & UPGRADEABLE_READER == UPGRADEABLE_READER,
1114        (WRITER | UPGRADEABLE_READER) & BEING_UPGRADED == 0,
1115        (WRITER | UPGRADEABLE_READER) & READER_MASK == 0,
1116        (WRITER | UPGRADEABLE_READER) & MAX_READER_MASK == 0,
1117        (WRITER | UPGRADEABLE_READER) & MAX_READER == 0,
1118{
1119}
1120
1121#[verifier::bit_vector]
1122proof fn lemma_consts_properties_value(prev: usize)
1123    ensures
1124        no_max_reader_overflow(prev) ==> prev + READER <= usize::MAX,
1125        prev & (WRITER | BEING_UPGRADED | MAX_READER) == 0 ==> {
1126            &&& prev & WRITER == 0
1127            &&& prev & BEING_UPGRADED == 0
1128            &&& prev & MAX_READER == 0
1129        },
1130        prev & (WRITER | UPGRADEABLE_READER) == 0 ==> {
1131            &&& prev & WRITER == 0
1132            &&& prev & UPGRADEABLE_READER == 0
1133        },
1134        prev & MAX_READER == 0 ==> prev & READER_MASK == prev & MAX_READER_MASK,
1135        prev & MAX_READER != 0 ==> prev & MAX_READER_MASK >= MAX_READER,
1136        prev & (WRITER | UPGRADEABLE_READER) == WRITER ==> {
1137            &&& prev & UPGRADEABLE_READER == 0
1138            &&& prev & WRITER == WRITER
1139        },
1140        prev & UPGRADEABLE_READER != 0 ==> prev >= UPGRADEABLE_READER,
1141        prev & UPGRADEABLE_READER == 0 ==> {
1142            ||| prev & (WRITER | UPGRADEABLE_READER) == 0
1143            ||| prev & (WRITER | UPGRADEABLE_READER) == WRITER
1144        },
1145{
1146}
1147
1148#[verifier::bit_vector]
1149proof fn lemma_consts_properties_prev_next(prev: usize, next: usize)
1150    ensures
1151        prev & READER_MASK < MAX_READER,
1152        next == UPGRADEABLE_READER && prev == WRITER ==> {
1153            &&& next & WRITER == 0
1154            &&& next & UPGRADEABLE_READER == UPGRADEABLE_READER
1155            &&& next & READER_MASK == 0
1156            &&& next & MAX_READER_MASK == 0
1157            &&& next & MAX_READER == 0
1158            &&& next & BEING_UPGRADED == 0
1159        },
1160        next == prev | UPGRADEABLE_READER ==> {
1161            &&& next & UPGRADEABLE_READER != 0
1162            &&& next & WRITER == prev & WRITER
1163            &&& next & READER_MASK == prev & READER_MASK
1164            &&& next & MAX_READER_MASK == prev & MAX_READER_MASK
1165            &&& next & MAX_READER == prev & MAX_READER
1166            &&& next & BEING_UPGRADED == prev & BEING_UPGRADED
1167        },
1168        next == prev | BEING_UPGRADED ==> {
1169            &&& next & BEING_UPGRADED != 0
1170            &&& next & WRITER == prev & WRITER
1171            &&& next & UPGRADEABLE_READER == prev & UPGRADEABLE_READER
1172            &&& next & READER_MASK == prev & READER_MASK
1173            &&& next & MAX_READER_MASK == prev & MAX_READER_MASK
1174            &&& next & MAX_READER == prev & MAX_READER
1175        },
1176        next == prev - UPGRADEABLE_READER && prev & UPGRADEABLE_READER != 0 ==> {
1177            &&& next & UPGRADEABLE_READER == 0
1178            &&& next & WRITER == prev & WRITER
1179            &&& next & READER_MASK == prev & READER_MASK
1180            &&& next & MAX_READER_MASK == prev & MAX_READER_MASK
1181            &&& next & MAX_READER == prev & MAX_READER
1182            &&& next & BEING_UPGRADED == prev & BEING_UPGRADED
1183        },
1184        next == prev - READER && prev & READER_MASK != 0 ==> {
1185            &&& next & READER_MASK == (prev & READER_MASK) - READER
1186            &&& next & MAX_READER_MASK == (prev & MAX_READER_MASK) - READER
1187            &&& next & UPGRADEABLE_READER == prev & UPGRADEABLE_READER
1188            &&& next & WRITER == prev & WRITER
1189            &&& next & MAX_READER == prev & MAX_READER
1190            &&& next & BEING_UPGRADED == prev & BEING_UPGRADED
1191        },
1192        next == prev - READER && prev & MAX_READER_MASK != 0 ==> {
1193            &&& next & MAX_READER_MASK == (prev & MAX_READER_MASK) - READER
1194            &&& next & UPGRADEABLE_READER == prev & UPGRADEABLE_READER
1195            &&& next & WRITER == prev & WRITER
1196            &&& next & BEING_UPGRADED == prev & BEING_UPGRADED
1197        },
1198        next == prev + READER && no_max_reader_overflow(prev) ==> {
1199            &&& next & READER_MASK == if (prev & READER_MASK) + READER == MAX_READER {
1200                0
1201            } else {
1202                (prev & READER_MASK) + READER
1203            }
1204            &&& next & MAX_READER_MASK == (prev & MAX_READER_MASK) + READER
1205            &&& next & UPGRADEABLE_READER == prev & UPGRADEABLE_READER
1206            &&& next & WRITER == prev & WRITER
1207            &&& next & MAX_READER == if (prev & READER_MASK) + READER == MAX_READER {
1208                MAX_READER
1209            } else {
1210                prev & MAX_READER
1211            }
1212            &&& next & BEING_UPGRADED == prev & BEING_UPGRADED
1213        },
1214        next == prev & !WRITER ==> {
1215            &&& next & WRITER == 0
1216            &&& next & UPGRADEABLE_READER == prev & UPGRADEABLE_READER
1217            &&& next & READER_MASK == prev & READER_MASK
1218            &&& next & MAX_READER_MASK == prev & MAX_READER_MASK
1219            &&& next & MAX_READER == prev & MAX_READER
1220            &&& next & BEING_UPGRADED == prev & BEING_UPGRADED
1221        },
1222{
1223}
1224
1225} // verus!
ostd/sync/rwmutex.rs

ostd/sync/
rwmutex.rs
