ostd/timer/
jiffies.rs

1// SPDX-License-Identifier: MPL-2.0
2use vstd::prelude::*;
3use vstd::std_specs::convert::FromSpecImpl;
4
5use core::{
6    sync::atomic::{AtomicU64, Ordering},
7    time::Duration,
8};
9
10use crate::arch::timer::TIMER_FREQ;
11verus! {
12
13pub(crate) exec static ELAPSED: AtomicU64 = AtomicU64::new(0);
14
15} // verus!
16/// Jiffies is a term used to denote the units of time measurement by the kernel.
17///
18/// A jiffy represents one tick of the system timer interrupt,
19/// whose frequency is equal to [`TIMER_FREQ`] Hz.
20#[verus_verify]
21#[derive(Copy, Clone, Debug)]
22pub struct Jiffies(u64);
23
24verus! {
25
26impl View for Jiffies {
27    type V = u64;
28
29    closed spec fn view(&self) -> Self::V {
30        self.0
31    }
32}
33
34impl Jiffies {
35    /// The whole-second component of this jiffy count.
36    pub open spec fn duration_secs(self) -> u64 {
37        self@ / TIMER_FREQ
38    }
39
40    /// The subsecond nanosecond component of this jiffy count.
41    pub open spec fn duration_nanos(self) -> u32 {
42        (((self@ % TIMER_FREQ) * 1_000_000_000u64) / (TIMER_FREQ as int)) as u32
43    }
44}
45
46impl FromSpecImpl<Jiffies> for Duration {
47    open spec fn obeys_from_spec() -> bool {
48        true
49    }
50
51    open spec fn from_spec(value: Jiffies) -> Duration {
52        Duration::new(value.duration_secs(), value.duration_nanos())
53    }
54}
55
56} // verus!
57impl Jiffies {
58    /// The maximum value of [`Jiffies`].
59    pub const MAX: Self = Self(u64::MAX);
60}
61
62#[verus_verify]
63impl Jiffies {
64    /// Creates a new instance.
65    #[verus_spec(ret => ensures ret@ == value)]
66    pub fn new(value: u64) -> Self {
67        Self(value)
68    }
69
70    /// Returns the elapsed time since the system boots up.
71    pub fn elapsed() -> Self {
72        Self::new(ELAPSED.load(Ordering::Relaxed))
73    }
74
75    /// Gets the number of jiffies.
76    #[verus_spec(returns self@)]
77    pub fn as_u64(self) -> u64 {
78        self.0
79    }
80
81    /// Adds the given number of jiffies, saturating at [`Jiffies::MAX`] on overflow.
82    #[verus_spec(
83        ensures
84            final(self)@ == old(self)@.saturating_add(jiffies),
85    )]
86    pub fn add(&mut self, jiffies: u64) {
87        self.0 = self.0.saturating_add(jiffies);
88    }
89
90    /// Gets the [`Duration`] calculated from the jiffies counts.
91    #[verus_spec(returns Duration::new(
92        self.duration_secs(),
93        self.duration_nanos(),
94    ))]
95    pub fn as_duration(self) -> Duration {
96        let secs = self.0 / TIMER_FREQ;
97        let nanos = ((self.0 % TIMER_FREQ) * 1_000_000_000) / TIMER_FREQ;
98        Duration::new(secs, nanos as u32)
99    }
100}
101
102#[verus_verify]
103impl From<Jiffies> for Duration {
104    fn from(value: Jiffies) -> Self {
105        value.as_duration()
106    }
107}
ostd/timer/jiffies.rs

ostd/timer/
jiffies.rs
