Bytes in, bytes out
sysn is the network for sysk: Ethernet, ARP, IPv4, ICMP echo and UDP, as functions over buffers and one value of state. It has no tasks, no channels, no clock and no device. Nothing in it waits, does input or output, or allocates: even the state's memory is lent by the caller, once, as bytes. A frame comes in as bytes; what to send goes out as bytes, into a buffer the caller lends. sysk runs it in netd, the task that serves /net (sysk 052); here it runs on the host, against QEMU's own network.
net/Two ways in, and what comes out
A frame that arrived goes to net-input. A ping or a datagram to send goes to net-ping or net-send. Each returns a value saying what happened, an enum: Got for a frame taken, Sent for a send. Pick a case to follow it through the layers; what the stack said is from a recording of it talking to QEMU's network.
The caller decides when
The stack holds no packets. To send to a host whose hardware address it does not know yet, it writes an ARP request into the caller's buffer instead and returns (asking (len 60)). The caller sends that, and when a frame it passes in later comes back as (learned (ip …)), it sends again. This is the first ping of the recording, exactly:
Waiting, retrying and giving up are the caller's: on the host, a few lines of Racket; in sysk, the task that serves /net, which has a clock and channels. So the stack's code has no time in it at all, and every path through it ends.
What a Got promises
Every function that takes part of a frame ensures the same predicate of what it returns, and so does net-input: a reply fits the buffer lent for it, a datagram's payload lies within the frame it came in, and every number is what its field can hold. A caller can hand the payload on, or print a port, with no check of its own. The frame itself is untrusted: these hold whatever bytes arrive.
Why a frame is dropped
A frame the stack does not take comes back as (dropped (why …)), and the state counts it by reason, so a server can show the counts as files. The reasons, in the order the stack checks:
| Reason | When |
|---|---|
| short | fewer bytes than a header needs, or than the IPv4 total length says |
| not-ours | for another hardware address (not ours or every host's), or another IPv4 address |
| malformed | an IPv4 version that is not 4, a header shorter than 20 bytes or longer than the packet; ARP not for IPv4 over Ethernet; a UDP length that does not fit; an ICMP message shorter than its header |
| bad-sum | the IPv4 header's, ICMP's or UDP's checksum does not hold |
| fragment | a fragment of a larger packet: the stack takes none |
| protocol | a type of frame, an IPv4 protocol, an ICMP message or an ARP operation the stack does not take |
Every reason is exercised by hostile frames: frames slirp sent, cut short at every length and changed the ways a broken network would change them.
The state
One value: the host's addresses, its subnet and gateway, the next IPv4 identification, and 116 bytes of memory the caller lends it once (sysn 002): the last eight neighbours it heard from and the counts, in network order like everything else the stack reads. A caller that allocates, such as the host program, allocates them; sysk's net task takes them from its heap. net-end gives them back. The invariant is proven wherever the state crosses a function's boundary.