daniel/danos
1
0
Fork 0
Code Issues 4 Pull Requests Actions Packages Projects 1 Releases Wiki Activity

test: partitioned-image tool + shared-channel multi-volume proof (S3)

Browse Source 
The two-volumes case proves multiple DEVICES; this proves multiple
volumes on ONE device. make-partitioned-image.py lays several FAT32
partitions (each from make-fat-image) behind a classic MBR; the new
partitioned-volume case attaches one such disk (two partitions,
da7a0001 at lba 2048, da7a0002 at lba 83968) as a single usb-storage
device.

partition.allVolumes walks the table and the manager spawns a confined
fat per partition on the SAME block channel, each clamped to its own LBA
range by usb-storage's per-badge range table — so partition B's fat
cannot read partition A's blocks. The case asserts two mount lines at
two distinct non-zero base_lbas on one device; against the pre-uncap
allVolumes (S3 step 2, capped to one partition) only da7a0001 mounts.

No image is committed — the disk is generated per run. Full suite
130/130 (128 + two-volumes + partitioned-volume).
This commit is contained in:
Daniel Samson
2026-08-10 02:35:32 +01:00
parent bf9f8560c6
commit d59279422e
2 changed files with 120 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files
test/qemu_test.py
+32 -5
View File
@@ -837,6 +837,26 @@ CASES = [
r"(?=.*carries the system tree)"
r"(?=.*data volume; mounted at /volumes/fat-da7a0001)",
"fail": r"data volume; mounted at /volumes/fat-12345678|DANOS-TEST-RESULT: FAIL"},
# S3 shared-channel multi-volume: ONE usb-storage device carrying an MBR with
# TWO FAT partitions (da7a0001 at lba 2048, da7a0002 at lba 83968). allVolumes
# walks the table and the manager spawns a confined fat per partition on the
# SAME block channel, each clamped to its own LBA range (usb-storage's
# per-badge range table) — the path a pair of single-volume sticks (the
# two-volumes case) does NOT exercise. The two mount lines sit at two DISTINCT
# non-zero base_lbas on one device. Against the pre-uncap allVolumes (S3 step
# 2, capped to one partition) only da7a0001 mounts, so the da7a0002 lookaheads
# fail.
{"name": "partitioned-volume",
"build_case": "fat-mount",
"smp": 4,
"timeout": 150,
"data_volume": {"partitions": [{"serial": "DA7A0001", "size_mib": 40},
{"serial": "DA7A0002", "size_mib": 40}]},
"expect": r"(?s)(?=.*volume 0x0*da7a0001 -> \S+ \(pid \d+\), lba 2048, )"
r"(?=.*volume 0x0*da7a0002 -> \S+ \(pid \d+\), lba 83968, )"
r"(?=.*fat: mounted /volumes/fat-da7a0001)"
r"(?=.*fat: mounted /volumes/fat-da7a0002)",
"fail": r"DANOS-TEST-RESULT: FAIL"},
# Phase 2b: mkdir/unlink through the mount. Reuses the fat-mount build — the
# fat-test client, after listing, makes a directory, writes+reads a file inside
# it, then removes the file, exercising the whole VFS -> fat mutation path.
@@ -1451,11 +1471,18 @@ def run_case(arch, case):
if case.get("data_volume"):
dv = case["data_volume"]
data_img = os.path.join(WORK, "data-volume.img")
subprocess.run(
[sys.executable, os.path.join(REPO, "tools", "make-fat-image.py"),
"--serial", dv["serial"], "--label", dv.get("label", "DATAVOL"),
data_img, str(dv.get("size_mib", 64))],
check=True, stdout=subprocess.DEVNULL)
if dv.get("partitions"):
# One device, an MBR with several FAT partitions: several volumes share
# ONE block channel, each confined to its own LBA range.
gen = [sys.executable, os.path.join(REPO, "tools", "make-partitioned-image.py"), data_img]
for part in dv["partitions"]:
gen += [part["serial"], str(part.get("size_mib", 40))]
else:
# One device, one bare FAT volume.
gen = [sys.executable, os.path.join(REPO, "tools", "make-fat-image.py"),
"--serial", dv["serial"], "--label", dv.get("label", "DATAVOL"),
data_img, str(dv.get("size_mib", 64))]
subprocess.run(gen, check=True, stdout=subprocess.DEVNULL)
cmd += [
"-drive", f"if=none,id=datausb,format=raw,file={data_img}",
"-device", "usb-storage,bus=xhci.0,port=4,drive=datausb,removable=on,id=datastorage",