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#[cfg(feature = "irc11")]
7use {
8    crate::specs::mm::cpu::CpuId,
9    vstd::resource::Loc,
10    vstd_extra::{
11        atomic_irc11::{ThreadView, ViewSeen},
12        scheduler_thread_view::ScheduledTaskView,
13    },
14};
15
16#[cfg(feature = "irc11")]
17verus! {
18
19/// Linear proof state carried by a task while it is running on one CPU.
20///
21/// The scheduler creates this value by checking out the task's persistent
22/// IRC11 view. Weak-memory operations borrow the contained [`ViewSeen`], and
23/// schedule-out must consume the context to return the updated view to the
24/// same scheduler registry.
25pub tracked struct RunningTaskContext {
26    scheduled_view: ScheduledTaskView<Loc, CpuId>,
27}
28
29impl View for RunningTaskContext {
30    type V = ThreadView;
31
32    closed spec fn view(&self) -> ThreadView {
33        self.scheduled_view@
34    }
35}
36
37impl RunningTaskContext {
38    /// Wraps the view checked out by the scheduler for a running interval.
39    pub proof fn tracked_from_scheduled_view(
40        tracked scheduled_view: ScheduledTaskView<Loc, CpuId>,
41    ) -> (tracked res: Self)
42        ensures
43            res.registry_id() == scheduled_view.registry_id(),
44            res.task() == scheduled_view.task(),
45            res.cpu() == scheduled_view.cpu(),
46            res@ == scheduled_view@,
47    {
48        RunningTaskContext { scheduled_view }
49    }
50
51    /// Scheduler registry that owns the parked form of this task view.
52    pub closed spec fn registry_id(&self) -> Loc {
53        self.scheduled_view.registry_id()
54    }
55
56    /// Task whose subjective view is currently checked out.
57    pub closed spec fn task(&self) -> Loc {
58        self.scheduled_view.task()
59    }
60
61    /// CPU on which this running interval was started.
62    pub closed spec fn cpu(&self) -> CpuId {
63        self.scheduled_view.cpu()
64    }
65
66    /// Borrows the unique native IRC11 view for weak-memory operations.
67    pub proof fn tracked_borrow_irc11_view_mut(tracked &mut self) -> (tracked res: &mut ViewSeen)
68        ensures
69            (*res)@ == old(self)@,
70            final(self).registry_id() == old(self).registry_id(),
71            final(self).task() == old(self).task(),
72            final(self).cpu() == old(self).cpu(),
73            final(self)@ == (*final(res))@,
74    {
75        let tracked thread_view = self.scheduled_view.tracked_borrow_thread_view_mut();
76        thread_view.tracked_borrow_mut()
77    }
78
79    /// Ends the running interval and returns the scheduler's checked-out token.
80    pub proof fn tracked_into_scheduled_view(tracked self) -> (tracked res: ScheduledTaskView<
81        Loc,
82        CpuId,
83    >)
84        ensures
85            res.registry_id() == self.registry_id(),
86            res.task() == self.task(),
87            res.cpu() == self.cpu(),
88            res@ == self@,
89    {
90        self.scheduled_view
91    }
92}
93
94} // verus!
95/// A guard for disable preempt.
96#[verus_verify]
97#[clippy::has_significant_drop]
98#[must_use]
99#[derive(Debug)]
100pub struct DisabledPreemptGuard {
101    // This private field prevents user from constructing values of this type directly.
102    _private: (),
103}
104
105/* impl !Send for DisabledPreemptGuard {}
106
107// SAFETY: The guard disables preemptions, which meets the second
108// sufficient condition for atomic mode.
109unsafe impl InAtomicMode for DisabledPreemptGuard {}
110
111impl DisabledPreemptGuard {
112    fn new() -> Self {
113        super::cpu_local::inc_guard_count();
114        Self { _private: () }
115    }
116}
117*/
118#[verus_verify]
119impl GuardTransfer for DisabledPreemptGuard {
120    #[verifier::external_body]
121    fn transfer_to(&mut self) -> Self {
122        disable_preempt()
123    }
124}
125
126/*
127impl Drop for DisabledPreemptGuard {
128    fn drop(&mut self) {
129        super::cpu_local::dec_guard_count();
130    }
131} */
132
133/// Disables preemption.
134#[verifier::external_body]
135pub fn disable_preempt() -> DisabledPreemptGuard {
136    // DisabledPreemptGuard::new()
137    unimplemented!()
138}
ostd/task/preempt/guard.rs

ostd/task/preempt/
guard.rs
