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

ostd/sync/
rwmutex.rs
