nx_channel.nx source
↩ module page · 124 lines · 4209 B
1// channel.nx -- typed message-passing primitive (Phase M1 seed).
2//
3// Research: Honda 1993 ("Types for Dyadic Interaction"), Pony
4// actor-channel model, Go channels with session-type extensions.
5// The long-term destination is full session types (Honda 1998)
6// where the channel's type describes the entire protocol; this
7// file ships the foundation on which session-type checking will
8// stack in a future parse.nx pass.
9//
10// Today's capabilities:
11// * Typed FIFO channel with bounded capacity
12// * Non-blocking try_send / try_recv
13// * Blocking send / recv (spin-on-empty/full; MCU-friendly)
14// * Single-producer single-consumer (SPSC); MPSC / MPMC variants
15// ship in a follow-up once we have atomic primitives
16//
17// Currently specialised to i64 message type; generalises to Chan<T>
18// when full multi-parameter generics land in parse.nx.
19//
20// Scaling claim: same channel.nx source compiles on MCU (no kernel
21// threads, cooperative yield via __wfi between poll attempts) and
22// on supercomputer (the scheduler's context switch uses the same
23// primitive). Nothing about the API changes.
24
25// nx_safety_envelope:
26// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
27// sil_target: SIL1
28// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
29// verdict: NOT_YET_EVALUATED
30
31import "nx_syscalls.nx"
32
33// Ring-buffer backed channel. All SPSC ordering is maintained by
34// the head/tail indices; atomicity comes later via memory fences
35// (`__fence()`) once we run on multi-core.
36struct Chan {
37 buf: *i64, // ring storage; `cap` i64 slots
38 cap: i64, // capacity (must be power of 2 for index wrap)
39 head: i64, // next write position
40 tail: i64, // next read position
41}
42
43// Allocate a new channel with `cap` slots. cap is rounded up to the
44// next power of 2 so the head/tail wrap is a single AND mask instead
45// of a modulo.
46func chan_new(cap_hint: i64) -> *Chan {
47 var cap: i64 = 1
48 while cap < cap_hint { cap = cap * 2 }
49 if cap < 2 { cap = 2 }
50 let raw: *u8 = sys_mmap(64 + cap * 8 + 16)
51 let c: *Chan = raw as *Chan
52 c.buf = (raw as i64 + 64) as *i64
53 c.cap = cap
54 c.head = 0
55 c.tail = 0
56 return c
57}
58
59// Returns 1 if the channel is empty right now.
60func chan_is_empty(c: *Chan) -> i64 {
61 if c.head == c.tail { return 1 }
62 return 0
63}
64
65// Returns 1 if the channel is full right now. Full = one slot open
66// stays reserved so we can distinguish full from empty using only
67// head/tail.
68func chan_is_full(c: *Chan) -> i64 {
69 let next: i64 = (c.head + 1) & (c.cap - 1)
70 if next == c.tail { return 1 }
71 return 0
72}
73
74// Non-blocking send. Returns 1 on success, 0 when channel was full.
75func chan_try_send(c: *Chan, v: i64) -> i64 {
76 if chan_is_full(c) == 1 { return 0 }
77 c.buf[c.head] = v
78 // Memory fence so the store is visible before head advances --
79 // matters on multi-core; no-op on single-hart.
80 __fence()
81 c.head = (c.head + 1) & (c.cap - 1)
82 return 1
83}
84
85// Non-blocking receive. Returns 1 and writes value to *out on
86// success; returns 0 when channel was empty (*out untouched).
87func chan_try_recv(c: *Chan, out: *i64) -> i64 {
88 if chan_is_empty(c) == 1 { return 0 }
89 *out = c.buf[c.tail]
90 __fence()
91 c.tail = (c.tail + 1) & (c.cap - 1)
92 return 1
93}
94
95// Blocking send -- spins until space. On MCU / kernel contexts a
96// `__wfi()` yields the hart between attempts. On multi-threaded
97// userspace the caller should integrate with the scheduler rather
98// than busy-looping.
99func chan_send(c: *Chan, v: i64) -> i64 {
100 var sent: i64 = 0
101 while sent == 0 {
102 sent = chan_try_send(c, v)
103 if sent == 0 { __wfi() }
104 }
105 return 0
106}
107
108// Blocking receive -- spins until a message arrives.
109func chan_recv(c: *Chan) -> i64 {
110 let out_raw: *u8 = sys_mmap(16)
111 let out: *i64 = out_raw as *i64
112 *out = 0
113 var got: i64 = 0
114 while got == 0 {
115 got = chan_try_recv(c, out)
116 if got == 0 { __wfi() }
117 }
118 return *out
119}
120
121// Returns current message count (head - tail, wrapped to capacity).
122func chan_len(c: *Chan) -> i64 {
123 return (c.head - c.tail) & (c.cap - 1)
124}