nx_atom.nx source

1// nx_atom.nx -- atomic primitives + memory ordering. 2// 3// FOUNDATION LAYER. Every lock-free data structure, every SMP-safe 4// counter, every message queue in NishiOS sits on top of these 5// operations: load, store, CAS, FAA, and memory barriers. 6// 7// Why now (DARPA-class concurrency correctness): 8// 9// The current observability stack (nx_log, nx_trace, nx_metrics, 10// nx_arena, nx_ring, nx_id) is single-threaded-only. The moment 11// NishiOS ships its SMP scheduler, every one of those modules 12// either gains an atomic primitive or silently corrupts. Land 13// the primitive FIRST -- mechanical retrofit, not rescue. 14// 15// seL4 / Nemesis lineage: concurrency correctness is the 16// second-highest cost in kernel verification (after memory 17// safety). seL4's proof rests on a uniprocessor model; the 18// multi-core extension (MCS seL4) required re-proving sizable 19// chunks around synchronisation primitives. Getting the atomic 20// memory model RIGHT AT THE SOURCE LANGUAGE LAYER pays that cost 21// once. 22// 23// MEMORY ORDERING TAXONOMY (RV64A, C11 atomic_*, Rust atomic_*): 24// 25// NX_MO_RELAXED No ordering. Counter bumps. Fastest. 26// NX_MO_CONSUME Data-dependent loads (C11 intent; rarely used). 27// NX_MO_ACQUIRE Load-acquire: no load/store after this op can 28// migrate BEFORE it. Standard lock acquire. 29// NX_MO_RELEASE Store-release: no load/store before this op 30// can migrate AFTER it. Standard lock release. 31// NX_MO_ACQ_REL Both -- used on RMW (read-modify-write) ops. 32// NX_MO_SEQ_CST Sequential consistency: single global order 33// across all seq-cst ops on the machine. Slowest. 34// Default for userland until profiling warrants 35// weaker ordering. 36// 37// RV64A MAPPING (RISC-V A extension) -- emit targets when nxc2 grows 38// inline asm: 39// 40// load-acquire lr.d / ld + fence r,rw (aq bit on lr.d) 41// store-release sd + fence rw,w / sc.d (rl bit on sc.d) 42// CAS lr.d + sc.d loop 43// FAA amoadd.d (acq/rel via aq/rl) 44// Fence fence [pred], [succ] 45// 46// x86 TSO needs fewer fences; ARM weak-memory needs more. This 47// module is the abstraction point so user code writes once. 48// 49// WHAT WE SHIP TODAY: 50// 51// * Ordering enum (stable across future backends) 52// * Public API: load / store / cas / faa / fence (i64 cell) 53// * Inline-asm stubs with TODO markers -- NishiLang doesn't yet 54// have an __asm intrinsic; when it lands these emit real RV64A 55// * Convenience: inc, dec, try_lock, unlock spinlock pattern 56// * Property tests: CAS observe-then-write, FAA returns-prior, 57// spinlock take/release discipline 58// 59// WHAT WE DO NOT YET SHIP: 60// 61// * Real HW emit -- compiler change needed (__atomic_cas_i64 etc. 62// intrinsic that lowers to lr.d/sc.d). Tracked Q7 cluster. 63// * Per-ordering cost model for the regalloc. Future commit. 64// * SEQ_CST optimisation (store-load barrier elision when prev 65// op is already a release). When the cost model lands. 66// 67// REFERENCES: 68// 69// * C11 6.7.2.4 _Atomic; 7.17 <stdatomic.h> 70// * Rust std::sync::atomic (2015 stabilisation) 71// * Boehm-Adve "Foundations of the C++ Concurrency Memory Model" 72// PLDI 2008 73// * Lea & Manson JSR-133 Java Memory Model 74// * McKenney "Memory Barriers: a Hardware View for Software 75// Hackers" Linux kernel primer 76// * Sewell et al. "x86-TSO: A Rigorous and Usable Programmer's 77// Model for x86 Multiprocessors" CACM 2010 78// * RISC-V Unprivileged ISA, Chapter 14 (A extension) 79// * Klein et al. seL4 MCS extension 2018 (SMP proof experience) 80 81// nx_safety_envelope: 82// intended_use: AUTO_APPLIED -- primitive-specific tuning queued 83// sil_target: SIL1 84// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail] 85// verdict: NOT_YET_EVALUATED 86 87import "nx_syscalls.nx" 88 89// ---- memory ordering constants ------------------------------------ 90 91const NX_MO_RELAXED: i64 = 0 92const NX_MO_CONSUME: i64 = 1 93const NX_MO_ACQUIRE: i64 = 2 94const NX_MO_RELEASE: i64 = 3 95const NX_MO_ACQ_REL: i64 = 4 96const NX_MO_SEQ_CST: i64 = 5 97 98// ---- core primitives (stub lowering; HW emit TODO) ---------------- 99 100// Ordered load of 8 bytes. Lowers to `lr.d.aq` (ACQUIRE/SEQ_CST) or 101// plain `ld` (RELAXED) on RV64A; plain `movq` on x86 TSO. Real HW 102// emit since 2026-05-15. 103func nx_atom_load_i64(addr: *i64, mo: i64) -> i64 { 104 return __atomic_load_i64(addr, mo) 105} 106 107// Ordered store of 8 bytes. Lowers to `amoswap.d.rl x0, val, (addr)` 108// for RELEASE/SEQ_CST on RV64A; `xchgq` on SEQ_CST x86, `movq` else. 109func nx_atom_store_i64(addr: *i64, val: i64, mo: i64) -> i64 { 110 __atomic_store_i64(addr, val, mo) 111 return 0 112} 113 114// Compare-and-swap: if *addr == expected, write new and return 1; 115// else leave *addr alone, return 0. Lowers to a `lr.d.aq + sc.d.rl` 116// retry loop on RV64A; single `lock cmpxchgq` + setz on x86. 117func nx_atom_cas_i64(addr: *i64, expected: i64, new_val: i64, mo: i64) -> i64 { 118 return __atomic_cas_i64(addr, expected, new_val, mo) 119} 120 121// Fetch-and-add: returns the OLD value; atomically adds delta. 122// Single-instruction `amoadd.d.aqrl` on RV64A; `lock xaddq` on x86. 123func nx_atom_faa_i64(addr: *i64, delta: i64, mo: i64) -> i64 { 124 return __atomic_faa_i64(addr, delta, mo) 125} 126 127// Standalone fence. Lowers to `fence rw, rw` on RV64 SEQ_CST, 128// `fence r, rw` on ACQUIRE, `fence rw, w` on RELEASE; `mfence` on 129// x86 SEQ_CST/ACQ_REL. RELAXED is a no-op. 130func nx_atom_fence(mo: i64) -> i64 { 131 __atomic_fence(mo) 132 return 0 133} 134 135// ---- convenience primitives built on core ------------------------- 136 137// Increment, returning the new value. 138func nx_atom_inc_i64(addr: *i64) -> i64 { 139 let old: i64 = nx_atom_faa_i64(addr, 1, NX_MO_SEQ_CST) 140 return old + 1 141} 142 143// Decrement, returning the new value. 144func nx_atom_dec_i64(addr: *i64) -> i64 { 145 let old: i64 = nx_atom_faa_i64(addr, -1, NX_MO_SEQ_CST) 146 return old - 1 147} 148 149// Spinlock try-take (0=free, 1=taken). Returns 1 if acquired. 150func nx_atom_try_lock_i64(addr: *i64) -> i64 { 151 return nx_atom_cas_i64(addr, 0, 1, NX_MO_ACQUIRE) 152} 153 154// Spinlock release. 155func nx_atom_unlock_i64(addr: *i64) -> i64 { 156 nx_atom_store_i64(addr, 0, NX_MO_RELEASE) 157 return 0 158} 159 160// ---- self-test ---------------------------------------------------- 161 162func main() -> i64 { 163 let cell_raw: *u8 = sys_mmap(16) 164 let cell: *i64 = cell_raw as *i64 165 *cell = 0 166 167 // Load/store round-trip. 168 nx_atom_store_i64(cell, 42, NX_MO_RELAXED) 169 if nx_atom_load_i64(cell, NX_MO_RELAXED) != 42 { 170 return __syscall(93, 10, 0, 0, 0, 0, 0) 171 } 172 173 // FAA returns OLD, increments. 174 let old1: i64 = nx_atom_faa_i64(cell, 5, NX_MO_SEQ_CST) 175 if old1 != 42 { return __syscall(93, 20, 0, 0, 0, 0, 0) } 176 if *cell != 47 { return __syscall(93, 21, 0, 0, 0, 0, 0) } 177 178 // CAS success: observes old, writes new. 179 let r_ok: i64 = nx_atom_cas_i64(cell, 47, 100, NX_MO_SEQ_CST) 180 if r_ok != 1 { return __syscall(93, 30, 0, 0, 0, 0, 0) } 181 if *cell != 100 { return __syscall(93, 31, 0, 0, 0, 0, 0) } 182 183 // CAS failure: leaves cell, returns 0. 184 let r_fail: i64 = nx_atom_cas_i64(cell, 999, 123, NX_MO_SEQ_CST) 185 if r_fail != 0 { return __syscall(93, 40, 0, 0, 0, 0, 0) } 186 if *cell != 100 { return __syscall(93, 41, 0, 0, 0, 0, 0) } 187 188 // Inc / dec. 189 nx_atom_store_i64(cell, 10, NX_MO_RELAXED) 190 let after_inc: i64 = nx_atom_inc_i64(cell) 191 if after_inc != 11 { return __syscall(93, 50, 0, 0, 0, 0, 0) } 192 if *cell != 11 { return __syscall(93, 51, 0, 0, 0, 0, 0) } 193 let after_dec: i64 = nx_atom_dec_i64(cell) 194 if after_dec != 10 { return __syscall(93, 52, 0, 0, 0, 0, 0) } 195 196 // Spinlock discipline. 197 let lock_raw: *u8 = sys_mmap(16) 198 let lock: *i64 = lock_raw as *i64 199 *lock = 0 200 let got_a: i64 = nx_atom_try_lock_i64(lock) 201 if got_a != 1 { return __syscall(93, 60, 0, 0, 0, 0, 0) } 202 let got_b: i64 = nx_atom_try_lock_i64(lock) 203 if got_b != 0 { return __syscall(93, 61, 0, 0, 0, 0, 0) } 204 nx_atom_unlock_i64(lock) 205 let got_c: i64 = nx_atom_try_lock_i64(lock) 206 if got_c != 1 { return __syscall(93, 62, 0, 0, 0, 0, 0) } 207 208 // Ordering constants stable + distinct. 209 if NX_MO_RELAXED != 0 { return __syscall(93, 70, 0, 0, 0, 0, 0) } 210 if NX_MO_SEQ_CST != 5 { return __syscall(93, 71, 0, 0, 0, 0, 0) } 211 212 return 0 213}