erofs-freebsd-out-tree/docs/pre15-stage0/P15-032.md

P15-032 / G09 vnode-backed image gate

Decision rule

This gate is source-preparatory only. It does not link its model into EROFS and does not authorize B39 merely because a declared state sequence looks safe. It pins and extracts the relevant FreeBSD 15 vnode, pager, mount, GEOM, md(4), nullfs, unionfs, tarfs, and deadfs contracts, compiles an owned-temporary C lifecycle model generated from P15-032-input.json, and rejects adversarial false-GO mutations.

The runner exits with:

• 0: gate GO;
• 10: gate STOP;
• 20 or another nonzero value: runner failure;
• 124: absolute gate timeout.

All phases have absolute deadlines. The generated C source and its output are copied into the requested evidence directory; the temporary executable is removed by the runner trap.

Closeable local vnode contract

The pinned FreeBSD sources support a coherent local lifecycle:

1. Use an explicit vnode:/absolute/path tag; GEOM remains explicit or legacy GEOM syntax. A mount and all device.N sources use one backend kind.
2. Resolve with namei, require VREG, retain vnode identity with vn_open_vnode(FREAD), retain the mounter credential with crhold, and use that credential for every source VOP_READ.
3. Apply VOP_SET_TEXT before first I/O. The default write-count contract rejects existing or later writers with ETXTBSY; retain a size snapshot and convert a short source read into EIO. Rename or pathname replacement does not change the held vnode identity.
4. Read synchronously into UIO_SYSSPACE under a source range lock and source vnode lock. FreeBSD's old vnode-pager fallback drops the VM object write lock before VOP_READ, so no user-buffer pager fault is introduced by this read shape.
5. Register the source mount with vfs_register_upper_from_vp before first I/O. On unmount, reject new I/O, drain delayed and in-flight completions, vflush, unregister the upper mount, unset text, close the vnode, release the held credential, and then release the final mount-private reference. A forced dead source returns ENXIO rather than silently changing identity.
6. Keep GEOM open/read/close and vnode open/read/close as disjoint tagged-union branches. This preserves the existing GEOM and multidevice behavior.

The generated model checks this order and independently removes each local invariant to ensure that every mutation is rejected.

Blocking FreeBSD contract

The required pre-I/O self and ancestor check is transitive across VFS and GEOM, not only across pathname aliases:

regular source vnode
  -> source filesystem
  -> md(4) GEOM provider
  -> md_s.s_vnode.vnode
  -> another filesystem vnode

The final identity edge is not available through a generic, identity-preserving FreeBSD API:

• VOP_GETLOWVNODE exposes vnode-stack aliases such as nullfs and unionfs, but it does not traverse a filesystem's GEOM storage dependency.
• vfs_register_upper_from_vp pins the immediate source vnode mount and orders its unmount, but it does not register hidden GEOM-to-vnode backing edges.
• md(4) stores the held backing vnode in the private struct md_s defined in md.c. Its GEOM object exposes only void *softc; dump configuration exposes a pathname, not a held vnode identity.
• Re-resolving that pathname fails the rename/replace invariant. Casting g_geom.softc to a copied private struct md_s is an undocumented, class-specific dependency and does not cover other filesystem-private or GEOM-private file-backed providers.

Consequently a visible-only oracle can approve all vnode, credential, pager, resize, and unmount checks while missing the hidden backing-vnode ancestor. The gate includes that case as an adversarial false-GO control. There is no sound place to return the required single cycle errno (EDEADLK) because the cycle identity cannot first be discovered.

Result

P15-032 is STOP and B39 is STOP-NO-SOURCE. Recursive I/O and its lock graph cannot be statically excluded for the requested regular-file source surface using documented generic FreeBSD interfaces. A safe future GO needs a new kernel dependency API that returns and pins transitive backing vnode identities, or an explicitly narrower feature contract whose permitted source filesystems have no hidden storage dependencies. Neither change is in B39's authorized write set.

Run from the repository root:

repo-pre-15/tests/pre15/gates/P15-032.sh \
  --base bd5a09054e5cf89efd4db82aadb051f20b06ebf7 \
  --freebsd-src /work/build/freebsd-src \
  --output /absolute/owned/output/path

No EROFS source, Makefile, feature documentation, B39 case, or B39 fixture is modified by this STOP addendum. D, H, K, Q, TC006, TC179, TC184, smoke, and the full feature suite are not run at the gate stage.