mmap/munmap EL1 fastpath

.ci/check-matrix-lists.sh

@@ -70,6 +70,7 @@ test-shim-urandom-wrap
 test-shim-futex-toctou
 test-ptrace-interrupt
 test-shim-cred-race
+test-mmap-fastpath
 test-mremap-infra
 test-mremap-fork-tracking
 test-dev-shm-paths

Makefile

@@ -142,6 +142,10 @@ $(ELFUSE_BIN): $(OBJS) | $(BUILD_DIR)
 
 # Native test binaries (macOS, Hypervisor.framework)
 
+$(BUILD_DIR)/test-materialize-host: $(BUILD_DIR)/test-materialize-host.o \
+        $(filter-out $(BUILD_DIR)/main.o,$(OBJS)) | $(BUILD_DIR)
+	$(call link-and-sign,$@,$^)
+
 ## Build the multi-vCPU HVF validation test (native macOS binary)
 $(BUILD_DIR)/test-multi-vcpu: $(BUILD_DIR)/test-multi-vcpu.o | $(BUILD_DIR)
 	$(call link-and-sign,$@,$<)
@@ -429,6 +433,33 @@ $(BUILD_DIR)/test-sigsuspend: tests/test-sigsuspend.c | $(BUILD_DIR)
 	@echo "  CROSS   $< (with -lpthread)"
 	$(Q)$(CROSS_COMPILE)gcc $(CROSS_TEST_CFLAGS) -Itests -o $@ $< -lpthread
 
+# bench-mmap has a multi-threaded mmap_lock-contention section; needs -lpthread.
+$(BUILD_DIR)/bench-mmap: tests/bench-mmap.c | $(BUILD_DIR)
+	@echo "  CROSS   $< (with -lpthread)"
+	$(Q)$(CROSS_COMPILE)gcc $(CROSS_TEST_CFLAGS) -o $@ $< -lpthread
+
+# test-mmap-lazy races concurrent first touch from several threads.
+$(BUILD_DIR)/test-mmap-lazy: tests/test-mmap-lazy.c | $(BUILD_DIR)
+	@echo "  CROSS   $< (with -lpthread)"
+	$(Q)$(CROSS_COMPILE)gcc $(CROSS_TEST_CFLAGS) -o $@ $< -lpthread
+
+.PHONY: test-mmap-lazy
+test-mmap-lazy: $(ELFUSE_BIN) $(BUILD_DIR)/test-mmap-lazy
+	@$(ELFUSE_BIN) $(BUILD_DIR)/test-mmap-lazy
+	@sh tests/test-mmap-dirty-stats.sh $(ELFUSE_BIN) \
+		$(BUILD_DIR)/test-mmap-lazy
+
+# EL1 consumer-mmap integration/stress test.
+$(BUILD_DIR)/test-mmap-fastpath: tests/test-mmap-fastpath.c | $(BUILD_DIR)
+	@echo "  CROSS   $< (with -lpthread)"
+	$(Q)$(CROSS_COMPILE)gcc $(CROSS_TEST_CFLAGS) -o $@ $< -lpthread
+
+.PHONY: test-mmap-fastpath
+test-mmap-fastpath: $(ELFUSE_BIN) $(BUILD_DIR)/test-mmap-fastpath
+	@$(ELFUSE_BIN) $(BUILD_DIR)/test-mmap-fastpath
+	@sh tests/test-mmap-fastpath-stats.sh $(ELFUSE_BIN) \
+		$(BUILD_DIR)/test-mmap-fastpath
+
 # test-thread-churn creates >64 threads to force thread-table slot reuse.
 $(BUILD_DIR)/test-thread-churn: tests/test-thread-churn.c | $(BUILD_DIR)
 	@echo "  CROSS   $< (with -lpthread)"

docs/internals.md

@@ -526,6 +526,14 @@ goes above the structured area, never below. Post-push masking
 
 ### `mmap` Notes
 
