sysprog21 · jserv · Aug 21, 2026 · Aug 21, 2026 · Aug 21, 2026 · Aug 22, 2026
diff --git a/.ci/check-matrix-lists.sh b/.ci/check-matrix-lists.sh
@@ -18,6 +18,13 @@
 #   2. A label in both lists at once. The test is then skipped under every
 #      runner the matrix has, so it never executes anywhere while still looking
 #      registered.
+#   3. A tests/manifest.txt binary that no test_* call registers at all. Same
+#      cost, arrived at from the other side: "make check" runs it, the matrix
+#      never does, and the reference kernel therefore never adjudicates it. Six
+#      tests reached that state before this check existed, four of them added
+#      in the same branch that claimed they encoded Linux behaviour. Only the
+#      matrix can substantiate such a claim, so a test that skips it is a claim
+#      nobody checked.
 #
 # The pass counts themselves are not checked here. test-matrix.sh already holds
 # each lane to its EXPECTED_BASELINES floor at runtime, which is a stronger
@@ -47,9 +54,61 @@ registered_labels()
         | sed -E 's/.*"\$runner" +"([^"]+)"$/\1/' | sort -u
 }
 
+# Manifest binaries the matrix deliberately does not run. Each asserts an
+# elfuse-internal implementation detail with no counterpart on a real kernel, so
+# the reference lane has nothing to say about it. The matrix's own comment above
+# its suite list is the long form; this is the machine-readable copy.
+MATRIX_EXEMPT="
+test-oom-proc
+test-shim-identity
+test-shim-identity-attention
+test-shim-verbose-trace
+test-shim-data-el1
+test-shim-urandom-smp
+test-shim-urandom-toctou
+test-shim-urandom-wrap
+test-shim-cred-race
+test-mremap-infra
+test-mremap-fork-tracking
+test-dev-shm-paths
+"
+
+# The binary name from each manifest line: the first field, with any trailing
+# arguments and any "#" marker dropped.
+#
+# Matching the whole line instead missed 17 of the 84 entries, because a
+# manifest line carries arguments (test-argc a b c) and markers (test-thread #
+# diff=skip) beside the name. Those were exactly the entries a coverage guard
+# most wants to see, and it reported success while checking two thirds of the
+# list.
+manifest_tests()
+{
+    local manifest
+    manifest="$(dirname "$0")/../tests/manifest.txt"
+    if [ ! -r "$manifest" ]; then
+        echo "Error: cannot read $manifest; the coverage check needs it" >&2
+        return 1
+    fi
+    sed -E 's/#.*//' "$manifest" | awk '{print $1}' \
+        | grep -E '^test-[A-Za-z0-9._-]+$' | sort -u
+}
+
 ret=0
 registered="$(registered_labels)"
 
+manifest_list="$(manifest_tests)" || exit 1
+
+while IFS= read -r test; do
+    [ -n "$test" ] || continue
+    printf '%s\n' "$MATRIX_EXEMPT" | grep -qxF "$test" && continue
+    if ! printf '%s\n' "$registered" | grep -qxF "$test"; then
+        echo "Error: tests/manifest.txt has '$test', which the matrix never runs." >&2
+        echo "       Add a test_* call for it, or name it in MATRIX_EXEMPT here" >&2
+        echo "       with the reason the reference kernel cannot adjudicate it." >&2
+        ret=1
+    fi
+done <<< "$manifest_list"
+
 for list in QEMU_SKIP ELFUSE_SKIP; do
     while IFS= read -r label; do
         [ -n "$label" ] || continue

diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml
@@ -123,6 +123,31 @@ jobs:
           # empty and the macOS job does not start at all.
           extra=$(comm -23 <(printf '%s\n' "$targets" | sort -u) \
                            <(printf '%s\n' "$mutants" | sort -u))
