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    fn guard() -> Self::Guard {
56        disable_preempt()
57    }
58    fn read_guard() -> Self::Guard {
59        disable_preempt()
60    }
61}
62
63/// A guardian that disables IRQs while holding a lock.
64///
65/// This guardian would incur a certain time overhead over
66/// [`PreemptDisabled`]. So prefer avoiding using this guardian when
67/// IRQ handlers are allowed to get executed while holding the
68/// lock. For example, if a lock is never used in the interrupt
69/// context, then it is ok not to use this guardian in the process context.
70#[verifier::external]
71pub enum LocalIrqDisabled {}
72
73#[verifier::external_type_specification]
74#[verifier::external_body]
75pub struct ExLocalIrqDisabled(LocalIrqDisabled);
76
77#[verus_verify]
78impl SpinGuardian for LocalIrqDisabled {
79    type Guard = DisabledLocalIrqGuard;
80    type ReadGuard = DisabledLocalIrqGuard;
81
82    fn guard() -> Self::Guard {
83        disable_local()
84    }
85
86    fn read_guard() -> Self::Guard {
87        disable_local()
88    }
89}
90
91/// A guardian that disables IRQs while holding a write lock.
92///
93/// This guardian should only be used for a [`RwLock`]. Using it with a [`SpinLock`] will behave in
94/// the same way as using [`LocalIrqDisabled`].
95///
96/// When using this guardian with a [`RwLock`], holding the read lock will only disable preemption,
97/// but holding a write lock will disable local IRQs. The user must ensure that the IRQ handlers
98/// never take the write lock, so we can take the read lock without disabling IRQs, but we are
99/// still free of deadlock even if the IRQ handlers are triggered in the middle.
100///
101/// [`RwLock`]: super::RwLock
102/// [`SpinLock`]: super::SpinLock
103#[verifier::external]
104pub enum WriteIrqDisabled {}
105
106#[verifier::external_type_specification]
107#[verifier::external_body]
108pub struct ExWriteIrqDisabled(WriteIrqDisabled);
109
110#[verus_verify]
111impl SpinGuardian for WriteIrqDisabled {
112    type Guard = DisabledLocalIrqGuard;
113    type ReadGuard = DisabledPreemptGuard;
114
115    fn guard() -> Self::Guard {
116        disable_local()
117    }
118
119    fn read_guard() -> Self::ReadGuard {
120        disable_preempt()
121    }
122}
ostd/sync/guard.rs

ostd/sync/
guard.rs
