A flashing route with no ELF to get wrong

1What the route is

The rule in the tree today makes a copy of the kernel ELF, gives its .apps section file content, and writes one application's TBF into it. The local-board route never opens an ELF. tockloader keeps a file that stands in for the board's flash; the kernel binary is written at the base of it and applications are installed into it at the application region, exactly as they would be onto a real board.

A fifth board is carried along without being edited. raspberry_pi_pico_w's Makefile is one line — include ../raspberry_pi_pico/Makefile — so it inherits whatever that file says. Splicing never had to care: objcopy wrote into the .apps section at whatever address the board's own ELF put it. Naming the address in the Makefile does have to care, and that board's layout.ld gives its kernel 576 K rather than 256 K, so its prog region begins at 0x10090000. Configured with 0x10040000 it would install applications on top of its own kernel. It sets APP_ADDRESS for itself, and make init there prints the higher address.

2Why the defect cannot occur here

#4770 is not really about the stack. It is about what objcopy does when a section acquires file content: it lays the program headers out again, and on the way through, the (NOLOAD) stack segment in SRAM comes back claiming file content it does not have. The section stays NOBITS the whole time, which is why nothing that reads the section table can see it.

That sequence needs an ELF to happen to. On this route the only objcopy in the chain is the kernel's own ELF-to-binary step, which the build already performs and which nothing here changes. There is no second copy, no section given contents, and no program header to recompute.

The three failure modes recorded on the #4770 page were checked against this route rather than assumed away. Two of them belong to the UF2 converters and cannot arise, because what they are handed is not an ELF. The third belonged to openocd, which used to write flash correctly, skip the SRAM segment with no flash bank found, and then fail its own verify_image against memory it had declined to write. The programming run in Section 3 emitted no such warning and verified clean, which is the observation rather than the argument.

3On silicon

The image was programmed onto a Pico 2 W over a Debug Probe, the board reset, and the console read. Two applications were used in turn: console, which prints a line and exits, and blink, which loops — so that the second run leaves a live process for the kernel to be asked about.

And two applications at once, which the route it replaces cannot do at all. --update-section .apps= takes one file. Two were installed into a 274,433-byte image — leak_claim at 0x10040080 and leak_observe at 0x10041080 — and the kernel listed both, loaded over SWD and again through the bootloader. One tockloader install --local-board carries both, its signature being [tab ...]: run with the two archives it reports a layout of leak_claim 4,096 bytes at 0x10040000 and leak_observe 8,192 bytes at 0x10041000, and the file it leaves is 274,433 bytes. That was read off the rule until 2026-09-09, when the call was made directly and the number came back the same. The two have to want different addresses: these are built for adjacent slots, and two applications compiled for the same one are refused with Could not meet fixed address requirements. That requirement comes from an optional TBF header, not from this route — process_binary.rs:231 only checks a fixed address when the application declares one.

And the empty case, which the rework created and nothing had tested. Collapsing program into flash means flash converts the image rather than the ELF, so with no application installed the board is handed a dense 262,144 bytes where the ELF was sparse. Run against an erased application region it boots and the process console answers list with its header row and nothing under it — which is two observations, not one: the kernel came up from the dense image, and an erased region really is empty rather than quietly holding something the loader would find.

The byte does the work, not the erase it triggers. That distinction looked unresolvable: the route writes the terminator through a programming path that erases the sector first, so the two always arrive together. They come apart on the bench, because NOR programming only clears bits and the terminator is 0x00 — nothing needs erasing to write it. With a ghost standing on the board, flash fillb 0x10041000 0x00 1 wrote that one byte and nothing else: a dump either side of it differs at exactly one position, the TBF version field going 02 to 00, with the header's size, checksum and name still intact. On the next reset the kernel listed one process where it had listed two. One byte, no erase, ghost gone.

The route does more than dodge the ELF defect — it closes a hazard the current one has. That took two measurements, and the first is about the kernel rather than about either route.

The loader stops at the first invalid header. It walks TBF headers from the start of the application region, and when one does not parse it gives up rather than scanning on. That was checked instead of assumed: a valid application placed one sector further along, with erased flash between, is never reached and never appears in the process list. So there is exactly one address at which an old application can come back — the slot immediately after the new image's last one.

tockloader writes a single zero byte at that slot. Splicing writes nothing there. That is the entire difference between the two routes on this point, and it is worth exactly one byte.

The ordinary case, for completeness. The A/B above is contrived on purpose — it puts an application exactly where the next one would start, because that is the only place a stale header can survive. The everyday version was run too: an 8,192-byte application flashed, then a 1,024-byte one over it with no erase in between. Only the second appears in the process list. That is the terminator doing its job without anyone arranging for it to matter.

What this retires. An earlier version of this page recommended padding the image across the whole application region. That rested on a wrong model of the loader — that it might scan past a gap — and it is unnecessary: the terminator already covers the only slot that can matter. Flashing a kernel on its own does leave applications in place, but that is Tock's ordinary behaviour and not a fault to be fixed here.

4The other half, byte for byte

The bootloader route was run — Section 3 — but a board booting is not the same as knowing what was written to it. So the UF2 was also taken apart and compared against the bytes that had just run over SWD.

5What it would cost

The four lines in #5156 buy a working make program and change nothing else. This route is better shaped, and it is not free.

The heaviest cost is the converter swap on the four RP2040 boards, so it was measured rather than estimated. It looks like a question about a chip — and there is no RP2040 to ask, nor an emulator: mainline QEMU has no such machine, and Tock's own emulated boards are RISC-V and x86. But it is really a question about two programs, and both are here.

6Choosing between this and #5156

Both fix #4770 on the same five boards — four Makefiles in #5156's case, because raspberry_pi_pico_w includes another board's. They are not alternatives in the sense of one being right — they are different sizes of change with different evidence behind them, and the order they land in costs nothing either way.

#5158 went first, and the collision cost one line. That pull request was two commits: one renamed a make target in two RP2 READMEs, and one said in the ADC syscall document that samples are left-justified. It merged on 2026-09-09, and this change was rebased onto it the same day. Both conflicts were the same shape — #5158's corrected make program against the tockloader install lines that replace the whole block — and both resolved by keeping the replacement. The ADC commit is untouched. This is what the queue's dependency arrows are for: the hold was recorded before either landed, and the resolution was a rebase rather than a surprise.

7What this does not establish

This list was longer, and every entry that came off it came off by going back to the board rather than by arguing about it: a UF2 written through the bootloader, two applications installed at once, an A/B rebuilt from real applications instead of a patched copy, and — after the rework introduced it — a kernel-only image, which the collapse of program into flash made a new and untested case. What follows is what nothing here could close.

• Nothing ran on an RP2040. There is no such board here and no emulator for it — mainline QEMU has no RP2040 machine, and Tock's own emulated boards are RISC-V and x86. The image assembles, begins with that board's own kernel binary byte for byte, and converts to the right family with a valid TBF header at the application address — but nothing was booted from it. make init and make flash do run end to end on raspberry_pi_pico, with tockloader 1.18.1 and picotool doing the work, so what is untested is the boot and not the rules. Figure 5 argues it would behave as it does today; it does not observe it.
• probe-rs ran, but not against the chip the rule names. The invocation in Figure 2 used --chip RP235x, because that is the board here. flash-probe on the RP2040 boards passes --chip rp2040, and that argument was never exercised. The flags around it were.
• The stale-slot A/B was run over SWD only. A UF2 was written through the bootloader in Section 3, but not as an arm of that comparison. The bootloader erases a sector before writing into it, so the same reasoning should hold; it was not observed.