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 91// MOVED DOWN to nx_syscalls.nx on 2026-08-25. This module still sees every one of them because 92// it imports that file, and so does every consumer of this module -- no caller changes. 93// 94// WHY DOWN AND NOT HERE. The arena allocator inside nx_syscalls needs an ordering value for its 95// own lock, and nx_syscalls CANNOT import this module: this module imports IT, so that would be a 96// cycle. Spelling the values a second time down there would have made it the FOURTH copy, because 97// they were already declared three times over -- here, in nx_atomic_intrinsic_test and in 98// nx_simd_i32x8_test (measured, corpus_complete=1, all three reading 5 for SEQ_CST today). 99// A constant written in four places is four rulers that agree until one of them does not. 100// ONE DEFINITION, AT THE LAYER EVERYTHING ALREADY IMPORTS. 101 102// ---- core primitives (stub lowering; HW emit TODO) ---------------- 103 104// Ordered load of 8 bytes. Lowers to `lr.d.aq` (ACQUIRE/SEQ_CST) or 105// plain `ld` (RELAXED) on RV64A; plain `movq` on x86 TSO. Real HW 106// emit since 2026-05-15. 107func nx_atom_load_i64(addr: *i64, mo: i64) -> i64 { 108 return __atomic_load_i64(addr, mo) 109} 110 111// Ordered store of 8 bytes. Lowers to `amoswap.d.rl x0, val, (addr)` 112// for RELEASE/SEQ_CST on RV64A; `xchgq` on SEQ_CST x86, `movq` else. 113func nx_atom_store_i64(addr: *i64, val: i64, mo: i64) -> i64 { 114 // ⚠nx_cc REFUSES a bare intrinsic statement ("computes a value and never uses it"), and an atomic 115 // STORE has no meaningful result to use -- so the result is bound and discarded deliberately. Before 116 // this, nx_atom.nx DID NOT COMPILE AT ALL (control 2026-08-14: built standalone, COMPILE-FAIL), which 117 // means every organ importing this shared concurrency lib was unbuildable. The contract is unchanged: 118 // this function still returns 0, so no caller testing the result is affected. 119 let discarded: i64 = __atomic_store_i64(addr, val, mo) 120 if discarded != 0 { return 0 } 121 return 0 122} 123 124// Compare-and-swap: if *addr == expected, write new and return 1; 125// else leave *addr alone, return 0. Lowers to a `lr.d.aq + sc.d.rl` 126// retry loop on RV64A; single `lock cmpxchgq` + setz on x86. 127func nx_atom_cas_i64(addr: *i64, expected: i64, new_val: i64, mo: i64) -> i64 { 128 return __atomic_cas_i64(addr, expected, new_val, mo) 129} 130 131// Fetch-and-add: returns the OLD value; atomically adds delta. 132// Single-instruction `amoadd.d.aqrl` on RV64A; `lock xaddq` on x86. 133func nx_atom_faa_i64(addr: *i64, delta: i64, mo: i64) -> i64 { 134 return __atomic_faa_i64(addr, delta, mo) 135} 136 137// Standalone fence. Lowers to `fence rw, rw` on RV64 SEQ_CST, 138// `fence r, rw` on ACQUIRE, `fence rw, w` on RELEASE; `mfence` on 139// x86 SEQ_CST/ACQ_REL. RELAXED is a no-op. 140func nx_atom_fence(mo: i64) -> i64 { 141 // Same reason as nx_atom_store_i64 above: a fence has no result worth using, but nx_cc requires the 142 // value be consumed, so it is bound and discarded. Contract unchanged -- still returns 0. 143 let discarded: i64 = __atomic_fence(mo) 144 if discarded != 0 { return 0 } 145 return 0 146} 147 148// ---- convenience primitives built on core ------------------------- 149 150// Increment, returning the new value. 151func nx_atom_inc_i64(addr: *i64) -> i64 { 152 let old: i64 = nx_atom_faa_i64(addr, 1, NX_MO_SEQ_CST) 153 return old + 1 154} 155 156// Decrement, returning the new value. 157func nx_atom_dec_i64(addr: *i64) -> i64 { 158 let old: i64 = nx_atom_faa_i64(addr, -1, NX_MO_SEQ_CST) 159 return old - 1 160} 161 162// Spinlock try-take (0=free, 1=taken). Returns 1 if acquired. 163func nx_atom_try_lock_i64(addr: *i64) -> i64 { 164 return nx_atom_cas_i64(addr, 0, 1, NX_MO_ACQUIRE) 165} 166 167// Spinlock release. 168func nx_atom_unlock_i64(addr: *i64) -> i64 { 169 nx_atom_store_i64(addr, 0, NX_MO_RELEASE) 170 return 0 171} 172 173// ---- self-test ---------------------------------------------------- 174 175func main() -> i64 { 176 let cell_raw: *u8 = sys_mmap(16) 177 let cell: *i64 = cell_raw as *i64 178 *cell = 0 179 180 // Load/store round-trip. 181 nx_atom_store_i64(cell, 42, NX_MO_RELAXED) 182 if nx_atom_load_i64(cell, NX_MO_RELAXED) != 42 { 183 return __syscall(93, 10, 0, 0, 0, 0, 0) 184 } 185 186 // FAA returns OLD, increments. 187 let old1: i64 = nx_atom_faa_i64(cell, 5, NX_MO_SEQ_CST) 188 if old1 != 42 { return __syscall(93, 20, 0, 0, 0, 0, 0) } 189 if *cell != 47 { return __syscall(93, 21, 0, 0, 0, 0, 0) } 190 191 // CAS success: observes old, writes new. 192 let r_ok: i64 = nx_atom_cas_i64(cell, 47, 100, NX_MO_SEQ_CST) 193 if r_ok != 1 { return __syscall(93, 30, 0, 0, 0, 0, 0) } 194 if *cell != 100 { return __syscall(93, 31, 0, 0, 0, 0, 0) } 195 196 // CAS failure: leaves cell, returns 0. 197 let r_fail: i64 = nx_atom_cas_i64(cell, 999, 123, NX_MO_SEQ_CST) 198 if r_fail != 0 { return __syscall(93, 40, 0, 0, 0, 0, 0) } 199 if *cell != 100 { return __syscall(93, 41, 0, 0, 0, 0, 0) } 200 201 // Inc / dec. 202 nx_atom_store_i64(cell, 10, NX_MO_RELAXED) 203 let after_inc: i64 = nx_atom_inc_i64(cell) 204 if after_inc != 11 { return __syscall(93, 50, 0, 0, 0, 0, 0) } 205 if *cell != 11 { return __syscall(93, 51, 0, 0, 0, 0, 0) } 206 let after_dec: i64 = nx_atom_dec_i64(cell) 207 if after_dec != 10 { return __syscall(93, 52, 0, 0, 0, 0, 0) } 208 209 // Spinlock discipline. 210 let lock_raw: *u8 = sys_mmap(16) 211 let lock: *i64 = lock_raw as *i64 212 *lock = 0 213 let got_a: i64 = nx_atom_try_lock_i64(lock) 214 if got_a != 1 { return __syscall(93, 60, 0, 0, 0, 0, 0) } 215 let got_b: i64 = nx_atom_try_lock_i64(lock) 216 if got_b != 0 { return __syscall(93, 61, 0, 0, 0, 0, 0) } 217 nx_atom_unlock_i64(lock) 218 let got_c: i64 = nx_atom_try_lock_i64(lock) 219 if got_c != 1 { return __syscall(93, 62, 0, 0, 0, 0, 0) } 220 221 // Ordering constants stable + distinct. 222 if NX_MO_RELAXED != 0 { return __syscall(93, 70, 0, 0, 0, 0, 0) } 223 if NX_MO_SEQ_CST != 5 { return __syscall(93, 71, 0, 0, 0, 0, 0) } 224 225 return 0 226}