test(ublk): porcupine linearizability on concurrent reads/writes

[ValentaTomas]

Stacked on: #27 (tests/rapid-state-machine).

Adds TestRapidLinearizability (in ublk/porcupine_integration_test.go) — a porcupine-driven linearizability checker for concurrent reads and writes against a single ublk device.

Why this catches things rapid alone doesn't

TestRapidStateMachine (PR #27) checks a per-operation invariant: after every action, the device's bytes match the model's shadow. That's sufficient when the test driver issues actions sequentially — which it does, because rapid state machines are sequential by construction.

This PR addresses a different question: can the global real-time history of concurrent ops be explained by some valid sequential ordering? That's linearizability, the same property Jepsen checks for distributed databases. A history can pass the per-operation invariant on every read taken in isolation and still be non-linearizable — e.g. if two concurrent writes' effects are observed in inconsistent orders by later reads.

Implementation choice — Option B

Both options outlined in the spec were on the table:

• Option A would have instrumented TestRapidStateMachine to record an operation history. The problem: rapid drives the actions strictly sequentially, so the history is trivially linearizable and the porcupine check is pure overhead.
• Option B (chosen): a standalone test in its own file driving a concurrent worker pool. The rapid state machine is preserved untouched as the per-operation invariant checker; this test is the global-ordering checker. Cleaner separation of concerns and avoids forcing PR test(ublk): rapid property-based state-machine tests #27's test into a shape it doesn't want.

The model

One register per 4 KiB block (map[int]uint64 — block index → most-recent stamp). Each write embeds a unique 8-byte stamp (from a global atomic counter starting at 1) at the start of its 4 KiB block; reads recover the stamp from the bytes returned. Reads/writes are constrained to a single block at a time so each op is atomic from the model's perspective. Stamp 0 is reserved for "never written", which matches the all-zero bytes the device returns for unwritten blocks.

The workload

• Single 256 KiB device (64 blocks of 4 KiB).
• Default 4 concurrent goroutines × 50 ops each (200 ops total).
• Each op:
  • Call = time.Now() recorded immediately before the syscall.
  • Issues unix.Pread/unix.Pwrite against /dev/ublkbN with O_DIRECT and alignedBuf.
  • Return = time.Now() recorded immediately after.
  • Appended to a mutex-protected []porcupine.Operation.
• After the workload phase: porcupine.CheckOperationsVerbose(model, history, 30s). Illegal histories are rendered to a HTML visualization via porcupine.VisualizePath and the test fails with the path logged. Unknown (timeout) is logged as a soft pass with guidance to either shrink the history or grow the budget.

Tunables: UBLK_LINZ_OPS (default 200) and UBLK_LINZ_WORKERS (default 4).

Tooling

• make test-linz runs only this test against an integration-tagged binary.
• No new CI job needed: the existing test-integration job already runs every //go:build integration test in ./ublk/. Verified in .github/workflows/ci.yml.
• TODO.md "Linearizability checking" bullet replaced with a (done) summary.
• Pinned dependency: github.com/anishathalye/porcupine v1.1.0.

fd-close-before-Close discipline

Per AGENTS.md: the user fd opened on /dev/ublkbN is closed before dev.Close() (in a t.Cleanup), otherwise del_gendisk blocks waiting for the open ref to drop. Documented inline.

Test plan

• go vet ./...
• golangci-lint run ./... → 0 issues.
• go test -count=1 -race ./ublk/uring/ ./ublk/
• go test -c -tags=integration -o /tmp/ublk.test ./ublk/ compiles
• gofmt -l . empty
• go mod tidy -diff clean
• CI's test-integration job exercises TestRapidLinearizability end-to-end on a host with ublk_drv + root.
• (Optional) Manual sanity check: make test-linz on a kernel host; should pass and log linearizable: 200 ops checked in <Xs>.

Forbidden checks

• No library code touched (ublk.go, worker.go, device.go, types.go, ublk/uring/* untouched).
• PR ci: bump actions/checkout from 4 to 6 #1 (fuzz_test.go) and PR ci: bump codecov/codecov-action from 4 to 5 #2 (chaos_integration_test.go) files not modified.
• No t.Skip for missing root or kernel.
• TestRapidStateMachine and the rest of PR test(ublk): rapid property-based state-machine tests #27 untouched (additive only).

[cursor]

PR Summary

Low Risk
Low risk because changes are limited to tests/tooling and a new test-only dependency, with no production code changes. Main risk is longer or flaky integration runs due to timing- and concurrency-sensitive checking.

Overview
Adds an integration-tagged TestPorcupineLinearizability that drives concurrent pread/pwrite workloads against a ublk device, records a real-time history, and checks it with github.com/anishathalye/porcupine (with HTML visualization on failure and a soft-pass on checker timeout).

Updates go.mod/go.sum to include Porcupine, adds make test-linz to run only this test, and removes the corresponding now-completed linearizability TODO entry.

^{Reviewed by Cursor Bugbot for commit 94bf7da. Bugbot is set up for automated code reviews on this repo. Configure here.}

[cursor]

Cursor Bugbot has reviewed your changes and found 1 potential issue.

^{Bugbot Autofix is ON, but it could not run because the branch was deleted or merged before autofix could start.}

^{Reviewed by Cursor Bugbot for commit 94bf7da. Configure here.}

[cursor]

Timeout guidance says "increase" but means "decrease"

Low Severity

The timeout log message says "increase UBLK_LINZ_OPS to keep histories small" but UBLK_LINZ_OPS controls the total number of operations — increasing it makes the history larger, making timeouts more likely. The guidance is inverted and would lead a developer to worsen the problem. It needs to say "decrease".

 

^{Reviewed by Cursor Bugbot for commit 94bf7da. Configure here.}