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

ostd/sync/
rwmutex.rs