+          # Write the split to the run summary. Someone reading a skipped
+          # "Frama-C WP proofs" job needs to see that its targets moved to the
+          # mutation legs rather than nowhere, without reading this file.
+          {
+            echo "### Proof scope"
+            echo
+            if [ -n "$mutants" ]; then
+              echo "Proved and mutated, in the mutation legs (each leg proves"
+              echo "its target unmutated first, as the control):"
+              echo
+              printf '%s\n' "$mutants" | sed 's/^/- /'
+            else
+              echo "No target's mutation verdict can change in this diff."
+            fi
+            echo
+            if [ -n "$extra" ]; then
+              echo "Proved in the standalone job, which nothing else covers:"
+              echo
+              printf '%s\n' "$extra" | sed 's/^/- /'
+            else
+              echo "The standalone proof job has nothing left to prove and"
+              echo "skips; every target above is proved in its mutation leg."
+            fi
+          } >> "$GITHUB_STEP_SUMMARY"
+
           # rules is already prefixed, so the prove job needs no shell of its
           # own; mutants is JSON because it is a matrix. The guard matters:
           # printf runs its format once even with no arguments, so an empty
@@ -185,7 +210,11 @@ jobs:
   # a proof-only job would quietly stop enforcing half of what anyone requiring
   # it expected. The combined verdict keeps that name; see the last job here.
   verify-proofs:
-    name: Frama-C WP proofs
+    # The name says which targets, because the skip is the common case and a
+    # bare "Frama-C WP proofs: skipped" on a diff that edits a proof reads as
+    # though the proofs did not run. They did, inside the mutation legs, each
+    # of which proves its target unmutated before it mutates anything.
+    name: Frama-C WP proofs (targets no mutation leg covers)
     needs: proof-targets
     # Nothing to prove, so do not boot a macOS runner for it.
     if: ${{ needs.proof-targets.outputs.empty != 'true' }}

diff --git a/Makefile b/Makefile
@@ -277,6 +277,14 @@ $(BUILD_DIR)/test-guest-env-host: $(BUILD_DIR)/test-guest-env-host.o \
 	@echo "  LD      $@"
 	$(Q)$(CC) $(CFLAGS) -o $@ $^
 
+# test-stdio-nonblock-host launches elfuse with a pipe as stdin and checks the
+# flags on its own end of that pipe afterwards, so it is a host binary. It sits
+# outside the guest-binary guard below because check requires it through
+# CHECK_HOST_UNIT_BINS whether or not the guest binaries are pre-built.
+$(BUILD_DIR)/test-stdio-nonblock-host: tests/test-stdio-nonblock-host.c | $(BUILD_DIR)
+	@echo "  CC      $<"
+	$(Q)$(CC) $(CFLAGS) -Itests -o $@ $<
+
 # Guest test binaries (cross-compiled, aarch64-linux)
 # Only used when GUEST_TEST_BINARIES is not set.
 
@@ -298,6 +306,29 @@ $(BUILD_DIR)/%: tests/%.c | $(BUILD_DIR)
 	@echo "  CROSS   $<"
 	$(Q)$(CROSS_COMPILE)gcc $(CROSS_TEST_CFLAGS) -o $@ $<
 
