code wiki / _hdl_build / nx_atomic_swap.nx
nx_atomic_swap.nx source
↩ module page · 75 lines · 3400 B
1// nx_atomic_swap.nx -- DEP-001 (CALLOUT-012 deploy-exceed). Prove + register the ATOMIC content
2// swap: write the new version to a temp file, then sys_renameat(temp, live) -> live is replaced
3// in ONE atomic FS operation (a concurrent reader sees whole-old or whole-new, NEVER torn). This
4// is the no-torn-deploy primitive the deploy-check named as a GAP (had via renameat, unregistered).
5// Composes the PROVEN sys_renameat (nx_syscalls). Self-validating gate (ATOMICSWAPGATE):
6// pre=old, swap rc=0, post=new (old GONE), temp consumed. license_tier: ORIGINAL
7import "nx_syscalls.nx"
8const AW_MAGIC_4096: i64 = 4096
9
10const AW_LIVE: *u8 = "/tmp/nx_asw_live"
11const AW_TMP: *u8 = "/tmp/nx_asw_tmp"
12const AW_V1: *u8 = "VERSION-1-OLD-content"
13const AW_V2: *u8 = "VERSION-2-NEW-content-atomic"
14
15func aw_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
16func aw_putn(v: i64) -> i64 { let bb: *u8 = sys_mmap(28); var m: i64=v; if m<0 {m=0-m}; let t: *u8 = sys_mmap(28); var k: i64=0; if m==0 {t[0]=48;k=1}; while m>0 {t[k]=48+(m%10); m=m/10; k=k+1}; var i: i64=0; while i<k {bb[i]=t[k-1-i]; i=i+1}; sys_write(1, bb, k); return 0 }
17func aw_strlen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
18
19func aw_write(path: *u8, content: *u8) -> i64 {
20 let fd: i64 = sys_openat_wr(path, 420)
21 if fd < 0 { return 0 - 1 }
22 sys_write(fd, content, aw_strlen(content))
23 sys_close(fd)
24 return 0
25}
26func aw_read(path: *u8, buf: *u8, cap: i64) -> i64 {
27 let fd: i64 = sys_openat_rd(path)
28 if fd < 0 { return 0 - 1 }
29 var tot: i64 = 0
30 var r: i64 = 1
31 while r > 0 { let dst: *u8 = ((buf as i64) + tot) as *u8; r = sys_read(fd, dst, cap - tot); if r > 0 { tot = tot + r } }
32 sys_close(fd)
33 return tot
34}
35func aw_has(buf: *u8, n: i64, needle: *u8) -> i64 {
36 var m: i64 = 0; while needle[m] != (0 as u8) { m = m + 1 }
37 if m == 0 { return 0 }
38 var i: i64 = 0
39 while i + m <= n { var j: i64 = 0; var ok: i64 = 1; while j < m { if buf[i + j] != needle[j] { ok = 0; j = m } else { j = j + 1 } } if ok == 1 { return 1 } i = i + 1 }
40 return 0
41}
42
43func main() -> i64 {
44 let buf: *u8 = sys_mmap(AW_MAGIC_4096)
45
46 aw_write(AW_LIVE, AW_V1)
47 let pre_n: i64 = aw_read(AW_LIVE, buf, AW_MAGIC_4096)
48 let pre_v1: i64 = aw_has(buf, pre_n, AW_V1)
49
50 aw_write(AW_TMP, AW_V2)
51 let rc: i64 = sys_renameat(AW_TMP, AW_LIVE)
52 var swap_ok: i64 = 0; if rc == 0 { swap_ok = 1 }
53
54 let post_n: i64 = aw_read(AW_LIVE, buf, AW_MAGIC_4096)
55 let post_v2: i64 = aw_has(buf, post_n, AW_V2)
56 let post_v1: i64 = aw_has(buf, post_n, AW_V1)
57 let tmp_after: i64 = aw_read(AW_TMP, buf, AW_MAGIC_4096)
58 var tmp_gone: i64 = 0; if tmp_after < 0 { tmp_gone = 1 }
59
60 aw_puts("ATOMICSWAPGATE pre_old=" as *u8); aw_putn(pre_v1)
61 aw_puts(" swap_rc0=" as *u8); aw_putn(swap_ok)
62 aw_puts(" post_new=" as *u8); aw_putn(post_v2)
63 aw_puts(" old_replaced=" as *u8); if post_v1 == 0 { aw_putn(1) } else { aw_putn(0) }
64 aw_puts(" temp_consumed=" as *u8); aw_putn(tmp_gone)
65
66 var ok: i64 = 1
67 if pre_v1 != 1 { ok = 0 }
68 if swap_ok != 1 { ok = 0 }
69 if post_v2 != 1 { ok = 0 }
70 if post_v1 != 0 { ok = 0 }
71 if tmp_gone != 1 { ok = 0 }
72 if ok == 1 { aw_puts(" verdict=GREEN registered=atomic-swap\n" as *u8); return 0 }
73 aw_puts(" verdict=RED\n" as *u8)
74 return 1
75}