Skip to main content

clock_kit/
monotonic.rs

1//! Process-wide monotonic floor — REQ-CLK-001 (G1).
2//!
3//! Every real (non-mock) clock implementation clamps its `mono` through
4//! this floor: a process-wide `AtomicU64` running `fetch_max`, so even a
5//! misbehaving or poorly-synchronized source is clamped to the highest
6//! value ever returned. On targets without 64-bit atomics the floor falls
7//! back to a critical-section cell (the chronoshift `MockClock` pattern;
8//! the `critical-section` impl is provided by the final binary per
9//! critical-section convention).
10//!
11//! The floor is deliberately *not* applied to [`MockClock`](crate::MockClock):
12//! G3 (deterministic fiction) wins there — a mock must not be perturbed by
13//! ambient reads from other tests, and its mono cannot regress by
14//! construction anyway (advancement is additive-only).
15//!
16//! Custom [`Clock`](crate::Clock) implementations should route their mono
17//! through [`mono_floor`] to honor REQ-CLK-001 by construction.
18
19#[cfg(all(not(loom), target_has_atomic = "64"))]
20use core::sync::atomic::{AtomicU64, Ordering};
21#[cfg(loom)]
22use loom::sync::atomic::{AtomicU64, Ordering};
23
24#[cfg(all(not(target_has_atomic = "64"), not(loom)))]
25use core::cell::Cell;
26#[cfg(all(not(target_has_atomic = "64"), not(loom)))]
27use critical_section::Mutex;
28
29#[cfg(not(loom))]
30static MONO_FLOOR: Floor = Floor::new();
31
32/// One floor cell: atomic max on 64-bit-atomic targets, critical-section
33/// cell otherwise. Split out (operating on a fresh cell) so loom can model
34/// the exact production logic per interleaving.
35pub(crate) struct Floor {
36    #[cfg(target_has_atomic = "64")]
37    cell: AtomicU64,
38    #[cfg(not(target_has_atomic = "64"))]
39    cell: Mutex<Cell<u64>>,
40}
41
42impl Floor {
43    // loom's AtomicU64::new is not const — only the real build needs a
44    // const constructor (for the process-wide static).
45    #[cfg(loom)]
46    pub(crate) fn new() -> Self {
47        Self {
48            #[cfg(target_has_atomic = "64")]
49            cell: AtomicU64::new(0),
50            #[cfg(not(target_has_atomic = "64"))]
51            cell: Mutex::new(Cell::new(0)),
52        }
53    }
54
55    #[cfg(not(loom))]
56    pub(crate) const fn new() -> Self {
57        Self {
58            #[cfg(target_has_atomic = "64")]
59            cell: AtomicU64::new(0),
60            #[cfg(not(target_has_atomic = "64"))]
61            cell: Mutex::new(Cell::new(0)),
62        }
63    }
64
65    /// Clamp `x` to at least the highest value this floor has ever handed
66    /// out, and record it. Returned values are globally non-decreasing:
67    /// the cell only ever moves up, and each call returns the cell's value
68    /// at (or raised to) its own moment.
69    pub(crate) fn clamp(&self, x: u64) -> u64 {
70        #[cfg(target_has_atomic = "64")]
71        {
72            let prev = self.cell.fetch_max(x, Ordering::AcqRel);
73            if x > prev {
74                x
75            } else {
76                prev
77            }
78        }
79        #[cfg(not(target_has_atomic = "64"))]
80        {
81            critical_section::with(|cs| {
82                let c = self.cell.borrow(cs);
83                let prev = c.get();
84                let v = if x > prev { x } else { prev };
85                c.set(v);
86                v
87            })
88        }
89    }
90
91    /// Highest value ever handed out (observability; not a clock read).
92    #[cfg(test)]
93    pub(crate) fn peek(&self) -> u64 {
94        #[cfg(target_has_atomic = "64")]
95        {
96            self.cell.load(Ordering::Acquire)
97        }
98        #[cfg(not(target_has_atomic = "64"))]
99        {
100            critical_section::with(|cs| self.cell.borrow(cs).get())
101        }
102    }
103}
104
105/// Clamp a monotonic reading through the **process-wide** floor.
106///
107/// Custom [`Clock`](crate::Clock) implementations call this on their mono
108/// readings so the process-wide guarantee holds for their source too:
109/// the returned value never goes backward across calls within a process,
110/// even when the underlying source regresses. REQ-CLK-001.
111#[must_use]
112pub fn mono_floor(mono: u64) -> u64 {
113    // Under loom only `Floor::clamp` is modeled (fresh cell per
114    // interleaving); the process-wide static is a normal build artifact.
115    #[cfg(loom)]
116    {
117        let _ = mono;
118        0
119    }
120    #[cfg(not(loom))]
121    {
122        MONO_FLOOR.clamp(mono)
123    }
124}
125
126#[cfg(all(test, loom))]
127mod loom_tests {
128    use super::Floor;
129
130    /// Loom model: concurrent clamps through one floor. Tier-A
131    /// concurrency-primitive gate for the lock-free atomic max
132    /// (spec §Gate plan). Every handed-out value must be ≥ the attempted
133    /// value, and the final floor must equal the max of everything seen.
134    #[test]
135    fn loom_floor_fetch_max_never_decreases() {
136        loom::model(|| {
137            let floor = loom::sync::Arc::new(Floor::new());
138            let f1 = loom::sync::Arc::clone(&floor);
139            let f2 = loom::sync::Arc::clone(&floor);
140            let left = loom::sync::Arc::new(loom::sync::atomic::AtomicU64::new(0));
141            let left2 = loom::sync::Arc::clone(&left);
142            let right = loom::sync::Arc::new(loom::sync::atomic::AtomicU64::new(0));
143            let right2 = loom::sync::Arc::clone(&right);
144
145            let t1 = loom::thread::spawn(move || {
146                for x in [7_u64, 3, 9] {
147                    let v = f1.clamp(x);
148                    assert!(v >= x);
149                    left.fetch_max(v, loom::sync::atomic::Ordering::AcqRel);
150                }
151            });
152            let t2 = loom::thread::spawn(move || {
153                for x in [8_u64, 1, 5] {
154                    let v = f2.clamp(x);
155                    assert!(v >= x);
156                    right.fetch_max(v, loom::sync::atomic::Ordering::AcqRel);
157                }
158            });
159
160            // A panicking worker model means a broken invariant.
161            assert!(t1.join().is_ok(), "worker 1 panicked");
162            assert!(t2.join().is_ok(), "worker 2 panicked");
163
164            // Floor holds the max of everything attempted, and each
165            // thread's best handout never exceeded it.
166            assert_eq!(floor.peek(), 9);
167            assert!(left2.load(loom::sync::atomic::Ordering::Acquire) <= 9);
168            assert!(right2.load(loom::sync::atomic::Ordering::Acquire) <= 9);
169        });
170    }
171}
172
173#[cfg(test)]
174mod tests {
175    use super::{mono_floor, Floor};
176
177    /// Single-threaded clamp semantics: regressions are held at the floor,
178    /// advances raise it. (Runs under miri — pure logic.)
179    #[test]
180    fn floor_holds_regressions_single_threaded() {
181        let floor = Floor::new();
182        assert_eq!(floor.clamp(100), 100);
183        assert_eq!(floor.clamp(50), 100); // regression held
184        assert_eq!(floor.clamp(100), 100); // equal passes through
185        assert_eq!(floor.clamp(200), 200); // advance raises
186        assert_eq!(floor.clamp(199), 200); // held again
187        assert_eq!(floor.peek(), 200); // observability agrees
188    }
189
190    /// The process-wide global floor clamps an explicitly regressing
191    /// reading to the highest value ever handed out (REQ-CLK-001's core
192    /// promise, exercised through the public entry point).
193    #[test]
194    fn global_floor_clamps_regressions() {
195        let high = mono_floor(u64::MAX - 3);
196        assert_eq!(high, u64::MAX - 3);
197        assert_eq!(mono_floor(5), u64::MAX - 3, "regression must clamp");
198        assert_eq!(mono_floor(u64::MAX), u64::MAX);
199        assert_eq!(mono_floor(1), u64::MAX);
200    }
201}