ostd/sync/
guard.rs

1// SPDX-License-Identifier: MPL-2.0
2use vstd::prelude::*;
3
4use crate::{
5    task::{/* atomic_mode::AsAtomicModeGuard, */ disable_preempt, DisabledPreemptGuard},
6    trap::irq::{disable_local, DisabledLocalIrqGuard},
7};
8
9/// A guardian that denotes the guard behavior for holding a spin-based lock.
10///
11/// It at least ensures that the atomic mode is maintained while the lock is held.
12#[verus_verify]
13pub trait SpinGuardian {
14    /// The guard type for holding a spin lock or a spin-based write lock.
15    type Guard: GuardTransfer;
16    /// The guard type for holding a spin-based read lock.
17    type ReadGuard: GuardTransfer;
18
19    /// Creates a new guard.
20    fn guard() -> Self::Guard;
21    /// Creates a new read guard.
22    fn read_guard() -> Self::ReadGuard;
23}
24
25verus! {
26
27/// The Guard can be transferred atomically.
28#[verus_verify]
29pub trait GuardTransfer: Sized {
30    /// Atomically transfers the current guard to a new instance.
31    ///
32    /// This function ensures that there are no 'gaps' between the destruction of the old guard and
33    /// the creation of the new guard, thereby maintaining the atomicity of guard transitions.
34    ///
35    /// The original guard must be dropped immediately after calling this method.
36    fn transfer_to(&mut self) -> Self
37        no_unwind
38    ;
39}
40
41} // verus!
42/// A guardian that disables preemption while holding a lock.
43#[verifier::external]
44pub enum PreemptDisabled {}
45
46#[verifier::external_type_specification]
47#[verifier::external_body]
48pub struct ExPreemptDisabled(PreemptDisabled);
49
50#[verus_verify]
51impl SpinGuardian for PreemptDisabled {
52    type Guard = DisabledPreemptGuard;
53    type ReadGuard = DisabledPreemptGuard;
54
55    #[verifier::external_body]
56    fn guard() -> Self::Guard {
57        disable_preempt()
58    }
59    #[verifier::external_body]
60    fn read_guard() -> Self::Guard {
61        disable_preempt()
62    }
63}
64
65/// A guardian that disables IRQs while holding a lock.
66///
67/// This guardian would incur a certain time overhead over
68/// [`PreemptDisabled`]. So prefer avoiding using this guardian when
69/// IRQ handlers are allowed to get executed while holding the
70/// lock. For example, if a lock is never used in the interrupt
71/// context, then it is ok not to use this guardian in the process context.
72#[verifier::external]
73pub enum LocalIrqDisabled {}
74
75#[verifier::external_type_specification]
76#[verifier::external_body]
77pub struct ExLocalIrqDisabled(LocalIrqDisabled);
78
79#[verus_verify]
80impl SpinGuardian for LocalIrqDisabled {
81    type Guard = DisabledLocalIrqGuard;
82    type ReadGuard = DisabledLocalIrqGuard;
83
84    #[verifier::external_body]
85    fn guard() -> Self::Guard {
86        disable_local()
87    }
88    #[verifier::external_body]
89    fn read_guard() -> Self::Guard {
90        disable_local()
91    }
92}
93
94/// A guardian that disables IRQs while holding a write lock.
95///
96/// This guardian should only be used for a [`RwLock`]. Using it with a [`SpinLock`] will behave in
97/// the same way as using [`LocalIrqDisabled`].
98///
99/// When using this guardian with a [`RwLock`], holding the read lock will only disable preemption,
100/// but holding a write lock will disable local IRQs. The user must ensure that the IRQ handlers
101/// never take the write lock, so we can take the read lock without disabling IRQs, but we are
102/// still free of deadlock even if the IRQ handlers are triggered in the middle.
103///
104/// [`RwLock`]: super::RwLock
105/// [`SpinLock`]: super::SpinLock
106#[verifier::external]
107pub enum WriteIrqDisabled {}
108
109#[verifier::external_type_specification]
110#[verifier::external_body]
111pub struct ExWriteIrqDisabled(WriteIrqDisabled);
112
113#[verus_verify]
114impl SpinGuardian for WriteIrqDisabled {
115    type Guard = DisabledLocalIrqGuard;
116    type ReadGuard = DisabledPreemptGuard;
117
118    #[verifier::external_body]
119    fn guard() -> Self::Guard {
120        disable_local()
121    }
122    #[verifier::external_body]
123    fn read_guard() -> Self::ReadGuard {
124        disable_preempt()
125    }
126}
ostd/sync/guard.rs

ostd/sync/
guard.rs
