The boundary · L4 and L3

The network

/net is the network, served by netd, a task that runs sysn's stack: Ethernet, ARP, IPv4, ICMP echo and UDP, as plain sysp, every obligation proven. Beneath it the network card's driver passes frames to and from a virtio network device, on QEMU's user network. cat /net/eth0/arp shows the neighbours the stack has heard from (sysk 052; 053: the card's own directory), and ping 10.0.2.2 talks to one (sysk 054), a program lent only its conversation (sysk 058).

Four tasks in a line

The shell asks netd over the files protocol, as it asks the disk's server and the entropy driver: a request and a reply of 576 bytes each (Files). netd and the driver pass frames over a pair of streams of their own, typed channels the deadlock model sees, rather than files: a frame is up to 1,514 bytes, more than a file's payload (docs/directions.md). Pick a moment to follow it.

A card and its files

The card has a directory, eth0, and a second name for it, eth: the card, whichever it is, so a script that wants the network need not know its number. With a second card, eth1 would be the next directory, and eth still the first (sysk 053). The walk follows names one at a time, so both lead to the same node, and a stat or a read says the same through either. Its three files say how the card is; icmp holds conversations (below). Each file is rendered when it is read, as one s-expression a line, so the shell and a host lay them out as values (syst). Nothing in /net can be written: changing the address or flushing the neighbours is control, which waits for the operator profile (docs/authority.md). These are a boot test, after a datagram from the host:

sysk> ls /net
eth/
eth0/
sysk> ls /net/eth0
addr
arp
stats
icmp/
sysk> cat /net/eth0/addr
(addr (mac 52:54:00:12:34:56) (ip 10.0.2.15) (mask 255.255.255.0) (gateway 10.0.2.2))
sysk> cat /net/eth/arp
(neighbour (ip 10.0.2.2) (mac 52:55:0a:00:02:02))
sysk> cat /net/eth0/stats
(taken (arp 1) (icmp 0) (udp 1))
(dropped (short 0) (malformed 0) (not-ours 0) (protocol 0) (bad-sum 0) (fragment 0))

The address is QEMU's guest's, 10.0.2.15 on 10.0.2.0/24, with the gateway at 10.0.2.2; the hardware address is the card's own, read from its configuration. At the start netd asks for the gateway's address, so it is a neighbour before anything needs it. The counts are the stack's, by protocol and by the reason a frame was dropped. Without a card, the tree is there and addr says (addr none).

Where /net is, the shell learns from the manifest: its namespace mounts netd's tree there, ("/net" net-ask) (Files).

Neither waits to send

netd sends frames to the driver, and the driver sends frames to netd. If each could block sending to the other, both full, the two would wait forever. Neither does: each waits with alt for whichever comes first, a frame from the other, room to send its own, or (the driver) the card. A frame that cannot go yet waits in its task:

TaskWhile a frame waits to go
net-driverA frame the card received waits for room on frames-in; meanwhile the card still sends every frame frames-out brings.
netdA frame the stack wrote (an ARP reply, an echo reply) waits for room on frames-out; meanwhile netd takes nothing from frames-in, but still answers the shell.

The deadlock model proves every run can still finish. Its first verdict was a cycle: at the end, the driver drained frames-out while it still owed frames-in. The fix made the driver plainer: once it stops taking frames from the card, for any reason, it closes frames-in first, then drains frames-out. And netd's loop ends where the shell's requests end, as the model reads a server's (sysk 047), so the shell's view of /net's replies does not carry their end through every step. A third server still costs the shell's configurations a third more, 17,078 from 11,824: every call of ask has one more way to go.

The card

A virtio network device has two queues: 0 receives, 1 sends (virtio 1.2 §5.1). Every frame either way follows a 12-byte header, all zero here: no checksums offloaded, no segments merged. The driver lends the card one buffer of 1,526 bytes at a time to receive into, and lends each frame to send as one part the card reads. Both go through the generic queue of sysk 042, so the kernel still knows no device's requests; what it gives a device stays proven and private.

One thing was new: a buffer the device may never give back. The disk and the entropy device return every request; a receive buffer comes back only when a frame arrives. So the driver could not finish, holding a buffer only the device could return. sysk 052 added one function to the kernel's device file, virtio-reset: it stops the device and waits until it reads as reset, when the device has let go of every queue, and the buffer is the driver's again (Storage). That is the only change in kernel/devices.sysp; the measure sysk 042 set was "no line changed", so it was met but for this.

