Prove two-node RISC-V Type 3 dirty back-invalidation - #2
Merged
Conversation
There was a problem hiding this comment.
Pull request overview
This PR adds a reproducible, end-to-end “two-node” functional-model proof that a dirty CXL Type 3 cache line written by a Legofs direct-path operation in one SiFive U RISC-V QEMU guest is returned via MESI-v2 back-invalidation to satisfy a competing read from a second guest, with strict evidence capture and offline validation.
Changes:
- Adds a complete build + run workflow (
run-legofs-type3.sh) to build the stack and execute two concurrentqemu-system-riscv64 -M sifive_uguests plus a TCP MESI-v2 CXLMemSim server. - Introduces a strict evidence pipeline (manifest schema v2, coherence JSONL parsing/correlation, console sidecar capture, and invariant checks) with new unit tests.
- Adds Legofs submodule pinning and documentation/specs describing the proof’s acceptance criteria and functional-model boundary.
Reviewed changes
Copilot reviewed 19 out of 19 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
tests/test_manifest.py |
Updates manifest tests for schema v2 and compiler version recording. |
tests/test_legofs_sources.py |
Adds tests ensuring Legofs/CXLMemSim ancestry pins and approved remote URL usage. |
tests/test_legofs_runtime.py |
Adds tests asserting exact SiFive U QEMU command construction and runtime invariants. |
tests/test_legofs_evidence.py |
Adds tests validating dirty back-invalidation correlation, strict JSONL parsing, and ordering gates. |
tests/test_legofs_build_contract.py |
Adds tests for kernel/devdax/network build requirements and build/run script contracts. |
scripts/write_manifest.py |
Extends build manifest generator to record compiler command + version output (schema v2). |
scripts/legofs_type3_2node.py |
Implements two-node orchestration, ownership/cleanup, evidence parsing, correlation, and result publication. |
scripts/build_legofs_type3.sh |
Adds a dedicated build pipeline producing static RV64 artifacts, images, and the build manifest. |
run-legofs-type3.sh |
Adds the single top-level entrypoint for building and/or running the proof. |
README.md |
Documents the one-command workflow and the functional-model claim boundary. |
guest/legofs_node_init.c |
Adds a freestanding PID1 that configures network, waits for devdax, and runs server/client roles with strict markers. |
docs/superpowers/specs/2026-08-14-legofs-two-riscv-type3-mesi-backinvalidation-design.md |
Adds the design/specification for the two-node back-invalidation proof. |
docs/superpowers/plans/2026-08-14-legofs-two-riscv-type3-mesi-backinvalidation.md |
Adds the implementation plan and acceptance checklist used to structure the work. |
configs/linux-cxl.config |
Extends kernel fragment with hotplug, ZONE_DEVICE, devdax, and network requirements. |
.gitmodules |
Adds the components/legofs submodule configuration. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
Comment on lines
+921
to
+924
| registrations = validate_registrations(read_coherence_trace(paths.coherence_trace)) | ||
| pre_benchmark_offset = paths.coherence_trace.stat().st_size | ||
| result["registrations"] = registrations | ||
| result["pre_benchmark_trace_offset"] = pre_benchmark_offset |
Comment on lines
+507
to
+511
| ack_ns = _required_integer(correlation["ack"], "monotonic_ns") | ||
| completion_ns = _required_integer(correlation["completion"], "monotonic_ns") | ||
| for direct_ns in direct_times: | ||
| for success_ns in success_times: | ||
| if direct_ns < snoop_ns <= ack_ns <= completion_ns < success_ns: |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What changed
qemu-system-riscv64 -M sifive_uguests with one file-backed 256 MiB CXL Type 3 SSD per nodessd-streambackend and records strict address, operation ID, and host-time evidenceWhy
The earlier path could boot the stack but did not prove that a Legofs direct write remained dirty in one guest and was returned by QEMU back-invalidation before the remote store completed. The server readiness probe also depended on an unconfigured loopback interface, and the evidence parser expected the dirty completion to repeat the snoop opcode instead of recording the real
SNOOP_ACKframe.Impact
A passing result now requires a node1-directed
SNP_DATA_INV, a 64-byte MODEL dirty ACK, a matching dirty completion, the same Legofs operation and mapping range, and the orderingdirect unmap < snoop < ACK < dirty completion < store success. Fallback I/O and coherence error counters must remain zero.Validation
python3 -m unittest discover -s tests -v: 52 passedcargo test -p badfs-bench -p badfs-server: passedstatus=passed, 1024 strict dirty-BI correlations, both QEMU processes overlapped, zero owned processes remainedThis is QEMU/TCG and CXLMemSim functional-model evidence. The SSD backing is simulated and does not claim physical CXL media durability or hardware performance.