Conversation
Guest TCP leaves through the mixnet and nowhere else. When the mixnet holds no gateway, net.sockets answers the connect with E_NO_TRANSPORT (6); the personality turned every non-zero status into ECONNREFUSED, so a program was told a peer had answered and refused it when no packet could have left the machine. Status 6 is now ENETUNREACH, the errno Linux gives when there is no route. Every other refusal stays ECONNREFUSED, and a call that got no reply stays EIO. The mixnet stays the only way out: nothing here opens a direct path.
…ishes them virtio-net wrote descriptors, avail ring slots and the frame itself, then the avail index, with no fence anywhere. The descriptor and ring stores are volatile, but the frame bytes on the TX side are a plain copy, and Rust only orders volatile accesses against each other: the compiler is free to sink the copy past the index store that tells the device to read it. On the RX side the used element and the frame were read after the used index with nothing tying them to it. x86 hardware keeps these in order today; the language does not, and a weakly ordered CPU would not either. A release fence now sits before every avail index store (prime, refill, TX post) and an acquire fence after the used index is seen to move, the same pairing virtio-gpu already used. virtio-gpu had the acquire in the wrong place: after reading the used entry rather than before, so it ordered nothing the entry depended on. It moves ahead of the reads.
Both capsules re-ran their whole setup in a yield loop for ten seconds when no device matched, then exited 0. The broker is filled from PCI during kernel init, before the first capsule starts, so discovery gives the same answer on every pass; the loop only burned the CPU through that part of boot. On a PC, which has neither device, that was ten seconds of every boot. While virtio-net sat in it, net_core's link probes to driver.virtio_net0 went unanswered and each one waited out its timeout. A failed discovery now exits 2, as e1000, rtl8139 and rtl8169 do for an absent chip. The bounded retry stays for a device that is present and fails a later step. Booted with an e1000 on plain VGA, so with neither device present, both now leave with code 2 as they start and the desktop comes up on the GOP framebuffer. With no virtio-net present, net_core had logged "ipc.call unanswered driver.virtio_net0" five times in a boot; with this it logs it none.
…al, take short frames
The driver never answered the stack. It tagged replies with its own magic
(0x4E45_3130) and sent them to KERNEL_REPLY_ENDPOINT, an inbox nothing has read
since the stack moved into capsules. net_core and net_l2 speak NNET
(0x4E4E_4554) and wait for the answer to their own call, which is how
virtio-net replies. Requests are now taken with mk_ipc_recv_from and every
answer goes back to the capsule that asked, with mk_ipc_reply, under the
NNET tag. The ops and payload layouts already matched.
Booted as the only NIC, the e1000 came up and net_core's probe got nothing
("link probe driver.e1000_0 no-answer"). With this it binds and takes the
lease itself: "bind: interface up on driver.e1000_0", "lease 10.0.2.15/24 gw
10.0.2.2", and the mixnet directory fetch connects and handshakes over it as
it does over virtio-net.
TX posted every frame unconditionally and then spun on DD. When the spin ran
out the handler answered E_IO but left the descriptor live with TDT already
moved, and the next call wrote over the same slot without looking. On silicon
the 8254x sets no DD while the link is down (auto-negotiation after SLU, a
pulled cable, a blocking switch port), so every send timed out; after 31 of
them TDT caught up with TDH, which the part reads as an empty ring, and later
posts overwrote buffers it might still be fetching. A frame answered E_IO was
also still sent once the link came up, so a retry went out twice. QEMU's model
sets DD with the link down, which is why it never showed. TX now keeps a clean
index: reclaim walks it over finished descriptors, a ring with no free slot
answers E_AGAIN (one slot always stays empty), and a frame is answered once it
is queued.
The reset wrote CTRL and the receive address within microseconds of RST
clearing. A global reset starts an EEPROM auto-load that rewrites RAL0/RAH0 and
parts of CTRL, so the drawn station address could be replaced by the factory
one afterwards and unicast would go to the wrong filter. The sequence now
follows e1000_reset_hw: mask, stop RX and TX, wait 10 ms for bus-master cycles
in flight, reset, keep off the part for the first millisecond, poll RST clear
against a time bound rather than a spin count, then wait 20 ms for the
auto-load (5 ms on 82540/5/6, 20 on 82541/7) before anything is written.
Frames under 60 bytes were refused. TCTL.PSP has the part pad them, and ARP
(42) and a bare TCP ACK (54) are shorter than that, so IPv4 stopped right after
DHCP. A bare header is now the minimum.
The driver bound its INTx line and never used it: it polls and IMS is never
set. The discovery filter also skipped the NIC when firmware left Interrupt
Line at 0xFF, which UEFI commonly does, and a bound line is masked until acked,
so a shared GSI stayed masked for any other device on it. No line is bound
now, and the capsule gives up the Irq capability in its manifest and in the
kernel's spawn spec.
Release fences sit before the TDT and RDT writes and the ring hand-over, and an
acquire follows the DD reads, as in virtio-net.
e1000_proofs: 14 passed. The host shim gains Deadline, the fixture drops the
IRQ grant, and the request fixture carries the NNET tag. The no-entropy test
still holds the transmitter and receiver to never having been written, so
the quiesce writes TCTL as 0.
…the ring The driver never answered the stack. It tagged replies with its own magic (0x4E52_3839) and sent them to KERNEL_REPLY_ENDPOINT, an inbox nothing has read since the stack moved into capsules. net_core and net_l2 speak NNET (0x4E4E_4554) and wait for the answer to their own call, which is how virtio-net replies. Requests are now taken with mk_ipc_recv_from and every answer goes back to the capsule that asked, with mk_ipc_reply, under the NNET tag. The ops and payload layouts already matched. Discovery skipped any card whose PCI Interrupt Line read 0xFF. OVMF leaves it there, as UEFI firmware commonly does, so booted under OVMF with an RTL8139 as its only NIC the driver exited 2, absent. The line was only ever bound to be acked; the driver polls. It binds none now, sets IMR to 0 so an unserviced source cannot hold a shared INTx asserted for another device, and gives up the Irq capability. The station address was the factory one, read out of IDR: the identifier nonos_mac exists to keep off the wire, where e1000 and rtl8169 already drew theirs. It is now drawn through nonos_mac too, written as dwords with the config lock open as 8139too writes it, read back, and fails closed. The capsule gains Crypto, which CryptoRandom is gated on, in its manifest and in the kernel's spawn spec. Booted under OVMF as the only NIC, it now binds and takes the lease itself: "bind: interface up on driver.rtl8139_0", "lease 10.0.2.15/24 gw 10.0.2.2", and the mixnet directory fetch connects and handshakes over it. QEMU's `info network` shows the card at b6:54:0b:29:cc:83 rather than its configured 52:54:00:12:34:56, so the lease was taken under the drawn address. RCR set no RBLEN bits, so the chip used an 8K+16 ring while every offset here was taken against 32K. After about 8 KB received the chip wrote at the start of the ring and the driver read zeros at 8K: ROK clear, an error, and every later receive failed the same way. QEMU honours RBLEN too (8192 << RBLEN), so this was reachable in emulation. RBLEN is now 10, the 32K+16 ring the allocation was already sized for. With RCR.WRAP set, a frame that crosses the end of the ring is written on past it into the slack, not back at the start, but reads wrapped modulo the ring and took the tail of that frame from offset 0: stale bytes once a lap. Reads are linear now, and a read past the allocation returns zero. The ring proofs held the modulo behaviour; they now hold the linear one, over a buffer the size of the real allocation, and still check that no read leaves it. The chip does not pad short frames and frames under 60 bytes were refused, so ARP (42) and bare TCP ACKs (54) were never sent. A bare header is the minimum now and send zero-pads to 60. A bad header (ROK clear, or a length no good frame carries) returned without moving, so the same header was read forever. Receive now restarts from the top of the ring the way 8139too's rx_err does. A good frame too big for the caller (a tagged full-size one) is skipped instead of stalling, and 0xFFF0 (still arriving) is left for the next poll. TX walked TSD0-3 with a cursor that stayed put when a send failed, while the chip's own pointer moved on, so every later send waited on a descriptor the chip would never look at again. TX is now four slots with a cursor and a reclaim index, as 8139too keeps cur_tx and dirty_tx: a slot is finished on TOK, TUN or TABT, an abort writes TCR.CLRABT to restart the transmitter, a full ring answers E_AGAIN, and the early-TX threshold starts at 256 bytes rather than 8. Rx and Tx are enabled before RCR and TCR are written, as 8139too and the BSD drivers do. rtl8139_proofs: 7 passed.
The driver never answered the stack. It tagged replies with its own magic (0x4E52_3639) and sent them to KERNEL_REPLY_ENDPOINT, an inbox nothing has read since the stack moved into capsules. net_core and net_l2 speak NNET (0x4E4E_4554) and wait for the answer to their own call, which is how virtio-net replies. Requests are now taken with mk_ipc_recv_from and every answer goes back to the capsule that asked, with mk_ipc_reply, under the NNET tag. The ops and payload layouts already matched. It could not have come up on any card in any case. The station address is drawn with CryptoRandom, which is gated on the Crypto capability, and neither the manifest nor the kernel's spawn spec granted it: the draw failed closed and bring-up stopped with "no entropy for station address". Both grant it now, as they already did for e1000 and rtl8821ce. Discovery skipped any card whose PCI Interrupt Line read 0xFF, which is what UEFI firmware commonly leaves there, so on those PCs a present RTL8111/8168 was reported absent. The line was only ever bound to be acked; the driver polls. It binds none now, sets IMR to 0 so an unserviced source cannot hold a shared INTx asserted for another device, and gives up the Irq capability. The TX doorbell wrote TPPoll bit 7, which polls the high-priority ring. Only the normal-priority ring (TNPDS) is ever set up; THPDS is never written. On a real card the part fetched a descriptor from whatever THPDS held after reset, the real descriptor kept OWN, the first send timed out and every later one saw "busy". No frame was ever transmitted. The doorbell is bit 6, NPQ, as in Linux r8169. Both rings could fall a slot behind the part for good. On an RX descriptor error the slot was re-armed but the cursor stayed, while the part had already moved on; low-rate traffic like ARP then sat unread until fifteen more frames wrapped the ring. On TX the cursor moved only after a clean completion, so a TER or a slow completion (link still negotiating) left it on a slot the part had left. The RX cursor now advances past a bad descriptor, and the TX cursor advances the moment OWN is handed over; the OWN check on the next slot is the full-ring test, answered with E_AGAIN. The station address went into IDR with byte writes. The part takes IDR as dwords; byte writes are dropped on silicon, the readback check failed, and bring-up stopped there. It is now two 32-bit writes, high dword first, each read back to post it, as rtl_rar_set does. RxConfig and TxConfig were written with the receiver and transmitter off. On the 8169 and 8168B-F those writes can be lost and the accept bits never take. TE|RE now go on first, then the two configs, still after the station address, so the part is never enabled under the factory one (the bring-up proof that watches for that still passes). Frames under 60 bytes were refused. ARP (42) and a bare TCP ACK (54) are shorter than that; they are now zero-padded to 60, which also covers the 8168 revisions that pad short frames wrong. No QEMU model exists for this chip. rtl8169_proofs: 8 passed; the bring-up proof now holds IMR at 0.
"bind: interface up" did not say which interface. With a wired port and a WiFi link both present the choice is the first thing to know, and on a boot with one NIC it is what ties the lease that follows to a driver. The line now names the candidate, for example "bind: interface up on driver.e1000_0".
No profile carried e1000, rtl8139 or rtl8169, so none of them had ever been booted with the stack. This target is the desktop profile plus those three, under the same attestation. QEMU models the e1000 and the RTL8139, so each can be booted as the only NIC and has to take the lease itself; the RTL8169 has no QEMU model and shows that a driver whose chip is absent exits and the boot goes on.
…yout
Setup polled CSR_GP_CNTRL bit 1 for MAC clock ready. In the v1 CSR layout
that every family probed here uses, bit 1 is undefined and the flag is bit 0,
so the poll timed out on every card and the capsule exited before serving
anything. RF-kill was read from INIT_DONE, the bit setup had just set itself,
so the airplane-mode switch was never reported; it is HW_RF_KILL_SW, bit 27,
set while the radio is allowed on. Bz-family parts (BE200) use the v2 layout
and are still not handled.
The legacy firmware parser read the version at offset 8, which is the start of
the 64-byte name ("Core", "rele", "jenk" in the bundled images), so every image
was refused as an unknown API. The header is 88 bytes: version at 72, build at
76, TLVs from 88. The section types were one off (20/21/33): 19 is the runtime
image, 20 INIT, 32 paging, so the INIT and WoWLAN images were staged and the
runtime one never was. The gen3 path already had 19. The API ceiling moves to
86 to take the newest bundled image.
Checked against the six bundled .ucode files: the version at 72 is the API in
each file name (29, 36, 46, 77, 84, 86) and the TLV walk from 88 ends exactly
at the end of every file. The blob test written for this was never declared in
the proofs crate; it is wired in now and runs against the real 7265D-29 image
(four runtime sections, 364400 bytes). iwlwifi_proofs: 76 passed.
This gets the capsule past its first register and its firmware file. It does
not boot the firmware: the per-family load paths, the RX and TX queues and the
post-ALIVE command sequence are still to be written.
The GTK KDE in message 3 carries the key's index, and find_gtk threw it away. The driver then installed every group key in CAM slot 1. With the sec engine looking group-addressed frames up by the CCMP KeyID, that works until the AP rekeys: hostapd starts at 1 and swaps between 1 and 2 on every rekey, so after the first one every broadcast frame (ARP requests, DHCP, router adverts) came in under index 2, found an empty slot, and was dropped. The index now travels from the supplicant through the MLME and the join outcome to install_gtk and the session that removes it. TX data frames were also tagged SEC_TYPE_CCMP in the descriptor after the station had already encrypted them in software (header, CCMP header, MIC). rtw88 sets the security type only for frames with a hardware key; a frame tagged for hardware CCMP after software encryption risks being encrypted twice and failing the AP's MIC check. The tag is now zero. nonos_wifi_core_proofs gains a handshake test that drives the real supplicant with the KDE naming index 1, 2 and 3 (and with the Tx bit set) and holds it to the index sent: 14 passed. rtl8821ce_proofs does not build on main (sec.rs wants a crate::constants the proofs crate never declares, and its tests look for the firmware under the capsule directory rather than nonos-bootloader/firmware/realtek, where it is), so these edits are checked by the capsule build.
|
Reviewed at Verdict: Request changes. Two red lanes, both small, but one of them is a formal confinement proof that no longer holds over code this PR reworked — that should not merge without a sentence saying which side is wrong. The virtqueue ordering fix is the best thing in here
That is correct and it is the subtle part. The fix is the textbook pairing: let used = rx.used_idx();
if used == rx.last_used { return None; }
// The element and the frame are only valid once the index is seen.
fence(Ordering::Acquire);
let (desc_id, used_len) = rx.used_elem_at(ring_pos);The fence sits between observing the index and reading what the index publishes, which is the only placement that does anything. And it found the same mistake already shipped in virtio-gpu: "virtio-gpu had the acquire in the wrong place: after reading the used entry rather than before, so it ordered nothing the entry depended on." A fence that orders nothing is worse than no fence, because it reads as handled. The driver work around it is the same register-level care — Important1. Three Kani harnesses fail, and they are the ones this PR's ring rework should have updated.
All three live in They share one assumption, which is why I think this is a stale model rather than three unrelated regressions. assert!(out[i] == ring[(start + i) % RX_BUF_DATA_BYTES]);— that is, the copy wraps modulo the nominal ring size, and the two That is a guess, and it is the PR's to confirm rather than mine. What should not happen is this landing with a buffer-confinement proof red and no statement either way: if the model is stale, update the harnesses alongside 2. The stub ratchet has one new admission, and it wants a baseline decision.
The site is honest and specific — So the ratchet is doing its job: net Worth noting the ratchet is bidirectional on new sites only, so the two closures do not offset the addition. If that asymmetry is deliberate, fine; if the intent was a net-count ratchet, this PR is the case that shows it is not behaving that way. Minor
Questions
Verified correct
CI at this headTwo real failures. |
|
Superseded. This work is integrated into the 0.9.2 release and ships in the current tree. Closing as part of the 0.9.2 consolidation. |
2 participants
What was wrong
The zerostate image (
microkernel-full-gui) ships e1000, rtl8139, rtl8169, iwlwifi and rtl8821ce. None of the three wired drivers could carry traffic for the stack:link probe driver.e1000_0 no-answer.nonos_macexists to keep that address off the wire.On top of that, each driver had ring and descriptor bugs that only show on silicon; they are listed in its commit.
What changed
ENETUNREACH, notECONNREFUSED. The mixnet stays the only way out.nonos-mk-ethernet-prod: the desktop profile plus the three wired drivers.Evidence
Each boot runs
nonos-mk-ethernet-produnder QEMU q35 + OVMF with one NIC, so a lease can only have come through the driver named. The disk is openedsnapshot=on.link probe driver.e1000_0 no-answer, no lease[EXIT] code=2 driver.rtl8139_0(skipped: Interrupt Line 0xFF)bind: interface up on driver.e1000_0,lease 10.0.2.15/24 gw 10.0.2.2; mixnet directory fetch connects and handshakes over itbind: interface up on driver.rtl8139_0,lease 10.0.2.15/24 gw 10.0.2.2, handshake; QEMUinfo networkshowsb6:54:0b:29:cc:83(drawn), not52:54:00:12:34:56In every boot rtl8169 exits 2: QEMU has no model for it. After the handshake the directory sync fails with code 20 over every NIC. virtio-net fails the same way, so the cause is not these drivers.
Proofs: e1000_proofs 14, rtl8139_proofs 7, rtl8169_proofs 8, iwlwifi_proofs 76, nonos_wifi_core_proofs 14 passed.
Not done
src/hardware/{e1000,rtl8139,rtl8169}_capsule/clientstill speak the old per-driver magic. Nothing calls them.