ostd/task/preempt/
guard.rs

1// SPDX-License-Identifier: MPL-2.0
2use vstd::prelude::*;
3
4use crate::{sync::GuardTransfer /*, task::atomic_mode::InAtomicMode*/};
5
6/// A guard for disable preempt.
7#[verus_verify]
8#[clippy::has_significant_drop]
9#[must_use]
10#[derive(Debug)]
11pub struct DisabledPreemptGuard {
12    // This private field prevents user from constructing values of this type directly.
13    _private: (),
14}
15
16/* impl !Send for DisabledPreemptGuard {}
17
18// SAFETY: The guard disables preemptions, which meets the second
19// sufficient condition for atomic mode.
20unsafe impl InAtomicMode for DisabledPreemptGuard {}
21
22impl DisabledPreemptGuard {
23    fn new() -> Self {
24        super::cpu_local::inc_guard_count();
25        Self { _private: () }
26    }
27}
28*/
29#[verus_verify]
30impl GuardTransfer for DisabledPreemptGuard {
31    #[verifier::external_body]
32    fn transfer_to(&mut self) -> Self {
33        disable_preempt()
34    }
35}
36
37/*
38impl Drop for DisabledPreemptGuard {
39    fn drop(&mut self) {
40        super::cpu_local::dec_guard_count();
41    }
42} */
43
44/// Disables preemption.
45#[verifier::external_body]
46pub fn disable_preempt() -> DisabledPreemptGuard {
47    // DisabledPreemptGuard::new()
48    unimplemented!()
49}
ostd/task/preempt/guard.rs

ostd/task/preempt/
guard.rs