+Private anonymous mappings are lazy at 2 MiB materialization granularity. A
+host-side hierarchical bitmap records which low-VA 2 MiB blocks contain any
+valid TTBR0 PTE, independently of the dirty-block bitmap. `munmap` and recycled
+fast-path arenas use this index to visit only materialized blocks, so untouched
+multi-GiB reservations have length-independent teardown. When every mapping in
+a per-vCPU arena has been released and the index confirms that no PTE remains,
+the arena cursor rewinds in place instead of taking a refill HVC.
+
 Aligned file-backed `MAP_SHARED` (fixed or non-fixed) installs a real
 host `mmap(MAP_FIXED|MAP_SHARED, fd)` overlay onto the guest slab so
 the kernel page cache keeps the mapping coherent with the file (and

docs/usage.md

@@ -93,6 +93,16 @@ host `KEY=` imports as `KEY=`. An empty variable name is rejected. Given neither
 `--env` nor `--clear-env`, the guest inherits the host environment unchanged.
 `--clear-env` starts from nothing, leaving only what `--env` puts back.
 
+### mmap call fast path
+
+The aarch64 EL1 consumer fast path is enabled by default for
+`mmap(NULL, len, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS, ...)` up to
+32 GiB per request.
+Set `ELFUSE_MMAP_FASTPATH=0` to disable it. Unsupported mmap shapes, exhausted
+arenas, and full consumption rings fall back to the normal host syscall path.
+Verbose tracing, the syscall histogram, GDB, and Rosetta keep mmap on the host
+path so observability and translated-guest behavior are unchanged.
+
 ## Common Launch Patterns
 
 Run a statically linked guest binary:

mk/shim.mk

@@ -1,11 +1,33 @@
-# EL1 kernel shim assembly pipeline
+# EL1 kernel shim pipeline
 #
-# shim.S -> shim.o -> shim.bin -> shim_blob.h (C byte array)
+# shim.S + freestanding shim-mmap.c -> shim.o -> shim.bin -> shim_blob.h
 
-$(BUILD_DIR)/shim.o: src/core/shim.S | $(BUILD_DIR)
+# Disable RCpc codegen so acquire loads remain cumulative LDARs.  The retire
+# snapshot rule carries cross-vCPU causality through different atomic words;
+# LDAPR is intentionally too weak for that protocol.
+SHIM_CFLAGS := -O2 -Wall -Wextra -Wpedantic -Wshadow \
+	-Wstrict-prototypes -Wmissing-prototypes -Wformat=2 \
+	-Wimplicit-fallthrough -Wundef -Wnull-dereference \
+	-Wno-unused-parameter -ffreestanding -fno-builtin \
+	-fno-stack-protector -fno-unwind-tables \
+	-fno-asynchronous-unwind-tables -mno-outline-atomics \
+	-Xclang -target-feature -Xclang -rcpc
+SHIM_LD ?= ld
+
+$(BUILD_DIR)/shim-asm.o: src/core/shim.S | $(BUILD_DIR)
 	@echo "  AS      $<"
 	$(Q)$(SHIM_AS) $(SHIM_ASFLAGS) -o $@ $<
 
+$(BUILD_DIR)/shim-mmap.o: src/core/shim-mmap.c src/core/shim-mmap.h \
+		src/core/mmap-fastpath.h src/core/shim-globals.h | $(BUILD_DIR)
+	@echo "  CC      $<"
+	$(Q)$(CC) $(SHIM_CFLAGS) -MMD -MP -MF $(BUILD_DIR)/shim-mmap.d \
+		-Isrc -c -o $@ $<
+
+$(BUILD_DIR)/shim.o: $(BUILD_DIR)/shim-asm.o $(BUILD_DIR)/shim-mmap.o
+	@echo "  LD      $@"
+	$(Q)$(SHIM_LD) -static -arch arm64 -e _start -o $@ $^
+
 $(BUILD_DIR)/shim.bin: $(BUILD_DIR)/shim.o
 	@echo "  OBJCOPY $@"
 	$(Q)$(OBJCOPY) -O binary $< $@

mk/tests.mk

@@ -300,6 +300,7 @@ check: $(ELFUSE_BIN) $(TEST_DEPS) check-syscall-coverage check-eintr-contract ch
 	$(call run-lane,test-shebang-host,shebang parser unit test)
 	$(call run-lane,test-shim-futex-stats,futex EL1 fast path is live)
 	$(call run-lane,test-gva-contracts,proved/gva.h call-site contract checks)
+	$(call run-lane,test-materialize-host,lazy materialization and signal-frame boundaries)
 	$(call run-lane,test-proctitle-host,proctitle argv-tail regression)
 	$(call run-lane,test-proctitle-low-stack,proctitle low-stack regression)
 	$(call run-lane,test-busybox,busybox applet validation)
@@ -1366,6 +1367,10 @@ test-shim-futex-stats: $(ELFUSE_BIN) $(TEST_DIR)/test-shim-futex-fast \
 		$(TEST_DIR)/test-shim-futex-fast \
 		$(TEST_DIR)/test-futex-wake-nowaiter
 
+.PHONY: test-materialize-host
+test-materialize-host: $(BUILD_DIR)/test-materialize-host
+	@$(BUILD_DIR)/test-materialize-host
+
 ## Run busybox applet smoke tests
 test-busybox: $(ELFUSE_BIN) $(BUSYBOX_DEPS)
 	@if [ ! -x "$(BUSYBOX_BIN)" ]; then \

mk/verify.mk

@@ -390,6 +390,35 @@ VERIFY_FUTEXOP_MODEL := typed
 VERIFY_FUTEXOP_SCAN := src/proved/futexop.h
 VERIFY_FUTEXOP_CLAIM := for ANY guest-supplied val3 word
 VERIFY_FUTEXOP_UNPROVED := the wake and requeue walks around them stay test-covered
+# Includes align.h: request_fits calls align_up_ok and window_fits, so this
+# proof must discharge their contracts too, not merely assume them, the same
+# reason VERIFY_ELF appends VERIFY_UTILS_FCTS.
+#
+# MIN_GOALS is the complete count from a real run. Keep the floor at that count
+# so a future edit that quietly drops a contract or a runtime-error obligation
+# cannot turn a smaller proof into a pass.
+#
+# mmap_fastpath_pow2_clamped was originally the classic bit-smear
+# round-up-to-power-of-two; that form's bound and power-of-two properties
+# were confirmed unreachable by these provers (a single OR step already
+# times out), the same wall align_up_ok's own history describes one level
+# down. Rewritten to a doubling loop with an axiomatized power-of-two ghost
+# invariant -- same inputs, same outputs, linear arithmetic instead of
+# bitwise -- and it discharges completely; see the comment above it.
+VERIFY_MMAPFASTPATH_SRC  := src/proved/mmap-fastpath.h
+VERIFY_MMAPFASTPATH_FCTS := mmap_fastpath_request_fits mmap_fastpath_pow2_clamped \
+                            mmap_fastpath_window_max mmap_fastpath_arena_size \
+                            align_up_ok window_fits
+VERIFY_MMAPFASTPATH_MIN_GOALS ?= 93
+VERIFY_MMAPFASTPATH_MODEL := typed
+VERIFY_MMAPFASTPATH_SCAN := src/proved/mmap-fastpath.h src/proved/align.h
+VERIFY_MMAPFASTPATH_CLAIM := for ANY cursor/limit/len and ANY registration history
+VERIFY_MMAPFASTPATH_UNPROVED := mmap_fastpath_window_max reporting an actual array member \
+                                 rather than just an upper bound (the loop-invariant \
+                                 preservation step for that claim times out even with a \
+                                 ghost witness index, confirmed unreachable, see the comment \
+                                 above it); the atomic control-block bookkeeping around all \
+                                 four stays test-covered
 
 VERIFY_PATHDEPTH_SRC  := src/proved/pathdepth.h
 VERIFY_PATHDEPTH_FCTS := path_depth_push path_depth_pop

scripts/check-mutants.py

@@ -247,6 +247,41 @@ def _load(stem, name):
         "    return start <= limit && length <= limit - start;",
         "    return start <= limit && length <= limit - start + 1;",
     ),
