Conversation
The kernel demand-filled any user page a thread touched first, foreign guests included. A Linux guest's PROT_NONE reservation read as zeros, and a pthread's guard page, which musl leaves as the unopened bottom of a PROT_NONE stack reservation, took a fresh page and guarded nothing: a recursion ran straight through it. Every page a Linux guest is meant to have is already mapped by its supervisor with MkPeerMap: brk, the initial stack, the ELF segments, file maps, anonymous maps and mprotect commits. Demand fill only ever gave a guest pages nobody had mapped for it. Now a not-present fault in a foreign guest is refused. The fault path ends the thread with -11, the kernel posts the death to the supervisor as before, and the personality ends the process with status 139. The page tables stay the one record of what a guest holds; nothing new is kept in the kernel. guardpage, a musl pthread recursing into its guard page, proves it: the process ends on SIGSEGV with status 139 and never prints the line it prints when it runs 64 KiB below the stack.
The peer protection bits had write and exec and nothing for no access: MkPeerMap and MkPeerProtect with neither bit gave a present, readable user page. So mprotect(PROT_NONE) on a mapped span, and a PROT_NONE file mapping, left the pages readable, and the region list had no way to say a backed span was closed. MkPeerMap and MkPeerProtect now take PEER_PROT_NONE. The page stays present with the user bit clear: every guest access faults, the kernel still copies it at fork and frees it at teardown, and the bytes are there again when a later mprotect opens it, as Linux keeps them. A region records whether it allows access at all, and one function turns a region's protection into peer bits for map, commit, mprotect and the fork copy. protnone proves it part by part in forked children.
mprotect changed the page protection of a backed span in the kernel but left the region list with the protection the span was mapped with. Fork maps the child from that list, so after mprotect RW to R, or RW to PROT_NONE, the child got the span read-write: a write the parent could not make succeeded in the child. Every protection change on a backed span goes through protect_span, and protect_span now records the new write, exec and access on exactly the part it changed, splitting the region around it and keeping whether the bytes were proved. Fork maps the child with what the parent has now. protfork proves it: RW to R, RW to PROT_NONE, RW to R to RW, and one page closed in the middle of three, each checked in a forked child.
A MAP_FIXED mmap over pages the guest already had kept them: MkPeerMap skips a page that is present, so the old bytes and the old protection stayed, and the region list held the old span and the new one on top of each other. A program that wrote a page, mapped PROT_NONE over it with MAP_FIXED and opened it again read its old bytes, where Linux gives zeroes, and fork copied the doubled span twice. MAP_FIXED now unmaps the target span just before the new pages go in, as Linux replaces a mapping. It is done after every refusal the mapping can meet, so a refused mapping leaves the old one in place. touchfork proves it with the reservation cases around it: bytes written into an opened part of a reservation reach a forked child, still do after the part is closed and opened again in the child, a page never opened faults in the child, and MAP_FIXED PROT_NONE over a written page reads zero once opened.
mmap took any nonzero address as fixed, hint or not, and the mapping cursor took the next address above the last mapping it chose without looking at what the guest had mapped there itself. Either way a new mapping could land on an old one: MkPeerMap skips a present page, so the guest got the old bytes back as its new, zeroed mapping, and the region list held both. MAP_FIXED_NOREPLACE was taken as a hint and mapped over whatever was there. Placement now follows Linux. MAP_FIXED is the exact address; MAP_FIXED_NOREPLACE is the exact address or EEXIST when anything is there; any other address is a hint, rounded up to a page and used only when nothing is there. Otherwise the cursor chooses and skips every span the guest holds, and moves past a mapping only when it chose it.
brk mapped from the old break itself, which is rarely page aligned, so every call that grew the break pushed a second region for the page the break already sat in, and fork copied that page once per call. A lower break only moved the number: the pages above it stayed mapped, and growing again handed back the old bytes where Linux gives zeroes. And a break that grew into a mapping the guest had placed in the heap area with MAP_FIXED mapped over it. The break now grows from the page above the old one, is refused, as Linux refuses it, when that span meets a mapping, and a lower break unmaps the whole pages above it.
mremap gave the part it grew read-write whatever the mapping was, so a PROT_NONE or read-only mapping grew a writable tail. A move read the old bytes and failed with EFAULT on a reservation, which has none; restored only read-only or read-write on the copy, so a PROT_NONE mapping came back readable; left the new span mapped when the copy failed; and dropped the mark that the bytes came from a file nothing proved, so the moved copy could then be made executable with mprotect, past the check that refuses it where the file was mapped. It also accepted an old span running across mappings with different protections. The grown part and the moved copy are now held like the mapping they came from: its protection, its backing and its provenance. A reservation grows or moves as a reservation with no bytes to copy. A move that fails unmaps what it made. An old span that is not one mapping is refused with EFAULT, as Linux refuses it. The move goes to a free span found the same way mmap finds one.
munmap and mprotect rounded an address that was not on a page boundary down to one, and so acted on bytes below the address the guest named. mmap did the same for a MAP_FIXED address, and took a file offset that was not on a page boundary. Linux answers all four with EINVAL. They now answer EINVAL. Only a length is rounded, and a hint address without MAP_FIXED, as on Linux.
A guest calling mlock, mlock2, munlock, mlockall, munlockall, msync or mincore got an unserved line and ENOSYS, where Linux answers each. In this memory model every page a guest holds is resident from the commit that maps it until it is unmapped, and nothing is paged out. So the lock calls have nothing left to do but Linux's argument checks: the span must be held (ENOMEM), the flags known (EINVAL), and RLIMIT_MEMLOCK is already reported unlimited. Every file mapping is private, since MAP_SHARED of a file is refused, so msync has nothing to write back and answers its checks alone, ENOMEM for a span with a hole included. mincore answers from the region list, one byte per page: 1 for a backed page, whatever its protection, and 0 for a reservation page, which has no frame. memcalls proves these and the placement, brk, alignment and mremap changes before it, one line per part.
With the gopoll, gopreempt and cwait guests enrolled beside the five memory proof guests, the guest-test store no longer loaded: nonos-store-pack counted 18039927 payload bytes against the vfs budget of 16777216 and refused it, so no guest could boot. Each guest in the store is its binary plus its certificate, manifest and a 327 KiB proof trailer, and the five memory guests came to 1907576 bytes of it, 1683520 of them proofs. The five proofs are now one program, memproof, whose first argument names the proof: guardpage, protnone, protfork, touchfork or memcalls. Each proof keeps its own file and is built with its main renamed, so it runs exactly as it did as a program of its own. memcalls maps its own file for the provenance part, which is now /bin/memproof. The ids 4982 to 4989 are free again.
Nine files this branch touches ran past 75 lines, from 76 for map.rs to 224 for memcalls.c, and the comments added in the kernel, personality and guest files were written with // where the rule is /* */. Each long file is split along a line it already had: the three refusals of a demand fill go to faults/demand_refuse.rs; perms_of moves into peer_protect.rs; reserve and map_span leave mem_map.rs; the mprotect walk, the mremap one-mapping check, the mmap kind and the cursor search each get a file. The memory proofs share one file for printing, running a part in a child and counting, and memcalls is split by call family. call/mod.rs is back to its own export line and makes mem public, so the lock, msync and mincore calls are named call::mem::... in the table. No behaviour changes.
eKisNonos
force-pushed
the
linux/guest-memory
branch
from
September 29, 2026 09:13
3551d22 to
a42cf1f
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This makes a Linux guest's memory behave the way Linux says it should. Until now the kernel filled any page a guest touched for the first time, so a PROT_NONE reservation read back as zeros and a pthread's guard page stopped nothing. mprotect(PROT_NONE) on a mapped page left it readable, a fork after mprotect gave the child the old protection, MAP_FIXED kept the pages it landed on, and mlock, msync and mincore weren't served at all.
This branch sits on top of linux/go-guests and should be merged after it. Against that base it is 11 commits.
How it works
The kernel no longer fills a page for a foreign guest on its own. Every page a guest is supposed to have (brk, the initial stack, ELF segments, file maps, anonymous maps, mprotect commits, mremap) was already mapped up front by the personality through MkPeerMap. So demand fill only ever handed a guest pages nobody had given it. Now a fault on such a page takes the normal user fault path: the thread dies, the supervisor gets the death notice, and the personality ends the process with 139. The kernel reports and the personality decides.
I looked at two other ways to do it: keeping a list of committed ranges in the kernel, or a per-guest fill policy. Both need a new syscall and new kernel state, and a range list would be a second copy of what the page tables already say. It would also have put lazily filled guest pages under the 16 MiB demand budget in demand_cap.rs, which a Go heap outgrows. The change I made is one check, in faults/demand_refuse.rs.
PROT_NONE on a page that is already mapped needed a way to say "no access", and the peer protection bits only had write and exec. There is now a PEER_PROT_NONE bit for MkPeerMap and MkPeerProtect; no new syscall. x86_64 has no present-but-no-access user page, so the page stays present with the user bit cleared. Any guest access faults, the bytes stay put for a later mprotect that opens the page again, fork can still copy it (MkPeerCopy doesn't look at the user bit), and teardown frees it like any other page. usercopy does require the user bit, so no native syscall can read or write such a page.
Commits
The memproof commit is there because the guest test store has a 16777216 byte load budget. With five separate proof guests next to the ones already enrolled it came to 18039927 bytes and wouldn't load. As one guest it's 16565760 bytes.
What I found in munmap, mremap, brk and mmap
While in there I went through the other memory calls looking for the same kind of bug: pages left mapped, a region list that disagrees with the page tables, or a move that doesn't unmap.
mlock, munlock, mlockall, munlockall, msync and mincore are served now. Every page a guest holds is resident from the moment it's mapped and nothing is ever paged out, so the lock calls only need Linux's argument checks. msync has nothing to write back because every file mapping here is private. mincore answers from the region list.
Testing
Everything below was built and booted on the tree at a42cf1f (q35 under TCG, one vCPU). The kernel builds with 43 warnings, same as the base, and the personality with none. No boot had a triple fault or a reset, none logged a demand fill, and every guest finished with 0 unserved calls.
The proofs are one guest, /bin/memproof, run with the proof's name as its argument. I ran each one on host Linux first as the reference.
The existing guests all still pass: gohello (293 calls), goconc (250), cthreads (87), threadfault (death line and exit 139, 7 calls), gopoll (3 parts in 3434 ms, 371 calls) and cwait (16 parts in 2291 ms, 345 calls).
For the negative controls I removed each change with a small sed, rebuilt, booted, and restored it afterwards. That took four builds, each removal breaking only its own parts:
The repo gates show nothing new (check_unreachable still lists the known has_children). Every one of the 11 commits passes cargo check for the kernel and the personality on its own, and the head was built in full and booted.
Kernel segments
This changes the kernel, so here are the x86_64 PT_LOAD segments. I built the same tree with the kernel files put back as they are on linux/go-guests (before) and as they are here (after). Two builds of "after" came out identical.
This needs your sign-off.
Not done here