runtime/backlog/ceiling.rs
1// This Source Code Form is subject to the terms of the Mozilla Public
2// License, v. 2.0. If a copy of the MPL was not distributed with this
3// file, You can obtain one at https://mozilla.org/MPL/2.0/.
4// Copyright (c) 2026 2youg1 and the sprawling contributors
5
6//! What a command's result says about the person's memory ceiling
7//! (`crates/runtime/spec/Tools/Exec.lean` D95): the mark a command gets
8//! as it enters the table, and the verdict read when it is collected.
9//! The platforms only count refusals ([`super::jobs`] on Windows,
10//! [`super::cgroup`] on Linux); which case is reported is decided here
11//! and nowhere else.
12
13use std::num::NonZeroU64;
14
15/// How the person's memory ceiling fared while one command ran.
16///
17/// No variant means "held and not reached": a command whose ceiling held
18/// carries no entry at all, so the model reads nothing it has to discard.
19#[derive(Debug, Clone, Copy, PartialEq, Eq)]
20pub enum Ceiling {
21 /// While the command ran, an allocation of the run's processes was
22 /// refused at the ceiling.
23 Hit {
24 /// The bytes the run's processes may commit together.
25 limit: NonZeroU64,
26 },
27 /// The ceiling was asked for, and the command ran outside it.
28 Unapplied {
29 /// The bytes the person entered.
30 limit: NonZeroU64,
31 /// Why the command ran outside it.
32 why: Unapplied,
33 },
34 /// The ceiling was set, and whether it was reached cannot be read.
35 Unread {
36 /// The bytes the run's processes may commit together.
37 limit: NonZeroU64,
38 },
39}
40
41/// Why a command ran outside the ceiling the person asked for.
42#[derive(Debug, Clone, Copy, PartialEq, Eq)]
43pub enum Unapplied {
44 /// This platform has no per-run memory ceiling (macOS).
45 Platform,
46 /// The Linux cgroup this process sits in is not delegated to it.
47 NotDelegated,
48 /// The job or the cgroup refused the ceiling or the means to read it.
49 Refused,
50 /// The command did not join its run's job or cgroup.
51 Unjoined,
52}
53
54impl Unapplied {
55 /// The spelling a result carries.
56 #[must_use]
57 pub fn as_str(self) -> &'static str {
58 match self {
59 Unapplied::Platform => "platform",
60 Unapplied::NotDelegated => "not_delegated",
61 Unapplied::Refused => "refused",
62 Unapplied::Unjoined => "unjoined",
63 }
64 }
65}
66
67/// What a command was given as it entered the table: the Rust face of
68/// `CeilingMark` in the Lean part.
69#[derive(Debug, Clone, Copy, PartialEq, Eq)]
70pub(super) enum Mark {
71 /// No ceiling was asked for.
72 NotAsked,
73 /// A ceiling was asked for, and this command runs outside it.
74 Unapplied { limit: NonZeroU64, why: Unapplied },
75 /// The ceiling holds, and its refusal count did not read at entry.
76 Unread { limit: NonZeroU64 },
77 /// The ceiling holds, and its run had counted `before` refusals.
78 Watching { limit: NonZeroU64, before: u64 },
79}
80
81impl Mark {
82 /// The mark of a command that entered a ceiling whose refusal count
83 /// read `count` at that moment.
84 pub(super) fn entered(limit: NonZeroU64, count: Option<u64>) -> Mark {
85 match count {
86 Some(before) => Mark::Watching { limit, before },
87 None => Mark::Unread { limit },
88 }
89 }
90
91 /// The mark of a command that asked for `limit`, or nothing, and ran
92 /// outside it for `why`.
93 pub(super) fn outside(limit: Option<NonZeroU64>, why: Unapplied) -> Mark {
94 match limit {
95 Some(limit) => Mark::Unapplied { limit, why },
96 None => Mark::NotAsked,
97 }
98 }
99
100 /// Whether the verdict needs the run's refusal count read again.
101 pub(super) fn watching(self) -> bool {
102 matches!(self, Mark::Watching { .. })
103 }
104}
105
106/// The report for a command collected when its run's refusal count
107/// reads `count` (`ceilingAt` in the Lean part): a hit only when the
108/// count moved past the one at entry, and every asked ceiling that is not
109/// held and unhit says so.
110pub(super) fn verdict(mark: Mark, count: Option<u64>) -> Option<Ceiling> {
111 match mark {
112 Mark::NotAsked => None,
113 Mark::Unapplied { limit, why } => Some(Ceiling::Unapplied { limit, why }),
114 Mark::Unread { limit } => Some(Ceiling::Unread { limit }),
115 Mark::Watching { limit, before } => match count {
116 None => Some(Ceiling::Unread { limit }),
117 Some(after) if before < after => Some(Ceiling::Hit { limit }),
118 Some(_) => None,
119 },
120 }
121}
122
123#[cfg(test)]
124#[allow(clippy::unwrap_used, reason = "test code")]
125mod tests {
126 use super::*;
127 use proptest::prelude::*;
128
129 fn marks() -> impl Strategy<Value = Mark> {
130 let limit = (1_u64..=u64::MAX).prop_map(|bytes| NonZeroU64::new(bytes).unwrap());
131 let why = prop_oneof![
132 Just(Unapplied::Platform),
133 Just(Unapplied::NotDelegated),
134 Just(Unapplied::Refused),
135 Just(Unapplied::Unjoined),
136 ];
137 prop_oneof![
138 Just(Mark::NotAsked),
139 (limit.clone(), why).prop_map(|(limit, why)| Mark::Unapplied { limit, why }),
140 limit.clone().prop_map(|limit| Mark::Unread { limit }),
141 (limit, any::<u64>()).prop_map(|(limit, before)| Mark::Watching { limit, before }),
142 ]
143 }
144
145 proptest! {
146 /// `hit_only_when_the_count_moved`: a hit is reported exactly
147 /// when the ceiling was watched and the count read past its entry.
148 #[test]
149 fn a_hit_is_reported_only_when_the_count_moved(mark in marks(), count in any::<Option<u64>>()) {
150 let hit = matches!(verdict(mark, count), Some(Ceiling::Hit { .. }));
151 let moved = matches!((mark, count), (Mark::Watching { before, .. }, Some(after)) if before < after);
152 prop_assert_eq!(hit, moved);
153 }
154
155 /// `an_asked_ceiling_is_silent_only_when_held_and_unhit`: an asked
156 /// ceiling says nothing only when it was watched, read, and unmoved.
157 #[test]
158 fn an_asked_ceiling_is_silent_only_when_held_and_unhit(mark in marks(), count in any::<Option<u64>>()) {
159 let silent = verdict(mark, count).is_none();
160 let held = matches!((mark, count), (Mark::Watching { before, .. }, Some(after)) if after <= before);
161 prop_assert_eq!(silent, mark == Mark::NotAsked || held);
162 }
163 }
164}