vj_sim/determinism/
policy.rs

1//! DETERMINISM::POLICY (Task 17, ledger DT-001/DT-013) — the v1 conservative
2//! default and the fail-closed DPI speculation gate.
3//!
4//! ARCHITECTURE §2/§4 item 1: "ship v1 with `LOOKAHEAD_CYCLES = 0` globally
5//! ... functionally a conservative deterministic partitioned engine
6//! (bit-reproducible, no rollback)" — optimistic speculation is fully
7//! disabled at first release. This module is the one place that constant and
8//! the DPI fail-closed classification live; nothing here waits on WOCB.
9
10use vj_abi::Region;
11
12use crate::analysis::DpiVpiTag;
13
14/// DT-001: "a global `LOOKAHEAD_CYCLES` config defaults to 0 for every
15/// region." One constant, one place — every region-specific hook
16/// ([`lookahead_cycles_for_region`]) reads through it rather than each
17/// inlining its own `0`, so a later wave can turn per-region optimism on
18/// (ARCHITECTURE §4 item 2) without an API break.
19pub const LOOKAHEAD_CYCLES: u32 = 0;
20
21/// Whether a speculative window may run past a given point without waiting
22/// for a conservative barrier. v1 never produces `Allow` from an unproven or
23/// unclassified DPI call — see [`dpi_speculation_policy`].
24#[derive(Clone, Copy, PartialEq, Eq, Debug)]
25pub enum SpeculationGate {
26    Allow,
27    Barrier,
28}
29
30/// DT-013: DPI purity classification for speculation is fail-closed —
31/// anything not *provably* pure/safe defaults to [`SpeculationGate::Barrier`].
32/// `None` means unclassified (`analyze()` hasn't run, or doesn't exist yet in
33/// this wave) and is treated exactly like a proven-unsafe tag, never like a
34/// proven-safe one. The `match` inside the `Some` arm is exhaustive (no
35/// wildcard): adding a 5th `DpiVpiTag` variant later without updating this
36/// function fails to compile instead of silently defaulting that new variant
37/// to `Allow`.
38pub fn dpi_speculation_policy(tag: Option<DpiVpiTag>) -> SpeculationGate {
39    match tag {
40        None => SpeculationGate::Barrier,
41        Some(t) => match t {
42            DpiVpiTag::Pure => SpeculationGate::Allow,
43            DpiVpiTag::DeferredSafe => SpeculationGate::Allow,
44            DpiVpiTag::Barrier => SpeculationGate::Barrier,
45            DpiVpiTag::SpeculationUnsafe => SpeculationGate::Barrier,
46        },
47    }
48}
49
50/// DT-001's per-region hook: today every region reads the same global
51/// [`LOOKAHEAD_CYCLES`], but the hook's existence (rather than every call
52/// site inlining the constant) is what lets a later wave enable per-region
53/// optimism (ARCHITECTURE §4 item 2) without an API break — ties to SC-130's
54/// review in Task 22.
55pub fn lookahead_cycles_for_region(_region: Region) -> u32 {
56    LOOKAHEAD_CYCLES
57}
58
59#[cfg(test)]
60mod tests {
61    use super::*;
62    use crate::determinism::SequentialController;
63    use crate::sched::SchedTime;
64
65    #[test]
66    fn unclassified_dpi_defaults_to_barrier_never_pure() {
67        assert!(matches!(
68            dpi_speculation_policy(None),
69            SpeculationGate::Barrier
70        ));
71    }
72
73    #[test]
74    fn every_dpi_vpi_tag_variant_maps_correctly_fail_closed() {
75        let cases = [
76            (DpiVpiTag::Pure, SpeculationGate::Allow),
77            (DpiVpiTag::DeferredSafe, SpeculationGate::Allow),
78            (DpiVpiTag::Barrier, SpeculationGate::Barrier),
79            (DpiVpiTag::SpeculationUnsafe, SpeculationGate::Barrier),
80        ];
81        for (tag, expected) in cases {
82            assert_eq!(
83                dpi_speculation_policy(Some(tag)),
84                expected,
85                "DpiVpiTag::{tag:?} must map to {expected:?}"
86            );
87        }
88    }
89
90    #[test]
91    fn lookahead_cycles_is_zero_for_every_region_in_v1() {
92        for r in [
93            Region::Active,
94            Region::Inactive,
95            Region::Nba,
96            Region::Reactive,
97            Region::Postponed,
98        ] {
99            assert_eq!(
100                lookahead_cycles_for_region(r),
101                0,
102                "region {r:?} must have LOOKAHEAD_CYCLES == 0 in v1"
103            );
104        }
105    }
106
107    /// DT-001: "0 lookahead" and "the degenerate sequential controller" are
108    /// the same statement viewed two ways (ARCHITECTURE §4 item 1) — the
109    /// only `DeterminismController` reachable at default config is
110    /// `SequentialController`, whose own `gvt() == now` behavior is
111    /// consistent with a globally-zero lookahead (nothing ever runs ahead
112    /// of `now`, so there is nothing to roll back).
113    #[test]
114    fn the_only_determinism_controller_reachable_at_default_config_is_sequential() {
115        assert_eq!(lookahead_cycles_for_region(Region::Active), 0);
116
117        let controller = SequentialController::default_boxed();
118        let now = SchedTime { ticks: 11 };
119        let out = controller.partition(&[], Region::Active, now);
120        assert!(out.is_empty());
121        assert_eq!(
122            controller.gvt(),
123            now,
124            "the default controller's gvt() must equal now immediately after \
125             partition() — consistent with LOOKAHEAD_CYCLES == 0 (nothing ever \
126             runs ahead of now)"
127        );
128    }
129}
vj_sim/determinism/policy.rs

vj_sim/determinism/
policy.rs