+# test-eventfd-semaphore-contended races two blocking readers on one eventfd.
+$(BUILD_DIR)/test-eventfd-semaphore-contended: \
+		tests/test-eventfd-semaphore-contended.c | $(BUILD_DIR)
+	@echo "  CROSS   $< (with -lpthread)"
+	$(Q)$(CROSS_COMPILE)gcc $(CROSS_TEST_CFLAGS) -o $@ $< -lpthread
+
+# test-socket-accept-contended parks two threads on one listener.
+$(BUILD_DIR)/test-socket-accept-contended: \
+		tests/test-socket-accept-contended.c | $(BUILD_DIR)
+	@echo "  CROSS   $< (with -lpthread)"
+	$(Q)$(CROSS_COMPILE)gcc $(CROSS_TEST_CFLAGS) -o $@ $< -lpthread
+
+# test-socket-waitall drips the tail of a MSG_WAITALL request from a second
+# thread.
+$(BUILD_DIR)/test-socket-waitall: tests/test-socket-waitall.c | $(BUILD_DIR)
+	@echo "  CROSS   $< (with -lpthread)"
+	$(Q)$(CROSS_COMPILE)gcc $(CROSS_TEST_CFLAGS) -o $@ $< -lpthread
+
+# test-dup-setfl-race races a dup against an F_SETFL sweep from a second thread.
+$(BUILD_DIR)/test-dup-setfl-race: tests/test-dup-setfl-race.c | $(BUILD_DIR)
+	@echo "  CROSS   $< (with -lpthread)"
+	$(Q)$(CROSS_COMPILE)gcc $(CROSS_TEST_CFLAGS) -o $@ $< -lpthread
+
 # test-pthread needs -lpthread
 $(BUILD_DIR)/test-pthread: tests/test-pthread.c | $(BUILD_DIR)
 	@echo "  CROSS   $< (with -lpthread)"
@@ -329,6 +360,16 @@ $(BUILD_DIR)/test-threaded-exec: tests/test-threaded-exec.c | $(BUILD_DIR)
 	@echo "  CROSS   $< (with -lpthread)"
 	$(Q)$(CROSS_COMPILE)gcc $(CROSS_TEST_CFLAGS) -o $@ $< -lpthread
 
+# test-sigpipe needs a thread to close the reader mid-write.
+$(BUILD_DIR)/test-sigpipe: tests/test-sigpipe.c | $(BUILD_DIR)
+	@echo "  CROSS   $< (with -lpthread)"
+	$(Q)$(CROSS_COMPILE)gcc $(CROSS_TEST_CFLAGS) -Itests -o $@ $< -lpthread
+
+# test-pipe-steal contends several readers for one byte, then execs on top.
+$(BUILD_DIR)/test-pipe-steal: tests/test-pipe-steal.c | $(BUILD_DIR)
+	@echo "  CROSS   $< (with -lpthread)"
+	$(Q)$(CROSS_COMPILE)gcc $(CROSS_TEST_CFLAGS) -Itests -o $@ $< -lpthread
+
 # test-exec-handoff parks the leader while a worker hands it a failing execve.
 $(BUILD_DIR)/test-exec-handoff: tests/test-exec-handoff.c | $(BUILD_DIR)
 	@echo "  CROSS   $< (with -lpthread)"
@@ -444,6 +485,12 @@ $(BUILD_DIR)/test-lowbase-mem-300000: tests/test-lowbase-mem.c | $(BUILD_DIR)
 	$(Q)$(CROSS_COMPILE)gcc $(CROSS_TEST_CFLAGS) -no-pie \
 		-Wl,-Ttext-segment=0x300000 -o $@ $<
 
+# bench-hot-guard grew a bulk lane with a draining thread and a lane that runs
+# with a sibling alive, so it needs -lpthread; the pattern rule does not link it.
+$(BUILD_DIR)/bench-hot-guard: tests/bench-hot-guard.c | $(BUILD_DIR)
+	@echo "  CROSS   $< (with -lpthread)"
+	$(Q)$(CROSS_COMPILE)gcc $(CROSS_TEST_CFLAGS) -o $@ $< -lpthread
+
 # bench-hot-guard-glibc is the dynamic-glibc twin of bench-hot-guard.
 # Built only when the cross-glibc toolchain ships its own sysroot
 # (so a host without that toolchain can still run the rest of the
@@ -460,7 +507,7 @@ ifneq ($(wildcard $(LINUX_TOOLCHAIN)/aarch64-unknown-linux-gnu/sysroot/.),)
 $(BUILD_DIR)/bench-hot-guard-glibc: tests/bench-hot-guard.c | $(BUILD_DIR)
 	@echo "  CROSS   $< (dynamic glibc)"
 	$(Q)$(CROSS_COMPILE)gcc -D_GNU_SOURCE -DGUARD_USE_LIBC_CG=1 -O2 \
