[Greepolis]

Scope

Adds a replayable Linux ABI syscall test on ksvc_fake, using the real linux_syscall() dispatcher and handlers with independent reference models. The ABI module remains in the uncovered debt: the current tests cover useful slices, not the whole kernel/abi/ tree.

Modelled slices

• Regular files and offsets: open, read, write, lseek, pread64, pwrite64, dup, dup2, close; the oracle owns file bytes, open-description references and shared offsets.
• Descriptor table: dup3, fcntl(F_DUPFD), F_DUPFD_CLOEXEC, F_GETFD/F_SETFD, O_CLOEXEC, close_range, the 1024-descriptor limit and EMFILE, including first-free-slot reuse.
• Pipes: pipe2, queue ordering, partial reads, capacity-limited nonblocking writes, EAGAIN, and EOF after the last writer closes.
• Vector and positional I/O: readv, writev, preadv, pwritev, with checks that positional operations leave the shared offset unchanged.
• Anonymous memory mappings: two-page private mmap tracked by an independent interval model, MAP_FIXED_NOREPLACE, MAP_FIXED replacement of an existing page, unaligned-address and missing-mapping-type EINVAL checks, independent page contents, mprotect read-only enforcement and restoration, partial munmap, file-backed MAP_PRIVATE copy isolation, tmpfs MAP_SHARED page aliasing in both directions, and access checks against the real fake page tables.
• Fork and inherited descriptors: copied descriptor flags/table, shared open-description offsets across parent and child, inherited pipe writers, wait4(WNOHANG) while the child is live, private-page COW isolation after a child write, and survival of the child's mapping after the parent's munmap.
• Paths and metadata: mkdir/mkdirat, unlink/unlinkat, legacy readlink/readlinkat, chdir/getcwd (including ERANGE and cwd-relative lookup), relative openat through a directory descriptor, O_CREAT, O_EXCL, O_TRUNC, O_APPEND, linkat (shared inode/link count, directory refusal and cross-mount EXDEV), symlinkat/readlinkat (raw target bytes, truncation, follow/no-follow behavior), renameat2(RENAME_NOREPLACE), nested two-level directories with relative dirfds, nested getdents64/newfstatat, ENOTEMPTY refusal and cleanup, unlinkat, directory removal, one-directory getdents64 enumeration, ftruncate, fstat and relative newfstatat size/type checks.

The models compare returned values and user-visible bytes/metadata against state they own; they do not read the fake filesystem or kernel descriptor table.

Production mutations

The Linux model is paired with production mutations for lseek, dup shared offsets, pread64/pwrite64 position preservation, pipe2 nonblocking mode, dup3 and F_DUPFD_CLOEXEC flags, F_SETFD, close_range, EMFILE, O_APPEND, ftruncate, stat size, getdents64 enumeration, the renameat2 no-replace result, chdir working-directory updates, linkat, symlinkat, readlinkat and the legacy pathname wrappers, mkdirat, unlinkat, anonymous and file-backed private/shared mmap including fixed replacement and mapping-type validation, mprotect, munmap, fork descriptor-table copying and fork COW-page marking. A separate NT dispatcher suite (nt_syscall, not the Linux selector) models handle close/duplication and seeded file read/write sequences; its mutations cover NtClose, NtDuplicateObject, NtReadFile, NtWriteFile, NtCreateFile dispositions and per-handle access-right enforcement, and each runs against the NT host-test suite.

Remaining ABI debt

