ostd/sync/
rwmutex.rs

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

ostd/sync/
rwmutex.rs
