mmap/munmap EL1 fastpath
The primary goal is to reduce VM exits for mmap and munmap.
Architecture
Anonymous mappings are lazy: sys_mmap only records the region; page-table creation, host memory commit, and zeroing of reused backing all happen at first touch.
Each vCPU owns a private contiguous virtual address arena. When the guest traps into EL1 for mmap/munmap, EL1 serves the request directly out of its own arena and never leaves EL1. The host's job is to keep those arenas supplied with VA and to reconcile their effects into host-side region/PTE state, both done lazily under mmap_lock rather than synchronously per call.
mmap fast path
EL1 serves exactly one shape:
mmap(NULL, len, PROT_READ|PROT_WRITE,
MAP_PRIVATE|MAP_ANONYMOUS[|MAP_NORESERVE], fd, off)
file-backed mapping is excluded. The reason is that EL1 is a freestanding, no-syscall context that cannot read a file or install a page-cache overlay itself — that work is inherently the host's.
The host prepares a contiguous VA region per vCPU. Each vCPU is the sole producer of its own 32-entry publication ring and bump cursor, and publishes the extent into its ring. The host installs the corresponding PTEs.
Arena refill is dynamic, not fixed-size. Any host path that already holds mmap_lock — a syscall, a page fault, or a natural VM exit — opportunistically tops up the current thread's arena once its remaining drops under that recent high-water mark. Arena exhaustion, an unsupported shape, a full ring, or a stale arena generation each bail to the ordinary host mmap slow path.
munmap fast path
EL1 validates that the target range belongs to a live arena, clears the covering page-table entries directly, and issues a broadcast TLBI, all without leaving EL1
The address is unusable to the guest the instant EL1 returns. Only after clearing the PTEs and completing the TLBI does EL1 publish a retirement record — address, length, and the arena generation it came from — to a second, separate 32-entry SPSC ring. The host has not been involved yet at that point; its bookkeeping is reconciled lazily by mmap_fastpath_drain_locked(), which walks every vCPU's retire ring and commits the deferred cleanup. That drain runs on every natural VM exit as well as on every syscall or fault that needs the lock.
Cross-thread ordering matters here, and A and B are often touching the same address, not two unrelated ones: EL1's fast munmap scans every vCPU's arena, not just its own, because handing a fresh allocation to another thread to free is the common case. If the host were to drain B's teardown of address X before it has drained A's publication of that same X, the removal would be a no-op (X isn't in the region table yet) and the publication drain right after would insert X as live — reviving, in host bookkeeping, an address EL1 already invalidated. The drain avoids this by snapshotting every vCPU's retire-ring tail first, draining every mmap publication next, and only then consuming retirements up to that snapshot, so within one drain pass a publication a retirement depends on is always applied before the retirement removes it:
vCPU A vCPU B
─────── ───────
mmap(len) -> X
EL1 bump-allocates X
ring.push(publish X) ──┐
│ guest hands X to B
│ (shared pointer / queue)
└──────────────────────┐
▼
munmap(X)
EL1 clears PTE(X), TLBI
retire.push(X, arena=A)
════════════════════ host: mmap_fastpath_drain_locked() ════════════════════
1. snapshot every retire-ring tail <- B's entry is already in view
2. drain ALL mmap publications <- installs A's region X
3. consume retirements up to that snapshot <- removes region X
region-table never shows X as live after EL1 has already invalidated it.
(wrong order, for contrast: consume B's retirement first -> no region X
exists yet, so removal is a no-op; drain A's publication after -> X gets
inserted and marked live, even though EL1 killed it already.)
EL1 self-throttles rather than pinging the host mid-flight. If a producer's retire ring is within one slot of full, munmap bails out of the fast path entirely and falls through to the ordinary syscall trap, which drains the ring as a side effect of taking mmap_lock. Separately, once a vCPU's own unconsumed retired bytes cross a 256 MiB soft threshold, it sets an advisory cleanup_requested flag; this never forces an HVC, it only marks that real cleanup work is waiting for the next natural drain.
behavior while fork
Before the fork snapshot is taken, the parent-side handler acquires mmap_lock through the fork variant of the acquire path, drains every vCPU's publication and retire ring, and waits for any in-flight lazy materialization to finish. It then revokes every per-vCPU arena descriptor. Because sibling vCPUs are already quiesced for the fork snapshot, this revocation cannot race a live EL1 producer.
The child does not inherit the parent's arena or ring layout. The child's main thread begins with a fresh, empty arena rather than a stale one aliased to the parent's.
Any clone() call that publishes a stack for the new thread goes through this too. Any anonymous fast-path allocation that has become a live thread stack must remain reachable only through the ordinary stack-lifetime bookkeeping, not through EL1's arena-generation check, so revoking first guarantees no later EL1 fast munmap can tear down a live stack range by still recognizing it as belonging to a live arena. Only a clone() with a null child_stack skips this.
behavior while exec
sys_execve() takes mmap_lock immediately before the point of no return. That both closes the EL1 producer gate and drains every vCPU's mmap and munmap rings, so g->regions[] and PTE state agree with each other before the address space they describe is destroyed. guest_reset() then zeroes the entire shim-data page, arena, both rings.
exec does not explicitly do arena's control block comes back. The replacement image's first eligible slow-path mmap by calling the refill path and turns the fast path back.
Frama-C proof coverage
The guest-influenced arena sizing and capacity arithmetic is pulled out of src/syscall/mem.c into src/proved/mmap-fastpath.h specifically so it can be proved.
Four functions are proved, every input treated as fully guest-influenced (request_len is the guest's own mmap length; the history window is built from a sequence of guest-chosen lengths), because a slip here either wedges the allocator by undersizing an arena forever, or lets mmap_fastpath_request_fits accept a request that runs past arena_limit:
mmap_fastpath_request_fits: whether alen-byte request still fits beforelimit, covering the zero-length, sub-block, and block-aligned cases. Proved to never answer "fits" when the aligned start would actually run pastlimit.mmap_fastpath_pow2_clamped: rounds a target size up to the nearest power of two inside[MIN, MAX].mmap_fastpath_window_max: the largest of the last 16 registered mapping sizes. Proved as an upper bound over the whole history window.mmap_fastpath_arena_size: the target arena size given recent history and the request about to be served. Proved to always land in[MIN, MAX], with-wp-rteseparately closing both multiplication-overflow guards and the division-by-zero case.
92 of 93 discharged goals (the 93rd, align_up_ok_ensures_rejects_only_on_wrap, is a pre-existing align.h goal that also fails standalone under make verify-align in this environment, not something this change introduced).
Benchmark results
A. One timed mmap/munmap fast-path pair per fresh process
All values are nanoseconds. Speedup is OrbStack / elfuse; values above 1
mean elfuse is faster.
| Size | elfuse mmap | OrbStack mmap | mmap speedup | elfuse munmap | OrbStack munmap | munmap speedup |
|---|---|---|---|---|---|---|
| 4 KiB | 50.8 | 266.7 | 5.25x | 47.1 | 268.8 | 5.71x |
| 16 KiB | 52.7 | 245.7 | 4.66x | 51.7 | 251.3 | 4.86x |
| 64 KiB | 51.4 | 281.3 | 5.47x | 51.4 | 294.1 | 5.72x |
| 256 KiB | 57.4 | 275.6 | 4.80x | 55.9 | 313.0 | 5.60x |
| 1 MiB | 54.7 | 259.3 | 4.74x | 54.3 | 359.5 | 6.62x |
| 2 MiB | 52.0 | 394.6 | 7.59x | 54.8 | 267.5 | 4.88x |
| 8 MiB | 52.4 | 256.6 | 4.90x | 52.4 | 282.4 | 5.39x |
| 64 MiB | 54.7 | 248.4 | 4.54x | 56.8 | 335.5 | 5.91x |
| 256 MiB | 63.7 | 313.7 | 4.92x | 57.1 | 574.8 | 10.07x |
| 1 GiB | 59.0 | 262.9 | 4.46x | 52.1 | 834.0 | 16.01x |
| 4 GiB | 59.2 | 273.5 | 4.62x | 53.2 | 904.9 | 17.01x |
| 16 GiB | 57.6 | 273.9 | 4.76x | 52.1 | 856.1 | 16.43x |
| 32 GiB | 60.7 | 250.5 | 4.13x | 54.0 | 973.4 | 18.03x |
B. munmap after materializing one 4 KiB page
Fifteen fresh processes are used per size. Values are outer medians of the
per-process medians.
| Size | elfuse | OrbStack | speedup |
|---|---|---|---|
| 4 KiB | 357.0 | 608.3 | 1.70x |
| 16 KiB | 442.1 | 568.3 | 1.29x |
| 64 KiB | 384.9 | 622.7 | 1.62x |
| 256 KiB | 388.3 | 621.0 | 1.60x |
| 1 MiB | 430.7 | 730.4 | 1.70x |
| 2 MiB | 430.7 | 1429.2 | 3.32x |
| 8 MiB | 422.8 | 1245.5 | 2.95x |
| 64 MiB | 397.9 | 1366.5 | 3.43x |
| 256 MiB | 400.3 | 1591.6 | 3.98x |
| 1 GiB | 441.1 | 2481.6 | 5.63x |
| 4 GiB | 409.7 | 2436.4 | 5.95x |
| 16 GiB | 298.3 | 2376.5 | 7.97x |
| 32 GiB | 295.7 | 2290.2 | 7.75x |
C. munmap after dirtying every 4 KiB page
One fresh process is used per size. Each process performs one warmup, then the
listed number of timed operations. The table reports the in-process
distribution.
| Size | elfuse p50 | elfuse p95 | elfuse max | OrbStack p50 | OrbStack p95 | OrbStack max | p50 speedup |
|---|---|---|---|---|---|---|---|
| 4 KiB | 241.3 | 532.9 | 6032.9 | 573.5 | 1031.9 | 6073.5 | 2.38x |
| 16 KiB | 324.6 | 616.3 | 10032.9 | 532.8 | 1976.5 | 8741.1 | 1.64x |
| 64 KiB | 282.9 | 532.9 | 8241.3 | 906.9 | 2142.3 | 17490.2 | 3.21x |
| 256 KiB | 282.9 | 574.6 | 8866.3 | 1948.4 | 3429.7 | 9448.4 | 6.89x |
| 1 MiB | 324.6 | 574.6 | 3491.3 | 5531.7 | 7152.6 | 19240.1 | 17.04x |
| 2 MiB | 282.9 | 532.9 | 7241.3 | 11052.6 | 15208.8 | 20156.7 | 39.07x |
| 8 MiB | 324.6 | 712.1 | 2032.9 | 51448.4 | 61521.3 | 65115.1 | 158.50x |
| 64 MiB | 657.7 | 1895.2 | 158116.0 | 423532.0 | 483825.7 | 676823.6 | 643.96x |
| 256 MiB | 1137.1 | 1395.4 | 1574.6 | 1812344.2 | 2048150.5 | 2105948.4 | 1593.83x |
| 1 GiB | 1523.0 | 3639.7 | 4106.3 | 7029220.3 | 7461557.8 | 7482907.8 | 4615.38x |
munmap latency has a step right at the 2 MiB boundary. Under 2 MiB, which walks and clears one 4 KiB L3 leaf at a time.
Arena size is clamped to MMAP_FAST_ARENA_MIN = 64 MiB and MMAP_FAST_ARENA_MAX = 32 GiB per vCPU.
tests/bench-mmap-isolated all to reproduce mmap/munmap-vs-size numbers
Closes #165
Summary by cubic
Adds lazy anonymous mappings and an EL1 fast path for common anonymous mmap/munmap calls, reducing VM exits and making large-range teardown length-independent. Guest-visible semantics stay unchanged; closes #165.
Behavior
- The fast path serves
mmap(NULL, len, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, ...)up to 32 GiB; unsupported shapes, exhausted arenas, and full rings fall back to the host syscall path. - Each vCPU owns a private arena refilled from recent mapping history and publishes changes through rings the host reconciles under
mmap_lock. - Host lock-taking paths drain every ring unconditionally; unrelated VM exits skip
mmap_lockwhen no ring has pending work. - Anonymous mappings are lazy: first touch creates page tables, commits host memory, and zeros reused backing; host-side access materializes untouched pages,
PROT_NONEreservations still fault, andmremappreserves neighboring PTEs across block boundaries. - EL1
munmapclears PTEs, broadcasts TLBI, advances the page-table epoch, and defers host bookkeeping until the next drain. - A hierarchical 2 MiB dirty-block index skips untouched ranges; released ranges recycle and empty arenas rewind.
- Fork drains and revokes arenas before snapshotting, the child starts fresh, and exec drains and resets them.
- Blocked-signal masks now publish with one atomic release for lock-free readers.
Compatibility
- Set
ELFUSE_MMAP_FASTPATH=0to disable; verbose tracing, syscall histograms, GDB, and Rosetta disable it automatically. - Fork IPC magic changes from
ELFQtoELFRbecause the wire payload includes the dirty-block snapshot.