ostd/timer/
jiffies.rs

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

ostd/timer/
jiffies.rs