-		-o $@ $<
+		-o $@ $< -lpthread
 endif
 
 endif

diff --git a/mk/common.mk b/mk/common.mk
@@ -118,8 +118,25 @@ ifdef BUILD_FLAVOR_STALE
 # having succeeded, and a removal that failed silently is invisible to stderr.
 # Stopping is the point. Carrying on writes a stamp claiming a flavor the
 # leftover objects do not have.
-BUILD_FLAVOR_RM := $(shell find $(BUILD_DIR) \( -name '*.o' -o -name '*.d' \) -delete 2>/dev/null; \
-    find $(BUILD_DIR) \( -name '*.o' -o -name '*.d' \) 2>/dev/null | head -3)
+# Only the host objects and the dependency files that belong to them. A find
+# over the whole tree also takes the .d files of the cross-compiled guest
+# binaries, which are built with CROSS_TEST_CFLAGS and so have no flavor: the
+# binary survives the wipe while the record of which headers it depends on does
+# not, and editing tests/test-harness.h then stops rebuilding any of them. That
+# was invisible while the sanitizer lanes still depended on "clean", which
+# removed binary and .d together; dropping that prerequisite made the mismatch
+# permanent, so the wipe's unit has to match the flavor's unit.
+#
+# A .d does not sit beside its object. DEPFLAGS above writes it flat under
+# build/ with the path separators replaced by underscores, so the object
+# build/syscall/casefold.o is described by build/syscall_casefold.d. Deriving
+# the name by suffix substitution alone names a file that has never existed on
+# this tree, which is a wipe that silently keeps every stale record it claims
+# to remove.
+BUILD_FLAVOR_DEPS := $(foreach o,$(BUILD_FLAVOR_OBJS),\
+    $(BUILD_DIR)/$(subst /,_,$(patsubst $(BUILD_DIR)/%,%,$(basename $(o)))).d)
+BUILD_FLAVOR_RM := $(shell rm -f $(BUILD_FLAVOR_OBJS) $(BUILD_FLAVOR_DEPS) \
+    2>/dev/null; ls $(BUILD_FLAVOR_OBJS) $(BUILD_FLAVOR_DEPS) 2>/dev/null | head -3)
 ifneq ($(BUILD_FLAVOR_RM),)
 $(error FLAVOR: stale objects under $(BUILD_DIR) survived removal: $(BUILD_FLAVOR_RM))
 endif

diff --git a/mk/config.mk b/mk/config.mk
@@ -29,6 +29,7 @@ NATIVE_TESTS := tests/test-multi-vcpu.c tests/test-rwx.c \
                 tests/test-dynamic-array-host.c \
                 tests/test-string-builder-host.c \
                 tests/test-wakeup-pipe-host.c \
+                tests/test-stdio-nonblock-host.c \
                 tests/test-guest-env-host.c
 SPECIAL_TEST_SRCS := tests/test-lowbase-mem.c
 SPECIAL_TEST_BINS := $(BUILD_DIR)/test-lowbase-mem-200000 $(BUILD_DIR)/test-lowbase-mem-300000

diff --git a/mk/format.mk b/mk/format.mk
@@ -31,10 +31,16 @@ check-format: check-syscall-dispatch
 	@echo "  MATRIX  skip lists"
 	$(Q)bash .ci/check-matrix-lists.sh
 	$(call require-tool,shellcheck,brew install shellcheck)
+	@# -x follows the "# shellcheck source=..." directives the scripts already
+	@# carry. Without it those directives are inert, every variable a sourced
+	@# lib sets reads as unassigned, and the counters in tests/lib/report.sh
+	@# had to be duplicated into each of its twelve callers to keep the gate
+	@# quiet -- which then failed the other way, as twelve assignments nobody
+	@# in that file uses.
 	@printf "  SHCHK   %d scripts\n" $(words $(SHELL_SCRIPTS))
 	@fail=0; \
 	for f in $(SHELL_SCRIPTS); do \
