logicaffeine_compile/spatial/clock.rs
1//! ════════════════════════════════════════════════════════════════════════════════════════════════
2//! THE SPATIAL CLOCK — a period computed from the graph, not fitted to a counter.
3//!
4//! A spatial program has no meaningful global clock. Sixty-four sites run concurrently, each engine
5//! advances when its inputs are present, and "how long does it take" is not a property any one of them
6//! holds. Asking a simulator for a cycle count answers a different question — ttsim's counter advances
7//! once per simulated clock while it steps the RV32 cores, so a 4x deeper reduction moves it by one
8//! cycle (`benchmarks/silicon/ttsim_instrument_audit.json`).
9//!
10//! But the choreography is not an arbitrary concurrent program. [`certificate`](super::certificate)
11//! already proves it is a **Petri MARKED GRAPH** — every place has exactly one producer and one
12//! consumer — and certifies its liveness by Commoner's theorem. Marked graphs have a classical and
13//! exact steady-state result: the system settles into a period equal to the **maximum cycle mean**
14//!
15//! ```text
16//! Π = max over directed cycles C of ( Σ delay(t) for t ∈ C ) / ( Σ tokens(p) for p ∈ C )
17//! ```
18//!
19//! That is the spatial clock. It is a THEOREM about the graph the compiler already builds and already
20//! proves live, evaluated at per-transition delays that are architectural facts — a DRAM tile's
21//! bandwidth occupancy, an engine's issue rate — rather than regression coefficients. Nothing here is
22//! fitted, so nothing here can be corrupted by a counter that cannot see work.
23//!
24//! It also EXPLAINS itself: the cycle that attains the maximum is the critical cycle, and it names the
25//! exact chain of events that sets the period. "Bound on DRAM bandwidth" is a summary; the critical
26//! cycle is the evidence.
27//! ════════════════════════════════════════════════════════════════════════════════════════════════
28
29use super::certificate::{MarkedGraph, Transition};
30
31/// The steady-state period of a marked graph, with the cycle that attains it.
32#[derive(Clone, Debug, PartialEq)]
33pub struct Period {
34 /// Cycles per steady-state iteration — the spatial clock.
35 pub period: f64,
36 /// The transitions of a cycle attaining the maximum, in order. Empty when the graph is acyclic,
37 /// which means the program has no steady state to speak of: it runs once and drains.
38 pub critical_cycle: Vec<usize>,
39 /// Whether any directed cycle exists at all.
40 pub cyclic: bool,
41 /// False when some directed cycle carries NO token. Such a cycle can never fire — it is a deadlock,
42 /// and it is exactly what Commoner's condition forbids — so the period is infinite rather than
43 /// large. Reporting a big finite number there would hand a caller a schedule that cannot run.
44 pub live: bool,
45}
46
47/// One edge of the transition graph: place `p` runs producer → consumer, carrying `tokens` initially.
48struct Edge {
49 from: usize,
50 to: usize,
51 delay: f64,
52 tokens: f64,
53}
54
55fn edges(g: &MarkedGraph) -> Vec<Edge> {
56 let mut producer = vec![usize::MAX; g.places.len()];
57 for (ti, t) in g.transitions.iter().enumerate() {
58 for &p in &t.produces {
59 producer[p] = ti;
60 }
61 }
62 let mut out = Vec::new();
63 for (ti, t) in g.transitions.iter().enumerate() {
64 for &p in &t.consumes {
65 let from = producer[p];
66 if from == usize::MAX {
67 continue; // a source place: nobody produces it, so it closes no cycle
68 }
69 out.push(Edge {
70 from,
71 to: ti,
72 delay: 0.0,
73 tokens: g.places[p].marking as f64,
74 });
75 }
76 }
77 out
78}
79
80/// **The spatial clock.** The maximum cycle mean of `g` under `delay`, by parametric search: for a
81/// candidate period λ, give each edge the weight `delay(producer) − λ·tokens`. A positive-weight cycle
82/// exists exactly when some cycle's mean exceeds λ, so Bellman-Ford's longest-path relaxation decides
83/// the comparison and bisection converges on Π.
84///
85/// Deterministic: the same graph and the same delays give the same period, bit for bit.
86pub fn cycle_period(g: &MarkedGraph, delay: impl Fn(&Transition) -> f64) -> Period {
87 let n = g.transitions.len();
88 let mut e = edges(g);
89 for edge in e.iter_mut() {
90 edge.delay = delay(&g.transitions[edge.from]);
91 }
92 // A cycle needs at least one edge whose head reaches its own tail; bisect only if one exists.
93 let hi_seed = e.iter().map(|x| x.delay).fold(0.0f64, f64::max).max(1.0) * n.max(1) as f64;
94 if n == 0 || e.is_empty() || positive_cycle(n, &e, hi_seed * 2.0).is_none() {
95 // No cycle attains even an absurd mean ⇒ acyclic.
96 if n == 0 || e.is_empty() || !has_cycle(n, &e) {
97 return Period {
98 period: 0.0,
99 critical_cycle: Vec::new(),
100 cyclic: false,
101 live: true,
102 };
103 }
104 }
105 // A token-free cycle never fires. Detect it before bisecting, because parametric search cannot
106 // distinguish "infinite mean" from "very large mean" and would return a plausible finite lie.
107 let starved: Vec<&Edge> = e.iter().filter(|x| x.tokens == 0.0).collect();
108 let mut sn = vec![0usize; n];
109 let mut sadj = vec![Vec::new(); n];
110 for x in &starved {
111 sadj[x.from].push(x.to);
112 sn[x.to] += 1;
113 }
114 {
115 let mut q: Vec<usize> = (0..n).filter(|&i| sn[i] == 0).collect();
116 let mut seen = 0usize;
117 while let Some(v) = q.pop() {
118 seen += 1;
119 for &w in &sadj[v] {
120 sn[w] -= 1;
121 if sn[w] == 0 {
122 q.push(w);
123 }
124 }
125 }
126 if seen != n {
127 return Period {
128 period: f64::INFINITY,
129 critical_cycle: Vec::new(),
130 cyclic: true,
131 live: false,
132 };
133 }
134 }
135 let (mut lo, mut hi) = (0.0f64, hi_seed.max(1.0));
136 while positive_cycle(n, &e, hi).is_some() {
137 hi *= 2.0;
138 if hi > 1e18 {
139 break;
140 }
141 }
142 for _ in 0..200 {
143 let mid = 0.5 * (lo + hi);
144 if positive_cycle(n, &e, mid).is_some() {
145 lo = mid;
146 } else {
147 hi = mid;
148 }
149 }
150 let period = 0.5 * (lo + hi);
151 // Report the cycle attaining it: at a period just under Π one still exists.
152 let critical_cycle = positive_cycle(n, &e, period * (1.0 - 1e-9) - 1e-12).unwrap_or_default();
153 Period {
154 period,
155 critical_cycle,
156 cyclic: true,
157 live: true,
158 }
159}
160
161/// Any directed cycle at all, ignoring weights.
162fn has_cycle(n: usize, e: &[Edge]) -> bool {
163 let mut indeg = vec![0usize; n];
164 let mut adj = vec![Vec::new(); n];
165 for x in e {
166 adj[x.from].push(x.to);
167 indeg[x.to] += 1;
168 }
169 let mut q: Vec<usize> = (0..n).filter(|&i| indeg[i] == 0).collect();
170 let mut seen = 0usize;
171 while let Some(v) = q.pop() {
172 seen += 1;
173 for &w in &adj[v] {
174 indeg[w] -= 1;
175 if indeg[w] == 0 {
176 q.push(w);
177 }
178 }
179 }
180 seen != n
181}
182
183/// A cycle of strictly positive weight under `w(edge) = delay − λ·tokens`, as a transition list.
184fn positive_cycle(n: usize, e: &[Edge], lambda: f64) -> Option<Vec<usize>> {
185 // Longest path relaxation from every node at once; a node still improving after n rounds lies on
186 // (or downstream of) a positive cycle.
187 let mut dist = vec![0.0f64; n];
188 let mut pred = vec![usize::MAX; n];
189 let mut last = usize::MAX;
190 for round in 0..=n {
191 last = usize::MAX;
192 for x in e {
193 let cand = dist[x.from] + x.delay - lambda * x.tokens;
194 if cand > dist[x.to] + 1e-12 {
195 dist[x.to] = cand;
196 pred[x.to] = x.from;
197 last = x.to;
198 }
199 }
200 if last == usize::MAX {
201 return None;
202 }
203 let _ = round;
204 }
205 // Walk predecessors n times to land inside the cycle, then read it off.
206 let mut v = last;
207 for _ in 0..n {
208 v = pred[v];
209 if v == usize::MAX {
210 return None;
211 }
212 }
213 let start = v;
214 let mut cyc = vec![start];
215 let mut u = pred[start];
216 while u != start {
217 if u == usize::MAX || cyc.len() > n {
218 return None;
219 }
220 cyc.push(u);
221 u = pred[u];
222 }
223 cyc.reverse();
224 Some(cyc)
225}