nx_ts_drain_gate.nx source
↩ module page · 395 lines · 18005 B
1// nx_ts_drain_gate.nx -- TS2: THE PROCESS MUST KEEP SERVING AFTER TERM.
2//
3// /compare/trafficsafety rung TS2, accept rule taken VERBATIM from trafficsafety.plan and not
4// re-invented here: "with a request in flight at the moment TERM lands, the client receives a
5// complete response and not a 5xx or a reset, and a daemon that exits early FAILS the gate.
6// Anti-vacuity tooth required -- a run in which no request was in flight when TERM landed must be
7// reported as UNOBSERVED and must not score as a pass."
8//
9// THE MEASUREMENT IS WHAT THE CLIENT RECEIVED, NOT WHAT THE SERVER LOGGED. A drain that logs
10// "draining" and still cuts the response is the defect, so nothing here reads the subject's output:
11// a real client drives a real TCP connection and the verdict is whether the completion byte arrived.
12//
13// THE IN-FLIGHT WINDOW IS CONSTRUCTED, NOT HOPED FOR, and that is what makes this a gate rather than
14// a race. The subject answers a request in TWO parts: it writes ACK (the response has begun and is
15// therefore incomplete), then BLOCKS reading GO before writing DONE. The parent sends TERM and only
16// THEN sends GO. So at the instant TERM lands the subject is provably mid-request, every time:
17// - drain armed -> TERM is blocked, the blocking read is NOT interrupted, GO arrives, DONE is
18// written. The client gets a complete response AFTER TERM.
19// - neg-control -> TERM is delivered to a process blocked in read, default action TERMINATE, so
20// the subject dies BEFORE GO is ever written and the client gets nothing.
21// The ordering (TERM strictly before GO) is what removes the race; a sleep would have re-introduced
22// it and would have been a magic number besides.
23//
24// TEST THE STATE, NOT THE MESSAGE. The neg-control's tooth asserts the subject died BY SIGNAL 15 --
25// read out of the wait status, not out of any text -- because "the client got nothing" has several
26// possible causes and only one of them is the one this rung is about.
27//
28// IT ALSO VERIFIES THE SYSCALL NUMBER EMPIRICALLY. A subject that survives TERM can only have
29// blocked it, so T04 is a live check that raw x86-64 14 (rt_sigprocmask) really passes through
30// x86ctx_rv64_to_x86_64_syscall unchanged. Reasoning about that table is not the same as running it.
31//
32// SAFETY: loopback only; every port is FOUND by a bind that would have failed had it been occupied,
33// because a probe port you did not verify free is not a control, it is a second instance. The
34// listening socket is created by the PARENT and inherited across fork, so a child is never racing to
35// bind and the client can connect the instant the subject exists. No serving daemon is touched.
36// expect_exit: 0 license_tier: ORIGINAL No hw writes (Rule 26).
37import "nx_syscalls.nx"
38import "nx_ts_drain_lib.nx"
39import "nx_gate_emit_lib.nx"
40import "nx_gate_verdict.nx"
41
42const TD_NUM_SCRATCH: i64 = 24
43const TD_ASCII_ZERO: i64 = 48
44const TD_B10: i64 = 10
45const TD_ONE: i64 = 1
46const TD_SA_BYTES: i64 = 16
47// sockaddr_in FIELD OFFSETS, named so a reader checks them against the platform layout instead of
48// meeting bare indices: sin_family at 0, sin_port at 2 (big-endian), sin_addr at 4.
49const TD_SA_PORT_OFF: i64 = 2
50const TD_SA_ADDR_OFF: i64 = 4
51const TD_ADDR_BYTES: i64 = 4
52const TD_BYTE_RADIX: i64 = 256
53const TD_OUT_SLOTS: i64 = 8
54const TD_OUT_BYTES: i64 = 64
55const TD_LOOPBACK_A: i64 = 127
56const TD_LOOPBACK_D: i64 = 1
57const TD_PORT_BASE: i64 = 39300
58const TD_PORT_TRIES: i64 = 64
59const TD_PORT_NONE: i64 = 0 - 1
60const TD_BACKLOG: i64 = 8
61const TD_TRUE: i64 = 1
62const TD_FALSE: i64 = 0
63
64// Protocol bytes. Distinct values so a mis-sequenced exchange cannot be mistaken for a good one.
65const TD_PING: i64 = 80
66const TD_ACK: i64 = 65
67const TD_GO: i64 = 71
68const TD_DONE: i64 = 68
69const TD_READY: i64 = 82
70
71// Bounds exist only so a broken run fails LOUD instead of hanging. Reusing the shim's established
72// socket deadline rather than inventing a second budget for the same kind of wait.
73const TD_DEADLINE_S: i64 = ACCEPT_TMO_S
74
75// Subject exit codes -- each NAMES which step failed, so a red says where rather than merely that.
76const TD_C_OK: i64 = 0
77const TD_C_ARM: i64 = 2
78const TD_C_ACCEPT: i64 = 3
79const TD_C_BADREQ: i64 = 4
80const TD_C_WRITE: i64 = 5
81const TD_C_NODRAIN: i64 = 6
82const TD_C_IDLE_DRAIN: i64 = 7
83
84const TD_SIG_TERM: i64 = 15
85const TD_SIG_NONE: i64 = 0
86
87// Parent-side out slots.
88const TD_O_ACK: i64 = 0
89const TD_O_DONE: i64 = 1
90const TD_O_EXIT: i64 = 2
91const TD_O_TSIG: i64 = 3
92const TD_O_INFLIGHT: i64 = 4
93const TD_O_POST: i64 = 5
94
95const TD_DIR: *u8 = "/tmp/nx_ts_drain_gate" as *u8
96
97func g_putn(v: i64) -> i64 {
98 if v == 0 { sys_write(1, "0" as *u8, 1); return 0 }
99 var m: i64 = v
100 if m < 0 { sys_write(1, "-" as *u8, 1); m = 0 - m }
101 let d: *u8 = sys_mmap(TD_NUM_SCRATCH); var k: i64 = 0
102 while m > 0 { d[k] = ((TD_ASCII_ZERO + (m - (m / TD_B10) * TD_B10)) as u8); m = m / TD_B10; k = k + 1 }
103 var j: i64 = k - 1
104 while j >= 0 { sys_write(1, ((d as i64)+j) as *u8, 1); j = j - 1 }
105 return 0
106}
107
108func gq(label: *u8, got: i64, want: i64, ctr: *i64) -> i64 {
109 var c: i64 = 0
110 if got == want { c = 1 }
111 let r: i64 = gv_check(label, c, ctr)
112 if c == 0 {
113 g_puts(" got=" as *u8); g_putn(got)
114 g_puts(" want=" as *u8); g_putn(want)
115 g_puts("\n" as *u8)
116 }
117 return r
118}
119
120func td_sa(sa: *u8, port: i64) -> i64 {
121 var i: i64 = 0
122 while i < TD_SA_BYTES { sa[i] = 0; i = i + 1 }
123 // The zero-fill above already cleared every other octet, so only the non-zero lanes are written.
124 sa[0] = AF_INET
125 sa[TD_SA_PORT_OFF] = port / TD_BYTE_RADIX
126 sa[TD_SA_PORT_OFF + 1] = port % TD_BYTE_RADIX
127 sa[TD_SA_ADDR_OFF] = TD_LOOPBACK_A
128 sa[TD_SA_ADDR_OFF + TD_ADDR_BYTES - 1] = TD_LOOPBACK_D
129 return 0
130}
131
132func td_put1(fd: i64, v: i64) -> i64 {
133 let b: *u8 = sys_mmap(TD_ONE)
134 b[0] = v
135 return sys_write(fd, b, TD_ONE)
136}
137func td_get1(fd: i64) -> i64 {
138 let b: *u8 = sys_mmap(TD_ONE)
139 b[0] = 0
140 let r: i64 = sys_read(fd, b, TD_ONE)
141 if r != TD_ONE { return 0 - 1 }
142 return b[0] as i64
143}
144
145// reuse=1 sets SO_REUSEADDR. With reuse=0 the bind ITSELF is the free-port check, which is why the
146// port search below never sets it.
147func td_listen(port: i64, reuse: i64) -> i64 {
148 let fd: i64 = sys_socket(AF_INET, SOCK_STREAM, 0)
149 if fd < 0 { return fd }
150 if reuse == TD_TRUE {
151 let ra: *u8 = sys_mmap(SCM_U32_BYTES)
152 var z: i64 = 0
153 while z < SCM_U32_BYTES { ra[z] = 0 as u8; z = z + 1 }
154 ra[0] = 1
155 sys_setsockopt(fd, SOL_SOCKET, SO_REUSEADDR, ra, SCM_U32_BYTES)
156 }
157 let sa: *u8 = sys_mmap(TD_SA_BYTES)
158 td_sa(sa, port)
159 if sys_bind(fd, sa, TD_SA_BYTES) < 0 { sys_close(fd); return 0 - 1 }
160 if sys_listen(fd, TD_BACKLOG) < 0 { sys_close(fd); return 0 - 1 }
161 return fd
162}
163
164func td_find_port(from: i64) -> i64 {
165 var t: i64 = 0
166 while t < TD_PORT_TRIES {
167 let cand: i64 = from + t
168 let fd: i64 = td_listen(cand, TD_FALSE)
169 if fd >= 0 { sys_close(fd); return cand }
170 t = t + 1
171 }
172 return TD_PORT_NONE
173}
174
175func td_connect(port: i64) -> i64 {
176 let sa: *u8 = sys_mmap(TD_SA_BYTES)
177 td_sa(sa, port)
178 let fd: i64 = sys_socket(AF_INET, SOCK_STREAM, 0)
179 if fd < 0 { return 0 - 1 }
180 sys_set_socket_timeout(fd, TD_DEADLINE_S)
181 if sys_connect(fd, sa, TD_SA_BYTES) < 0 { sys_close(fd); return 0 - 1 }
182 return fd
183}
184
185// ---- THE SUBJECT -------------------------------------------------
186//
187// A minimal serving daemon in exactly the shape nx_survey_daemon now has: arm the drain BEFORE the
188// listener is usable, serve, then wait on the drain and the listener together. armed=0 is the CURRENT
189// estate-wide path -- no drain at all, TERM keeps its default disposition -- and it is the control.
190func td_subject_inflight(armed: i64, lfd: i64) -> i64 {
191 sys_alarm(TD_DEADLINE_S)
192 var dfd: i64 = 0 - 1
193 if armed == TD_TRUE {
194 let v: *i64 = (sys_mmap(TD_OUT_BYTES)) as *i64
195 v[0] = 0
196 dfd = ts_drain_on_term(v)
197 if dfd < 0 { return TD_C_ARM }
198 }
199 let acc: i64 = sys_accept(lfd)
200 if acc < 0 { return TD_C_ACCEPT }
201 sys_set_socket_timeout(acc, TD_DEADLINE_S)
202 if td_get1(acc) != TD_PING { sys_close(acc); return TD_C_BADREQ }
203 // THE RESPONSE HAS BEGUN AND IS INCOMPLETE. From here until DONE, this request is in flight.
204 if td_put1(acc, TD_ACK) != TD_ONE { sys_close(acc); return TD_C_WRITE }
205 // Block until the parent confirms it has ALREADY sent TERM. An unblocked TERM kills us HERE,
206 // which is precisely the neg-control's expected outcome.
207 if td_get1(acc) != TD_GO { sys_close(acc); return TD_C_BADREQ }
208 // COMPLETE THE RESPONSE AFTER TERM. This write is the whole accept rule.
209 if td_put1(acc, TD_DONE) != TD_ONE { sys_close(acc); return TD_C_WRITE }
210 sys_close(acc)
211 if armed == TD_TRUE {
212 // Behave like the drained loop: the next wait must report DRAIN and stop accepting.
213 let w: i64 = ts_drain_wait(lfd, dfd, TSD_WAIT_BLOCK)
214 if w != TSD_W_DRAIN { return TD_C_NODRAIN }
215 }
216 return TD_C_OK
217}
218
219// The IDLE subject: nothing in flight. It signals readiness over the listener, then blocks. If the
220// drain were poll-driven only by a timeout it would sleep out its budget and SIGALRM would kill it --
221// so a clean TD_C_IDLE_DRAIN exit is positive evidence that the wakeup was EVENT-driven.
222func td_subject_idle(lfd: i64) -> i64 {
223 sys_alarm(TD_DEADLINE_S)
224 let v: *i64 = (sys_mmap(TD_OUT_BYTES)) as *i64
225 v[0] = 0
226 let dfd: i64 = ts_drain_on_term(v)
227 if dfd < 0 { return TD_C_ARM }
228 let acc: i64 = sys_accept(lfd)
229 if acc < 0 { return TD_C_ACCEPT }
230 if td_put1(acc, TD_READY) != TD_ONE { sys_close(acc); return TD_C_WRITE }
231 sys_close(acc)
232 // IDLE from here: the request has fully returned and nothing is in flight.
233 let w: i64 = ts_drain_wait(lfd, dfd, TSD_WAIT_BLOCK)
234 if w != TSD_W_DRAIN { return TD_C_NODRAIN }
235 return TD_C_IDLE_DRAIN
236}
237
238// ---- THE EXPERIMENT ----------------------------------------------
239//
240// Identical script for both arms; the ONLY difference is whether the subject armed the drain.
241// Returns 1 when the harness reached the in-flight condition, 0 when it did not (UNOBSERVED).
242func td_run_inflight(armed: i64, lfd: i64, port: i64, out: *i64) -> i64 {
243 var k: i64 = 0
244 while k < TD_OUT_SLOTS { out[k] = 0; k = k + 1 }
245 let pid: i64 = sys_fork()
246 if pid == 0 { sys_exit(td_subject_inflight(armed, lfd)) }
247 let c: i64 = td_connect(port)
248 if c < 0 { return 0 }
249 if td_put1(c, TD_PING) != TD_ONE { sys_close(c); return 0 }
250 let a: i64 = td_get1(c)
251 if a == TD_ACK { out[TD_O_ACK] = 1 }
252 if out[TD_O_ACK] == 0 { sys_close(c); return 0 }
253 // THE IN-FLIGHT CONDITION IS NOW ESTABLISHED: the response has begun and has not completed.
254 out[TD_O_INFLIGHT] = 1
255 nx_kill(pid, TD_SIG_TERM)
256 // TERM strictly before GO -- that ordering is what makes both arms deterministic.
257 td_put1(c, TD_GO)
258 let d: i64 = td_get1(c)
259 if d == TD_DONE { out[TD_O_DONE] = 1 }
260 sys_close(c)
261 let st: *i64 = (sys_mmap(TD_OUT_BYTES)) as *i64
262 st[0] = 0
263 sys_wait4(pid, st, 0)
264 out[TD_O_EXIT] = wait_status_rc(st[0])
265 out[TD_O_TSIG] = wait_term_signal(st[0])
266 return 1
267}
268
269func td_report(tag: *u8, out: *i64) -> i64 {
270 g_puts(" " as *u8); g_puts(tag)
271 g_puts(" inflight_at_term=" as *u8); g_putn(out[TD_O_INFLIGHT])
272 g_puts(" ack=" as *u8); g_putn(out[TD_O_ACK])
273 g_puts(" complete_response=" as *u8); g_putn(out[TD_O_DONE])
274 g_puts(" subject_exit=" as *u8); g_putn(out[TD_O_EXIT])
275 g_puts(" killed_by_signal=" as *u8); g_putn(out[TD_O_TSIG])
276 g_puts("\n" as *u8)
277 return 0
278}
279
280func main() -> i64 {
281 let ctr: *i64 = gv_ctr()
282 gv_head("nx_ts_drain_gate -- TS2: keep serving after TERM until a derived deadline" as *u8)
283 sys_mkdir(TD_DIR, MODE_0755)
284
285 // ---- THE DEADLINE IS DERIVED, NOT TYPED.
286 let src: *i64 = (sys_mmap(TD_OUT_BYTES)) as *i64
287 src[0] = 0 - 1
288 let dl: i64 = ts_drain_deadline_s(src)
289 g_puts(" deadline_s=" as *u8); g_putn(dl)
290 g_puts(" src=" as *u8); g_putn(src[0])
291 g_puts(" ACCEPT_TMO_S=" as *u8); g_putn(ACCEPT_TMO_S)
292 g_puts(" (src 0=DERIVED 1=CONF)\n" as *u8)
293 gq("T01 the drain deadline is DERIVED from ACCEPT_TMO_S, never a literal" as *u8, dl, ACCEPT_TMO_S, ctr)
294 gq("T02 and it reports that provenance rather than leaving it implicit" as *u8, src[0], TSD_SRC_DERIVED, ctr)
295
296 let pa: i64 = td_find_port(TD_PORT_BASE)
297 var pn: i64 = TD_PORT_NONE
298 if pa != TD_PORT_NONE { pn = td_find_port(pa + 1) }
299 var pi: i64 = TD_PORT_NONE
300 if pn != TD_PORT_NONE { pi = td_find_port(pn + 1) }
301 var ports_ok: i64 = 0
302 if pa != TD_PORT_NONE { if pn != TD_PORT_NONE { if pi != TD_PORT_NONE { ports_ok = 1 } } }
303 if gv_need("three DISTINCT loopback ports proven free by a bind without SO_REUSEADDR" as *u8, ports_ok, ctr) == 0 {
304 let rcs: i64 = gv_verdict("TS-DRAIN-GATE" as *u8, ctr, "each tooth states its own strength above" as *u8)
305 sys_exit(rcs)
306 return rcs
307 }
308
309 // ---- ARM 1: THE DRAIN. The listener is created by the parent and inherited across fork, so the
310 // subject never races to bind and the client can connect the instant it exists.
311 let la: i64 = td_listen(pa, TD_TRUE)
312 let oa: *i64 = (sys_mmap(TD_OUT_BYTES)) as *i64
313 var ran_a: i64 = 0
314 if la >= 0 { ran_a = td_run_inflight(TD_TRUE, la, pa, oa) }
315 td_report("ARMED " as *u8, oa)
316 // ANTI-VACUITY FIRST. A run in which no request was in flight when TERM landed is UNOBSERVED and
317 // must not score as a pass -- that is the specific defect this rung's gate exists to make impossible.
318 var obs_a: i64 = 0
319 if ran_a == 1 { if oa[TD_O_INFLIGHT] == 1 { obs_a = 1 } }
320 if gv_need("anti-vacuity a request was PROVABLY in flight when TERM landed (ARMED)" as *u8, obs_a, ctr) == 1 {
321 gq("T03 THE ACCEPT RULE the client received a COMPLETE response after TERM" as *u8,
322 oa[TD_O_DONE], 1, ctr)
323 gq("T04 the daemon was NOT killed by TERM -- it blocked it, so the syscall really is rt_sigprocmask" as *u8,
324 oa[TD_O_TSIG], TD_SIG_NONE, ctr)
325 gq("T05 and it did not exit early -- it drained and exited cleanly" as *u8, oa[TD_O_EXIT], TD_C_OK, ctr)
326 }
327 if la >= 0 { sys_close(la) }
328
329 // ---- ARM 2: NEG-CONTROL. The same harness against a daemon with NO drain. If this does not lose
330 // the in-flight request, the armed arm's success proves nothing at all.
331 let ln: i64 = td_listen(pn, TD_TRUE)
332 let on: *i64 = (sys_mmap(TD_OUT_BYTES)) as *i64
333 var ran_n: i64 = 0
334 if ln >= 0 { ran_n = td_run_inflight(TD_FALSE, ln, pn, on) }
335 td_report("NEG-CTRL" as *u8, on)
336 var obs_n: i64 = 0
337 if ran_n == 1 { if on[TD_O_INFLIGHT] == 1 { obs_n = 1 } }
338 if gv_need("anti-vacuity a request was PROVABLY in flight when TERM landed (NEG-CONTROL)" as *u8, obs_n, ctr) == 1 {
339 gq("T06 neg-control-undrained the client does NOT receive a complete response" as *u8,
340 on[TD_O_DONE], 0, ctr)
341 // TEST THE STATE, NOT THE MESSAGE: "the client got nothing" has several possible causes and
342 // only one of them is the one this rung is about.
343 gq("T07 neg-control-attribution it died BY SIGNAL 15, not from a broken harness" as *u8,
344 on[TD_O_TSIG], TD_SIG_TERM, ctr)
345 gq("T08 neg-control-same-denominator both arms reached the same in-flight condition" as *u8,
346 on[TD_O_INFLIGHT], oa[TD_O_INFLIGHT], ctr)
347 // BOTH SIGNALS PRESENT AT ONCE: two arms that each isolate one signal do not prove the
348 // mechanism discriminates between them.
349 var disc: i64 = 0
350 if oa[TD_O_DONE] == 1 { if on[TD_O_DONE] == 0 { disc = 1 } }
351 gq("T09 the drain strictly beats the undrained path on the SAME harness" as *u8, disc, 1, ctr)
352 }
353 if ln >= 0 { sys_close(ln) }
354
355 // ---- ARM 3: EXIT EARLY WHEN IDLE. A drain with nothing in flight must finish immediately rather
356 // than sleeping out its budget. The subject arms SIGALRM at the deadline, so a drain that waited
357 // for a timeout would be killed by signal 14 instead of exiting cleanly -- the deadline itself is
358 // the ruler, which needs no clock and no second magic number.
359 let li: i64 = td_listen(pi, TD_TRUE)
360 let oi: *i64 = (sys_mmap(TD_OUT_BYTES)) as *i64
361 var k2: i64 = 0
362 while k2 < TD_OUT_SLOTS { oi[k2] = 0; k2 = k2 + 1 }
363 var ran_i: i64 = 0
364 if li >= 0 {
365 let pid: i64 = sys_fork()
366 if pid == 0 { sys_exit(td_subject_idle(li)) }
367 let c: i64 = td_connect(pi)
368 if c >= 0 {
369 if td_get1(c) == TD_READY { ran_i = 1 }
370 sys_close(c)
371 }
372 // The subject is IDLE and its drain is already armed, so TERM cannot be missed and cannot kill.
373 nx_kill(pid, TD_SIG_TERM)
374 let st: *i64 = (sys_mmap(TD_OUT_BYTES)) as *i64
375 st[0] = 0
376 sys_wait4(pid, st, 0)
377 oi[TD_O_EXIT] = wait_status_rc(st[0])
378 oi[TD_O_TSIG] = wait_term_signal(st[0])
379 }
380 g_puts(" IDLE ready=" as *u8); g_putn(ran_i)
381 g_puts(" subject_exit=" as *u8); g_putn(oi[TD_O_EXIT])
382 g_puts(" killed_by_signal=" as *u8); g_putn(oi[TD_O_TSIG])
383 g_puts("\n" as *u8)
384 if gv_need("anti-vacuity the idle subject reported ready before TERM was sent" as *u8, ran_i, ctr) == 1 {
385 gq("T10 an IDLE daemon woke on the DRAIN EVENT and exited, it did not sleep out its budget" as *u8,
386 oi[TD_O_EXIT], TD_C_IDLE_DRAIN, ctr)
387 gq("T11 neg-control-alarm it was not killed by the deadline alarm either" as *u8,
388 oi[TD_O_TSIG], TD_SIG_NONE, ctr)
389 }
390 if li >= 0 { sys_close(li) }
391
392 let rc: i64 = gv_verdict("TS-DRAIN-GATE" as *u8, ctr, "each tooth states its own strength above" as *u8)
393 sys_exit(rc)
394 return rc
395}