+    # ---- verify-mmapfastpath ----------------------------------------------
+    (
+        "mmapfastpath",
+        "src/proved/mmap-fastpath.h",
+        "mmap_fastpath_request_fits",
+        "accept every non-empty request (an allocation can pass the limit)",
+        "    return window_fits(start, len, limit);",
+        "    return true;",
+    ),
+    (
+        "mmapfastpath",
+        "src/proved/mmap-fastpath.h",
+        "mmap_fastpath_pow2_clamped",
+        "clamp an oversized arena request to the lower bound",
+        "    if (value >= MMAP_FAST_ARENA_MAX)\n"
+        "        return MMAP_FAST_ARENA_MAX;",
+        "    if (value >= MMAP_FAST_ARENA_MAX)\n"
+        "        return MMAP_FAST_ARENA_MIN;",
+    ),
+    (
+        "mmapfastpath",
+        "src/proved/mmap-fastpath.h",
+        "mmap_fastpath_window_max",
+        "discard a new maximum (the arena can be undersized)",
+        "        if (window[i] > max)\n            max = window[i];",
+        "        if (window[i] > max)\n            max = 0;",
+    ),
+    (
+        "mmapfastpath",
+        "src/proved/mmap-fastpath.h",
+        "mmap_fastpath_arena_size",
+        "return an arena size above the configured maximum",
+        "    return adaptive > covering ? adaptive : covering;",
+        "    return UINT64_MAX;",
+    ),
     # ---- verify-cmsg -------------------------------------------------------
     (
         "cmsg",

src/core/bootstrap.c

@@ -37,6 +37,7 @@
 #include "syscall/signal.h"
 
 #include "debug/log.h"
+#include "core/mmap-fastpath.h"
 
 /* Worst case: 7 fixed regions (shim, shim-data, vDSO, brk, stack, mmap RX, mmap
  * RW) plus up to ELF_MAX_SEGMENTS for both the executable and the interpreter.
@@ -138,6 +139,26 @@ static void register_runtime_regions(guest_t *g, size_t shim_bin_len)
     guest_invalidate_ptes(g, 0, 0x1000);
 }
 
+/* ELF/shim/stack bytes are populated directly in the slab before their page
+ * tables become live. Mark their semantic backing regardless of requested
+ * permissions: a read-only file segment is still nonzero and must be scrubbed
+ * if a later MAP_FIXED lazy-anonymous mapping reuses the same slab block.
+ * Synthetic page-table coverage for unallocated mmap space has no semantic
+ * region and therefore remains clean.
+ */
+static void mark_registered_backing_dirty(guest_t *g)
+{
+    for (int i = 0; i < g->nregions; i++) {
+        const guest_region_t *r = &g->regions[i];
+        if (r->end <= r->start)
+            continue;
+        uint64_t len = r->end - r->start;
+        if (r->gpa_base > g->guest_size || len > g->guest_size - r->gpa_base)
+            continue;
+        guest_dirty_mark_range(g, r->gpa_base, r->gpa_base + len);
+    }
+}
+
 int guest_bootstrap_probe_elf(const char *elf_path, elf_info_t *info)
 {
     memset(info, 0, sizeof(*info));
@@ -302,7 +323,15 @@ static bool build_boot_regions(mem_region_t *regions,
      * to the vDSO page when splitting the block; otherwise vdso_build cannot
      * write into it through guest_ptr.
      */
-    if (!append_boot_region(regions, nregions, g->shim_base,
+
+    /* EL1 fast munmap walks and atomically clears the live TTBR0 tree. Give the
+     * page-table pool an identity VA visible only to EL1; EL0 remains unable to
+     * inspect or corrupt descriptors, and every guest syscall still rejects the
+     * encompassing infrastructure range.
+     */
+    if (!append_boot_region(regions, nregions, g->pt_pool_base, g->pt_pool_end,
+                            MEM_PERM_RW_EL1_ONLY) ||
+        !append_boot_region(regions, nregions, g->shim_base,
                             g->shim_base + shim_bin_len, MEM_PERM_RX) ||
 
         /* shim_data is EL1-only: the guest must not directly read or write the
@@ -568,6 +597,7 @@ int guest_bootstrap_prepare(guest_t *g,
     }
 
     register_runtime_regions(g, shim_bin_len);
+    mark_registered_backing_dirty(g);
     startup_trace_step("register_regions", t0);
 
     log_debug("TTBR0=0x%llx, IPA base=0x%llx", (unsigned long long) boot->ttbr0,
@@ -761,6 +791,13 @@ int guest_bootstrap_create_vcpu(guest_t *g,
      */
     shim_globals_set_singleton(g);
 
+    /* Publish the main vCPU's first arena only after shim_globals_init has
+     * cleared every recycled control slot. Verbose tracing keeps all shim
+     * syscall fast paths on HVC so the trace remains complete.
+     */
+    if (!verbose)
+        mmap_fastpath_prepare_vcpu(g, current_thread);
+
     HV_CHECK(hv_vcpu_set_sys_reg(vcpu, HV_SYS_REG_CNTKCTL_EL1,
                                  CNTKCTL_EL1_EL0_TIMER_EN));
 
@@ -869,6 +906,7 @@ int guest_bootstrap_rosetta_post_reset(guest_t *g,
                                  g->rosetta_guest_base - g->rosetta_va_base,
                                  ROSETTA_PATH);
     register_runtime_regions(g, shim_bin_len);
+    mark_registered_backing_dirty(g);
 
     int rosetta_argc = 0;
     const char **rosetta_argv = NULL;