planarian_schema/
spec.rs

1//! Per-transition preconditions and predictions (§8 `TransitionSpec`, the
2//! pure half). Shared by the diagnoser, which builds proposals, and the
3//! executor, which checks that a proposal's `expected` refines `predict`
4//! (§12 step 3). Derivation of facts needs the evaluated generation and lives
5//! in `exec`.
6
7use crate::ids::Millis;
8use crate::state::{SystemState, UnitStatus};
9use crate::transition::{Expectation, Settle, Transition};
10use crate::unit::{Attribution, EdgeKind, OverrideDesired, UnitDefs, UnitId, UnitKind};
11use std::collections::{BTreeMap, BTreeSet};
12
13pub const DEFAULT_SETTLE: Millis = Millis::secs(15);
14pub const READY_TIMEOUT: Millis = Millis::secs(60);
15
16/// Units with a `Requires` edge to `unit`, transitively: systemd stops or
17/// restarts them along with it.
18pub fn dependents(unit: &UnitId, defs: &UnitDefs) -> BTreeSet<UnitId> {
19    let mut out = BTreeSet::new();
20    let mut frontier = vec![unit.clone()];
21    while let Some(u) = frontier.pop() {
22        for d in defs.values() {
23            if d.edges.iter().any(|e| e.to == u && e.kind == EdgeKind::Requires) && out.insert(d.id.clone()) {
24                frontier.push(d.id.clone());
25            }
26        }
27    }
28    out
29}
30
31pub fn precondition(t: &Transition, s: &SystemState, defs: &UnitDefs) -> bool {
32    match t {
33        Transition::RestartUnit(u) => {
34            defs.get(u).is_some_and(|d| d.id.kind != UnitKind::Device && !u.name.starts_with("external:"))
35                && !s.overridden(u)
36        }
37        Transition::StopUnit(u) | Transition::StopAndSuppress { unit: u, .. } => defs.contains_key(u),
38        // An inferred override is replaced only by an authorized principal setting a new one (§11).
39        Transition::SetOverride(sup) => s.override_of(&sup.unit).is_none_or(|o| o.attribution == Attribution::Inferred),
40        Transition::LiftOverride(u) => s.overridden(u),
41        Transition::BindDriver { device, .. } => {
42            defs.get(device).is_some_and(|d| d.id.kind == UnitKind::Device) && !s.overridden(device)
43        }
44        Transition::Rollback => s.generation != s.known_good,
45        Transition::SwitchGeneration(g) => *g != s.generation,
46        Transition::Revert { to } => *to != s.generation,
47        _ => true,
48    }
49}
50
51/// What the transition is expected to achieve. For generation operations the
52/// set of units that may change is only known after evaluation; `predict`
53/// leaves `may_change` empty with `others_unchanged = false`, and the executor
54/// bounds it by the derived `affected_units` instead.
55pub fn predict(t: &Transition, s: &SystemState, defs: &UnitDefs) -> Expectation {
56    let unit = |u: &UnitId, status: UnitStatus, settle: Settle| {
57        let mut may: BTreeSet<UnitId> = dependents(u, defs);
58        may.insert(u.clone());
59        Expectation {
60            units: BTreeMap::from([(u.clone(), status)]),
61            generation: None,
62            may_change: may,
63            others_unchanged: true,
64            settle,
65        }
66    };
67    let ready = |u: &UnitId| Settle::Ready { unit: u.clone(), timeout: READY_TIMEOUT };
68    let none = || Expectation {
69        units: BTreeMap::new(),
70        generation: None,
71        may_change: BTreeSet::new(),
72        others_unchanged: true,
73        settle: Settle::Duration(DEFAULT_SETTLE),
74    };
75    match t {
76        Transition::RestartUnit(u) => unit(u, UnitStatus::Running, ready(u)),
77        Transition::StopUnit(u) => unit(u, UnitStatus::Stopped, Settle::Duration(DEFAULT_SETTLE)),
78        Transition::StopAndSuppress { unit: u, .. } => {
79            unit(u, UnitStatus::Overridden(OverrideDesired::Stopped), Settle::Duration(DEFAULT_SETTLE))
80        }
81        Transition::SetOverride(sup) => Expectation {
82            units: BTreeMap::from([(sup.unit.clone(), UnitStatus::Overridden(sup.desired))]),
83            may_change: BTreeSet::from([sup.unit.clone()]),
84            ..none()
85        },
86        Transition::LiftOverride(u) => Expectation { may_change: BTreeSet::from([u.clone()]), ..none() },
87        Transition::BindDriver { device, .. } => unit(device, UnitStatus::Bound, Settle::Duration(DEFAULT_SETTLE)),
88        Transition::SwitchGeneration(g) | Transition::Revert { to: g } => {
89            Expectation { generation: Some(*g), others_unchanged: false, ..none() }
90        }
91        Transition::Rollback => Expectation { generation: Some(s.known_good), others_unchanged: false, ..none() },
92        Transition::ApplyChange { .. } | Transition::LoadModel(_) | Transition::RestoreSnapshot(_) => {
93            Expectation { others_unchanged: false, ..none() }
94        }
95        Transition::CollectGarbage { .. } | Transition::SetRuntimeOption { .. } | Transition::Resolve { .. } => none(),
96    }
97}
98
99/// §12 step 3: `claimed` must agree with `predicted` on every unit the
100/// prediction names, must not broaden `may_change`, and must not relax
101/// `others_unchanged`. For generation operations (`others_unchanged = false`
102/// in the prediction) `bound` limits `may_change` instead.
103pub fn refines(claimed: &Expectation, predicted: &Expectation, bound: Option<&[UnitId]>) -> Result<(), String> {
104    for (u, st) in &predicted.units {
105        if claimed.units.get(u) != Some(st) {
106            return Err(format!("expected status of {u} disagrees with the prediction"));
107        }
108    }
109    if predicted.generation.is_some() && claimed.generation != predicted.generation {
110        return Err("expected generation disagrees with the prediction".into());
111    }
112    if predicted.others_unchanged && !claimed.others_unchanged {
113        return Err("claims others may change where the prediction says they don't".into());
114    }
115    let allowed = |u: &UnitId| match (predicted.others_unchanged, bound) {
116        (true, _) => predicted.may_change.contains(u),
117        (false, Some(b)) => b.contains(u),
118        (false, None) => true,
119    };
120    if let Some(u) = claimed.may_change.iter().find(|u| !allowed(u)) {
121        return Err(format!("may_change broadened with {u}"));
122    }
123    Ok(())
124}
125
126#[cfg(test)]
127mod tests {
128    use super::*;
129    use crate::fixtures::*;
130
131    #[test]
132    fn restart_prediction_includes_dependents_and_refinement() {
133        let db = service("gym-db");
134        let mut app = service("gym-app");
135        edge(&mut app, "gym-db", EdgeKind::Requires);
136        let mut cache_user = service("gym-cache-user");
137        edge(&mut cache_user, "gym-app", EdgeKind::Ordering);
138        let defs = defs([db, app, cache_user]);
139        let s = empty_state(0);
140        let t = Transition::RestartUnit(UnitId::service("gym-db"));
141        let p = predict(&t, &s, &defs);
142        assert_eq!(p.may_change, [UnitId::service("gym-db"), UnitId::service("gym-app")].into());
143        assert!(refines(&p, &p, None).is_ok());
144        let mut broad = p.clone();
145        broad.may_change.insert(UnitId::service("sshd"));
146        assert!(refines(&broad, &p, None).is_err(), "policy-refinement-violation");
147        let mut lax = p.clone();
148        lax.others_unchanged = false;
149        assert!(refines(&lax, &p, None).is_err());
150        let mut narrower = p.clone();
151        narrower.may_change.remove(&UnitId::service("gym-app"));
152        assert!(refines(&narrower, &p, None).is_ok(), "a proposer may only add claims");
153    }
154}
planarian_schema/spec.rs

planarian_schema/
spec.rs