The stack, from another project

sysn's files are compiled into sysk's program when a file of it calls them: tools/wire.rkt --uses lists ../sysn/net/ as it lists lib/. The stack allocates nothing: netd lends it 116 bytes of its heap for its neighbours and counts (sysn 002), and gives it each frame as a view of a channel's message. It answers ARP requests for 10.0.2.15 and echo requests, and counts what it takes. It holds no packets: a send whose next hop is not known yet writes an ARP request instead, and says so.

Conversations, and ping

Talking to another host is a conversation, in Plan 9's shape (sysk 054). icmp, under the card, holds clone and up to four conversations. Opening clone to write takes one not in use, made new, and the fid is that conversation's ctl from then on; reading it says which. A conversation is in use while a fid names one of its files, the shell's or a job's, or while it is lent (sysk 058); only one in use is listed, or can be named. So it ends when its holders let go: nothing to hang up, nothing left behind, and no stale count to read.

FileReadWritten
cloneopened to write: a conversation's ctl—
N/ctlNconnect A.B.C.D: the host
N/datathe reply to the last echo, once: (echo (from …) (seq …) (ttl …) (us …)); a read that waits waits for it, and says (lost (seq …)) when its time passesan echo request, carrying what was written
N/status(icmp (to 10.0.2.2) (sent 3) (got 3))—

ping is a program of the catalogue (sysk 058; the shell's own command before). Naming the peer is granting it: when a command gives a program an address, the shell dials it, as Plan 9's dial does, opening clone and writing connect, and then lends the job only the conversation's data, to read and write. The job cannot write ctl, so it cannot say where its echoes go (docs/authority.md, Talk). It writes an echo, reads the reply with a read that waits up to a second, and paces the next by its clock, a second after the first. A boot test, on QEMU's user network:

sysk> ping 10.0.2.2
(echo (from 10.0.2.2) (seq 0) (ttl 255) (us 2029))
(echo (from 10.0.2.2) (seq 1) (ttl 255) (us 1035))
(echo (from 10.0.2.2) (seq 2) (ttl 255) (us 1581))
(ping (sent 3) (got 3))
job ended
sysk> ping 10.0.2.99 --times 1
(lost (seq 0))
(ping (sent 1) (got 0))
job ended
sysk> ping 300.1.1.1
not an address: 300.1.1.1
sysk> explain (ping 10.0.2.2 (times 2))
(task (program ping) (ask talk-ask) (answer talk-reply)
  (out out) (times 2))
(lends (data (dial 10.0.2.2)) (rights read write))
(verdict passed)

The round trip is netd's to measure: it reads its clock when the echo goes and when the reply comes, so the time is the network's and the stack's, not the job's. A reply is matched by the conversation's identifier and the last echo's sequence number, and kept once. No host answers 10.0.2.99: the stack asks for its hardware address instead of sending the echo, as it holds no packets, and the read's second passes.

netd serves jobs

netd serves the pool's talk service as fsd serves files (sysk 031): when a job that binds it starts, netd opens a lease and serves the job's requests beside the shell's, and frames, until the job's requests end; then the job's fids, and the lend, are gone, and the conversation with them. It never waits on the job but through alt. Which service a job binds is where the thing lent is: the namespace says (/net 7 (jobs 5 6)), so wc /net/eth/addr is a job of netd's too, and wc /notes/x one of fsd's (Lending). Programs are clients of a service of their message size, not of one by name.

A read that waits waits inside netd's answer to it: netd takes the request, then goes on taking frames, and sending them, until the reply comes or its clock says the time is up, and then answers. The other client's next request waits that second at most. Its first version held the read and answered later from its main loop; the deadlock model saw a reply that could come when the shell was waiting on another server, and rejected it. Answered in the request's own branch, every reply follows its request, as the model reads a server.

What comes next

UDP the same way: udp/clone, conversations, a program lent one; then the network shell, commands from outside, which needs the profiles and declared needs first (docs/authority.md): (needs (talk ARG)) in a program's spec, so the job check refuses any other lend.