Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 27 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -311,6 +311,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 -D_GNU_SOURCE -static -O2 -o $@ $< -lpthread

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P3: The three new explicit cross-test rules hardcode -D_GNU_SOURCE -static -O2 and drop the -MMD -MP header-dependency flags that every sibling rule gets via $(CROSS_TEST_CFLAGS). Because these explicit rules override the $(BUILD_DIR)/%: tests/%.c pattern rule, no .d file is emitted, so editing tests/test-harness.h (included by both test-mmap-lazy.c and test-mmap-fastpath.c) will no longer rebuild these binaries. This breaks the exact guarantee the pattern-rule comment states: "-MMD tracks the shared test headers, so editing one rebuilds every guest binary that includes it." Use $(CROSS_TEST_CFLAGS) like the neighboring rules so header changes rebuild these tests.

Prompt for AI agents
Check if this issue is valid — if so, understand the root cause and fix it. At Makefile, line 317:

<comment>The three new explicit cross-test rules hardcode `-D_GNU_SOURCE -static -O2` and drop the `-MMD -MP` header-dependency flags that every sibling rule gets via `$(CROSS_TEST_CFLAGS)`. Because these explicit rules override the `$(BUILD_DIR)/%: tests/%.c` pattern rule, no `.d` file is emitted, so editing `tests/test-harness.h` (included by both `test-mmap-lazy.c` and `test-mmap-fastpath.c`) will no longer rebuild these binaries. This breaks the exact guarantee the pattern-rule comment states: "-MMD tracks the shared test headers, so editing one rebuilds every guest binary that includes it." Use `$(CROSS_TEST_CFLAGS)` like the neighboring rules so header changes rebuild these tests.</comment>

<file context>
@@ -311,6 +311,33 @@ $(BUILD_DIR)/test-sigsuspend: tests/test-sigsuspend.c | $(BUILD_DIR)
+# 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 -D_GNU_SOURCE -static -O2 -o $@ $< -lpthread
+
+# test-mmap-lazy races concurrent first touch from several threads.
</file context>
Suggested change
$(Q)$(CROSS_COMPILE)gcc -D_GNU_SOURCE -static -O2 -o $@ $< -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 -D_GNU_SOURCE -static -O2 -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 -D_GNU_SOURCE -static -O2 -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)"
Expand Down
8 changes: 8 additions & 0 deletions docs/internals.md
Original file line number Diff line number Diff line change
Expand Up @@ -457,6 +457,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
Expand Down
10 changes: 10 additions & 0 deletions docs/usage.md
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
28 changes: 25 additions & 3 deletions mk/shim.mk
Original file line number Diff line number Diff line change
@@ -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 $< $@
Expand Down
32 changes: 32 additions & 0 deletions mk/verify.mk
Original file line number Diff line number Diff line change
Expand Up @@ -311,6 +311,38 @@ VERIFY_ALIGN_SCAN := src/proved/align.h
VERIFY_ALIGN_CLAIM := for ANY address, alignment, and search window
VERIFY_ALIGN_UNPROVED := the region-array walk around them stays 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 measured from a real run (92 of 93 discharged; 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 caused by this target, and not this target's to fix), set a little
# under 93 so a future edit that quietly drops goals still trips the floor.
#
# 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 ?= 88

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2: The comment block and the MIN_GOALS value disagree with each other and with the recipe's own gate. The comment says the measured run generated 93 obligations and discharged 92, leaving align_up_ok_ensures_rejects_only_on_wrap open, and that this "is not this target's to fix"; then it says the floor is "set a little under 93". But VERIFY_MMAPFASTPATH_MIN_GOALS is set to 88, which is not "a little under 93" and lets an edit silently drop five obligations without tripping the tripwire. More importantly, scripts/check-wp-result.py gate 4 fails the run whenever proved != total (--unproved is only printed in the success banner, not treated as a pass condition). So if the comment is accurate and one obligation genuinely stays open, the verify-mmapfastpath target cannot pass CI as written; if the target does pass, then the "92 of 93 discharged / not this target's to fix" description is wrong and misleading. Reconcile the two: either set MIN_GOALS to a value genuinely just under the passing run's generated count (e.g. 92 for 93) and state that all obligations are discharged, or actually discharge/address the open goal rather than describing it as an accepted open goal.

Prompt for AI agents
Check if this issue is valid — if so, understand the root cause and fix it. At mk/verify.mk, line 335:

<comment>The comment block and the MIN_GOALS value disagree with each other and with the recipe's own gate. The comment says the measured run generated 93 obligations and discharged 92, leaving `align_up_ok_ensures_rejects_only_on_wrap` open, and that this "is not this target's to fix"; then it says the floor is "set a little under 93". But `VERIFY_MMAPFASTPATH_MIN_GOALS` is set to 88, which is not "a little under 93" and lets an edit silently drop five obligations without tripping the tripwire. More importantly, scripts/check-wp-result.py gate 4 fails the run whenever `proved != total` (`--unproved` is only printed in the success banner, not treated as a pass condition). So if the comment is accurate and one obligation genuinely stays open, the `verify-mmapfastpath` target cannot pass CI as written; if the target does pass, then the "92 of 93 discharged / not this target's to fix" description is wrong and misleading. Reconcile the two: either set MIN_GOALS to a value genuinely just under the passing run's generated count (e.g. 92 for 93) and state that all obligations are discharged, or actually discharge/address the open goal rather than describing it as an accepted open goal.</comment>

<file context>
@@ -311,6 +311,38 @@ VERIFY_ALIGN_SCAN := src/proved/align.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 ?= 88
+VERIFY_MMAPFASTPATH_MODEL := typed
+VERIFY_MMAPFASTPATH_SCAN := src/proved/mmap-fastpath.h src/proved/align.h
</file context>

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
VERIFY_PATHDEPTH_MIN_GOALS ?= 24
Expand Down
39 changes: 38 additions & 1 deletion src/core/bootstrap.c
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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));
Expand Down Expand Up @@ -302,7 +323,14 @@ 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
Expand Down Expand Up @@ -563,6 +591,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,
Expand Down Expand Up @@ -756,6 +785,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));

Expand Down Expand Up @@ -864,6 +900,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;
Expand Down
Loading
Loading