-		if shellcheck --severity=warning "$$f" 2>&1; then \
+		if shellcheck -x --severity=warning "$$f" 2>&1; then \
 			printf "  $(GREEN)OK$(RESET) %s\n" "$$f"; \
 		else \
 			printf "  $(RED)FAIL$(RESET) %s\n" "$$f"; \

diff --git a/mk/tests.mk b/mk/tests.mk
@@ -107,16 +107,28 @@ endef
 # spurious TIMEOUT. TEST_TIMEOUT is only overridden if the caller has not
 # already set one.
 
+# No "clean" prerequisite. These lanes used to depend on it, which removed the
+# whole build tree including the 186 cross-compiled guest binaries -- built with
+# CROSS_TEST_CFLAGS, and so untouched by anything EXTRA_CFLAGS says. The FLAVOR
+# stamp in mk/common.mk was added later to solve the same problem exactly:
+# it removes the *.o and *.d that a CFLAGS change actually invalidates, and
+# leaves the rest. Measured on this tree, the clean cost 186 needless
+# cross-compiles per sanitizer run, most of the lane's wall time.
+#
+# What still protects the link is the stamp, not the clean: the sub-make below
+# re-reads common.mk with the sanitizer CFLAGS, sees a different flavor, and
+# drops every host object before anything is compiled or linked.
+
 ## Run the sanitizer subset with AddressSanitizer (ASAN)
-check-asan: clean
+check-asan:
 	ASAN_OPTIONS="abort_on_error=1:detect_leaks=0" TEST_TIMEOUT="$${TEST_TIMEOUT:-30}" $(MAKE) EXTRA_CFLAGS="-fsanitize=address -fno-omit-frame-pointer" check-sanitizer
 
 ## Run the sanitizer subset with UndefinedBehaviorSanitizer (UBSAN)
-check-ubsan: clean
+check-ubsan:
 	UBSAN_OPTIONS="halt_on_error=1:print_stacktrace=1" TEST_TIMEOUT="$${TEST_TIMEOUT:-30}" $(MAKE) EXTRA_CFLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined -fno-omit-frame-pointer" check-sanitizer
 
 ## Run the sanitizer subset with ThreadSanitizer (TSAN)
-check-tsan: clean
+check-tsan:
 	TSAN_OPTIONS="halt_on_error=1" TEST_TIMEOUT="$${TEST_TIMEOUT:-60}" $(MAKE) EXTRA_CFLAGS="-fsanitize=thread -fno-omit-frame-pointer" check-sanitizer
 
 # Manifest sections that exercise elfuse-internal concurrency, memory, fork,
@@ -180,7 +192,7 @@ endef
 CHECK_HOST_UNIT_BINS := $(addprefix $(BUILD_DIR)/, \
         test-tlbi-encoder-host test-fork-ipc-protocol-host \
         test-vcpu-run-hooks-host test-identity-override-host \
-        test-teardown-live-vcpu-host test-casefold-host \
+        test-teardown-live-vcpu-host test-stdio-nonblock-host test-casefold-host \
         test-casefold-walk-host test-absock-names-host \
         test-dynamic-array-host test-string-builder-host \
         test-wakeup-pipe-host test-guest-env-host)
@@ -201,6 +213,7 @@ $(call run-host-unit,test-absock-names-host,absock derived-name unit test)
 $(call run-host-unit,test-dynamic-array-host,dynamic array unit test)
 $(call run-host-unit,test-string-builder-host,string builder unit test)
 $(call run-host-unit,test-wakeup-pipe-host,wakeup pipe concurrency unit test)
