Bytes in, bytes out
sysn is the network for sysk: Ethernet, ARP, IPv4, ICMP echo and errors, UDP, TCP and a DNS resolver, as functions over buffers and one value of state. It has no tasks, no channels, no clock and no device: when the time matters, the caller gives it. 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, with the time. A ping or a datagram to send goes to net-ping or net-send, and a frame no one took that should be answered with an error, to net-unreachable (sysn 009); TCP has calls of its own, tcp-connect, tcp-send and the rest (TCP). 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. The stack reads no clock: TCP's timers are deadlines it tells the caller, who calls it back then with the time (TCP). 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; a TCP data offset below 20 bytes or past the segment, an option that runs past the header; a TCP segment without an ACK where one is due |
| bad-sum | the IPv4 header's, ICMP's, UDP's or TCP'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 |
| full | a returned SYN cookie when no conversation is free, nor one in time-wait (TCP) |
| window | a TCP reset outside the window, or a segment that answers no SYN of ours (RFC 5961) |
| throttled | a challenge ACK past 10 in 5 s (RFC 5961) |
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 the memory the caller lends it once (sysn 002): the last eight neighbours it heard from and the counts, 132 bytes in network order like everything else the stack reads, then TCP's part, as many conversations as the memory holds (TCP). 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.