pub struct SpinLock<T, G> { /* private fields */ }Expand description
A spin lock.
§Guard behavior
The type `G’ specifies the guard behavior of the spin lock. While holding the lock,
- if
Gis [PreemptDisabled], preemption is disabled; - if
GisLocalIrqDisabled, local IRQs are disabled.
The G can also be provided by other crates other than ostd,
if it behaves similar like [PreemptDisabled] or LocalIrqDisabled.
The guard behavior can be temporarily upgraded from [PreemptDisabled] to
LocalIrqDisabled using the disable_irq method.
§Verified Properties
§Verification Design
To verify the correctness of spin lock, we use a ghost permission (i.e., not present in executable Rust), and only the owner of the permission can access the protected data in the cell.
When lock or try_lock succeeds, the ghost permission is transferred to the lock guard and given to the user for accessing the protected data.
When the lock guard is dropped, the ghost permission is transferred back to the spin lock.
For curious readers, details of the permission can be found in vstd::cell::pcell::PointsTo.
§Invariant
When the internal AtomicBool is true, the permission has been transferred to some lock guard and nobody else can acquire the lock; when it is false,
the permission is held by the spin lock and can be acquired by a user.
§Safety
There are no data races.
§Functional Correctness
- At most one user can hold the lock at the same time.
Implementations§
Source§impl<T, G: SpinGuardian> SpinLock<T, G>
impl<T, G: SpinGuardian> SpinLock<T, G>
Sourcepub exec fn lock(&self) -> SpinLockGuard<'_, T, G>
pub exec fn lock(&self) -> SpinLockGuard<'_, T, G>
Acquires the spin lock.
Sourcepub exec fn lock_arc(self: &Arc<Self>) -> ArcSpinLockGuard<T, G>
pub exec fn lock_arc(self: &Arc<Self>) -> ArcSpinLockGuard<T, G>
Sourcepub exec fn try_lock(&self) -> Option<SpinLockGuard<'_, T, G>>
pub exec fn try_lock(&self) -> Option<SpinLockGuard<'_, T, G>>
Tries acquiring the spin lock immedidately.
Sourcepub exec fn spec_with_example(&self) -> ret : u32
pub exec fn spec_with_example(&self) -> ret : u32
ghost_in1: Tracked <int>,
ghost_in2: Tracked <int>,
->
ghost_out: Ghost <(int,int)>,ghost_in1@ >= 0,ghost_out@.0 == ghost_in1@,ret == 0,An example to show the doc generation with #[verus_spec] ghost parameters.
It will be removed after the doc generation function is merged.