+$(call run-host-unit,test-stdio-nonblock-host,launcher stdio flags across a guest)
 $(call run-host-unit,test-guest-env-host,guest environment merge cross product)
 $(call run-lane,test-sysroot-name-unique,one on-disk name per guest name)
 $(call run-lane,test-sysroot-name-relative,relative and dirfd-relative names)

diff --git a/mk/verify.mk b/mk/verify.mk
@@ -272,13 +272,21 @@ VERIFY_DIRENT_CLAIM := for ANY name length a host or FUSE directory can present
 VERIFY_DIRENT_UNPROVED := the readdir walk and the name translation stay test-covered
 
 VERIFY_IOV_SRC  := src/proved/iov.h
-VERIFY_IOV_FCTS := iov_count_ok iov_total_add
-VERIFY_IOV_MIN_GOALS ?= 17
+VERIFY_IOV_FCTS := iov_count_ok iov_total_add iov_advance_index
+VERIFY_IOV_MIN_GOALS ?= 40
 VERIFY_IOV_MODEL := typed
 VERIFY_IOV_SCAN := src/proved/iov.h
 VERIFY_IOV_CLAIM := for ANY iovec array a guest can write
 VERIFY_IOV_UNPROVED := the per-entry guest_ptr bounds stay test-covered
 
+VERIFY_ASYNCUDATA_SRC  := src/proved/asyncudata.h
+VERIFY_ASYNCUDATA_FCTS := async_udata_fd async_udata_gen async_udata_pack
+VERIFY_ASYNCUDATA_MIN_GOALS ?= 15
+VERIFY_ASYNCUDATA_MODEL := typed
+VERIFY_ASYNCUDATA_SCAN := src/proved/asyncudata.h
+VERIFY_ASYNCUDATA_CLAIM := for ANY guest fd and slot generation the watcher can arm
+VERIFY_ASYNCUDATA_UNPROVED := the kevent registration and the delivery-side owner checks stay test-covered
+
 VERIFY_FDSET_SRC  := src/proved/fdset.h
 VERIFY_FDSET_FCTS := fdset_words fdset_fd_index fdset_slot
 VERIFY_FDSET_MIN_GOALS ?= 43
@@ -336,7 +344,11 @@ commafy = $(subst $(verify_space),$(verify_comma),$(strip $(1)))
 # target name is enough and stays readable; a new target using a letter not
 # listed here shows up immediately as a literal upper-case character in the
 # rule name rather than silently misbehaving.
-lc = $(subst A,a,$(subst B,b,$(subst C,c,$(subst D,d,$(subst E,e,$(subst F,f,$(subst G,g,$(subst H,h,$(subst I,i,$(subst K,k,$(subst L,l,$(subst M,m,$(subst N,n,$(subst O,o,$(subst P,p,$(subst Q,q,$(subst R,r,$(subst S,s,$(subst T,t,$(subst U,u,$(subst V,v,$(subst W,w,$(subst X,x,$(1))))))))))))))))))))))))
+# Lowercase a target name. Spelled out per letter because make has no case
+# function; J, Y and Z were missing from this chain, so a proof target whose
+# name contained one produced a rule nobody could invoke -- silently, since the
+# .PHONY list and the rule name were wrong in the same way. Keep all 26.
+lc = $(subst A,a,$(subst B,b,$(subst C,c,$(subst D,d,$(subst E,e,$(subst F,f,$(subst G,g,$(subst H,h,$(subst I,i,$(subst J,j,$(subst K,k,$(subst L,l,$(subst M,m,$(subst N,n,$(subst O,o,$(subst P,p,$(subst Q,q,$(subst R,r,$(subst S,s,$(subst T,t,$(subst U,u,$(subst V,v,$(subst W,w,$(subst X,x,$(subst Y,y,$(subst Z,z,$(1)))))))))))))))))))))))))))
 
 # The proof targets, derived rather than listed. Make knows every variable it
 # has read, so the set of VERIFY_<T>_SRC assignments above IS the target list;