Not yet modelled: most Linux ABI syscall handlers, full directory-tree operations and more complex rename cases, broader file types, child exit/reap, exit-time descriptor release and the portable process table (the fake's ks_task_exit only escapes and does not model zombie/reap lifecycle), brk/mremap and the other memory handlers, and most of the NT personality. NT has a separate nt_syscall host-test harness, with a limited handle/file model and targeted mutations, but that does not cover the rest of kernel/abi/nt/. Unsupported areas remain documented as uncovered. Each newly claimed area needs a production mutation caught by its model.

The ABI nightly job remains enabled as a useful scoped test, but carries no module-coverage annotation. The checker baseline remains 3 (ABI, PROC and TXN).

Stacked follow-ups

• PR #209 is kept on hold; no changes are being made to its branch. Its current description still assumes ABI is covered and claims a baseline of 1; that claim must be recomputed before resuming it.
• PR #210 is kept on hold; no changes are being made to its branch. Its current description still assumes ABI, PROC and TXN are covered and claims a baseline of 0; that claim must be recomputed before resuming it.
• Issue [test] Burn down the uncovered-module debt in nightly intensive coverage #201 remains open.

Branch safety

• Branch: test/abi-intensive-coverage-201
• This branch contains merge commit c7322de3 from main.
• This PR itself has not been merged into main; no changes from this branch have been applied to main.

[Greepolis]

Review: changes requested — the ABI module is not covered yet

The test itself is good. It drives the real linux_syscall() dispatcher and handlers on ksvc_fake. Its model of file bytes, descriptors and shared offsets is independent of the code it checks, and it never reads the kernel's state. All three sabotage cases are caught: dup resetting the offset, pread64 moving it, and lseek returning 0. CI is green on the branch after the merge of main.

The problem is the claim. The test is small; the module it removes from the coverage debt is not.

Why abi cannot leave the debt with this test

check-nightly-coverage.py counts # module: abi as coverage of all of kernel/abi/:

Part	Lines	Covered here
kernel/abi/linux/	~18,700	8 file/descriptor syscalls
kernel/abi/nt/	~9,100	none
kernel/abi/files/	~4,100	regular files only
kernel/abi/mem/	~330	none

That is roughly 5% of the module. The rule in CLAUDE.md is one intensive, randomised test per module, checked against an independent model. Lowering the baseline from 3 to 2 on this test makes the ratchet green by construction: the checker sees the tag, not what the job exercises.

What is missing before abi can be counted

The model must be extended, with seeded sequences through ksvc_fake against an independent model. Each new area needs at least one production mutation that the model catches.

1. Paths and directories (kernel/abi/linux/fs.c):
   • openat with O_CREAT, O_EXCL, O_TRUNC and O_APPEND;
   • mkdir, rmdir, unlink, rename (including RENAME_NOREPLACE), link and symlink/readlink;
   • getdents64 checked against the model's tree;
   • stat/fstat sizes and types;
   • ftruncate;
   • chdir and relative paths with dirfd.
2. Descriptor table semantics:
   • dup3, and O_CLOEXEC/FD_CLOEXEC through fcntl;
   • fcntl(F_DUPFD) and close_range;
   • the 1024-descriptor limit (EMFILE).
3. Other file types (kernel/abi/files/): pipes, at least. That means pipe2, partial reads and writes, EAGAIN with O_NONBLOCK, and EOF after the last writer closes, all against a byte-queue model.
4. Vector and positional I/O: pwrite64, readv/writev and preadv/pwritev, which share the offset rules already modelled.
5. Processes and descriptors: fork sharing descriptions with the child, exit releasing them, and wait4 statuses, as far as the fake supports them. If the fake cannot run these, document it in the "why it remains" table rather than leaving them out silently.
6. Memory (kernel/abi/mem/, the mm rows in linux/): mmap/munmap/mprotect ranges against an interval model, including MAP_FIXED over an existing mapping and the EINVAL cases.
7. NT personality (kernel/abi/nt/): a seeded sequence of NtCreateFile/NtReadFile/NtWriteFile/NtClose and handle duplication against the same kind of model, with at least one mutation, such as a handle granted rights it was not asked for. Alternatively, split abi into abi-linux and abi-nt in the coverage checker and keep abi-nt in the debt explicitly. Either is acceptable; counting NT as covered by a Linux file test is not.

Smaller points

• The syscall numbers are bare literals (2, 0, 17, 32, …). Use named constants so a reader knows which call each one is.
• scripts/dev/cases/abi-coverage.txt is missing a blank line before the third case.
• The PR description says "no merge performed". The branch now contains a merge of main (c7322de).
• PRs #209 and #210 sit on top of this branch, and #210 says the final baseline reaches zero. Recompute both claims once ABI's scope is settled.

When this can be approved

When the model covers the areas above, or the ones left out are written down as a split module that stays in the debt, each with a mutation the model catches. The baseline may then go to 2.

[Greepolis]

Re-review: ready to merge, with one wording fix

What changed since the last review

The earlier review asked for one of two outcomes: cover the module, or write the uncovered parts down and keep abi in the debt. The PR now takes the second path, and does it honestly:

• the baseline stays at 3, and abi remains one uncovered module;
• module_torture.md and check-nightly-coverage.py say plainly that most of kernel/abi/linux/ and kernel/abi/nt/ is not modelled.

The 17 new commits add real value:

• MAP_FIXED. Replacing an existing page must give zero-filled memory, not keep the old page's bytes. An unaligned fixed address and a mapping with no type are now rejected with EINVAL.
• Legacy pathname wrappers. mkdir, unlink and readlink are now exercised as table entries of their own, each with a mutation.
• NT handle rights. There is a mutation for them, run against the NT suite.
• NT verifier fix. The NT mutations now run verify-nt-abi-torture.sh. Before, they ran the Linux torture, which cannot reach NT code, so those cases could not go red for the right reason.

Verification

I merged the PR with current main (11 commits ahead, which change nt/file.c, futex.c, timer.c and ext2.c) and ran:

Check	Result
Merge with main	clean, no conflicts
check-sabotage-anchors.py	ok, nothing unresolved
check-nightly-coverage.py	ok (baseline 3)
ctest	16/16 pass
verify-module-mutations.sh	rc 0, 63 cases across 15 files, every one red, every file restored

CI on the branch is green on all 18 checks.

One point to fix before merging

module_torture.md says the anonymous mappings are "tracked by an independent interval model". The interval set in test_memory_model() is updated by the test next to each call, and vm_model_access() asks the model, never the kernel. The checks that constrain the kernel are still the per-page kf_peek/kf_poke calls the scenario already made. As written, the model cannot disagree with the kernel, so it is not an oracle yet.

Either of these closes the point:

1. After each operation, walk every page of the range and require kf_peek to succeed exactly where the model says a page is mapped, and kf_poke exactly where it says the page is writable. The model then becomes a real oracle.
2. Or reword the sentence to say the interval set documents the expected layout, without claiming that it checks the kernel.

Option 1 is better: it is a small loop and it turns the model into evidence.

Minor

• The branch is 11 commits behind main. It merges cleanly and passes, so this needs no action.