concurrency by daniel-noland · Pull Request #1762 · githedgehog/dataplane

daniel-noland · 2026-08-26T03:00:31Z

No description provided.

coderabbitai · 2026-08-26T03:00:40Z

Important

Draft PR not reviewed

Draft PRs are not automatically reviewed by default.

Trigger a manual review

To automatically review draft PRs, update your CodeRabbit configuration:

reviews:
  auto_review:
    drafts: true

_{Comment @coderabbitai help to get the list of available commands.}

codecov · 2026-08-26T03:25:04Z

Codecov Report

❌ Patch coverage is 85.34799% with 80 lines in your changes missing coverage. Please review.
✅ All tests successful. No failed tests found.

Files with missing lines	Patch %	Lines
tracectl/src/evidence.rs	80.89%	55 Missing and 5 partials ⚠️
config/src/external/overlay/completeness.rs	90.34%	14 Missing and 3 partials ⚠️
nat/src/icmp_handler/nf.rs	81.81%	0 Missing and 2 partials ⚠️
dpdk/src/acl/context.rs	87.50%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!

First step of the multi-worker work: find out whether the pipeline can be driven inside a model-checked execution at all. It cannot, and the obstacle is not DPDK's opacity but one process-global lock, which the module docs set out. The three-case lock test exists to make that attributable rather than to assert anything interesting on its own. Its failing third case is written out rather than run: shuttle aborts the process instead of failing a test, so a live one would take the suite down with it. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

A `concurrency::sync` mutex in a `static` typechecks under loom and shuttle and then aborts the process, because the primitive belongs to the execution that created it and a `OnceLock` outlives every execution. `OnceLock` is what the concurrency crate recommends for the separate problem that `Mutex::new` is not `const fn` there, so the advice and the hazard point in opposite directions and nothing says so. This unblocks driving the pipeline under shuttle: every `Fabric` builds ACL contexts and so took this lock. Revisit if loom and shuttle ever make `Mutex::new` const. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The facade documented `OnceLock` as the workaround for `Mutex::new` not being `const fn` under the model checkers. It resolves that compile error and leaves a worse one, which nothing said: the second execution to take the lock aborts the process. `dpdk` followed the advice and was the only instance. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

A pipeline per thread needs one reader per thread. The readers this already published cannot serve: they hold `NonNull` table pointers and a `Cell` counter, and the fib readers cache `Rc<UnsafeCell<FibGroup>>`, so none of them is `Send` or `Sync` -- nor is `RouterTables`. A factory crosses the boundary and each thread makes its own reader, which is how `start_router` feeds its workers. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…worker A `Fabric` interleaved writer creation with stage assembly, so one configuration could only ever produce one pipeline and no property here could be about more than one worker. Which of the three parts may cross a thread boundary, and why only that one, is on `Blueprint`. The `nat` and `routing` re-exports are part of the same change: a blueprint has to name the reader-factory types in a field, and outside those crates they could not be named at all. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…ator The first property here that runs in the arrangement production runs in: two pipelines, one allocator, one flow table. It discriminates a lost update in the port-block claim. The measurement that says shuttle rather than the sanitizer is what catches it -- and what shuttle still cannot see -- is recorded on the test. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`table_name` promised process uniqueness and, under a model checker, did not deliver it. The counter was the concurrency facade's atomic, which belongs to the execution that created it; `rte_acl`'s registry is process-global and resets for nobody. Found by `dataplane::packet_processor::fuzz::model`, which lowers many configurations per process and so was the first thing to notice. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

bolero becomes the outer loop over the same draw the single-threaded generated property uses, so a shape reachable on one thread is reachable on two by construction. Measured against a deliberate allocator defect: this property does not catch it and the targeted one does. Both the measurement and the reason are on the test, because "the generated property covers that too" is the assumption it refutes. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Tests can now hold a recording that dumps the spans and events leading to a panic. It cannot be asserted on: there is no way to read the trace back into the program, and the module explains at length why that is the feature rather than a missing one. Three things about it were measured rather than assumed, and are written down where the next person will need them: which targets drown a dump under a model checker, that `#[instrument]` on the packet path captures whole `Packet` values, and that a scoped subscriber cannot exist under loom or shuttle at all. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The arrangement receive-side steering normally puts the gateway in, and the one no property here has ever been in: a reply's tuple is the request's reversed, so the return traffic of a flow opened on one worker routinely lands on another. The oracle is the existing `Conversation::judge_reply`, reused rather than restated. The limits of what this property isolates are recorded on the test itself, since it does not discriminate the crossing from the flow handling. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Both handlers re-read the same `RwLock`, and so does the `Display` behind the `logfmt()` in their debug lines, so the guard made those recursive acquisitions. `parking_lot` gives no recursion guarantee, and writers on this lock are ordinary data-path traffic; one of the two acquisitions being a log line means the window only opens when tracing is turned up. Found by the new model property below, which shuttle refused outright. Real threads had passed it every time. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Production's third thread. Every property before this froze the tables before sending a packet, so left-right under `FibTableReader` -- and the per-thread `Rc<UnsafeCell<FibGroup>>` cache behind it -- had never been asked to publish while a reader was mid-lookup. `Fleet` stops owning the `RouterTables` to make it possible: a fleet is shared by reference with every worker, so whoever wants to change a route cannot also be borrowing it through one. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The route-churn property states a frame condition, so it can only ever say that publishing did no harm. Aiming the churn at the route under test needs a claim with a lower bound as well, and the fib's in-place next-hop update -- which writes through an `UnsafeCell` every route already points at -- is the part of it whose safety argument had never been exercised. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The overlay half of config-apply-under-load. `Fleet::reconfigure` re-stores through the writers a running worker already reads, which is what production does and what rebuilding a fleet would not be. Written twice: the first shape overlapped nothing on the plain backend and passed for that reason. See the doc comment: rounds are what make the passing case mean something, and it records the two ways of provoking a failure that were tried and discarded, each of which looked conclusive and was not. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The design note proposed checking completeness against real configurations. That answers the wrong question -- the algebra's address plan is a function of its handles, so no real configuration is expressible and the report is "0% reachable". Per degree of freedom instead, with the fuzzer supplying the evidence and the survey's exhaustive destructuring stopping the build if the schema grows a field nobody classified. Reports thirteen of twenty-seven degrees of freedom fixed. Nothing acted on yet; the note names the four worth doing first. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

… touch The frame condition over a configuration that actually changes, with the frame taken from the algebra rather than guessed at. `X => A.X` from one draw split at its last operation. Round 1 races the change and is counted, not asserted: it fails about one run in twenty, and the doc comment records what was measured and what is still unknown. Rounds after it race a re-enactment and carry the full claim. Two harness faults found on the way and fixed here, both of which made earlier properties in this module prove less than they appeared to: a worker panicking between barriers hung the run instead of failing it, and the genid was pinned at 1 across enactments, which told the nat allocator no configuration ever changed and manufactured two symptoms that are not the dataplane's. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`Fleet` published neither: the nat allocator was told generation one on every enactment, and the stages were never told at all, because `Blueprint::worker` built its pipeline without `set_data`. The second also meant the flow revalidation path -- the code that exists for a configuration changing under live flows -- was unreachable from every property in this module. Also separates the two workers' five-tuples by disjoint halves of the port space rather than by an offset, which two drawn ports could cancel; `enact` performs config-apply one step at a time, for attributing a disturbance to one; and the ordering now follows `mgmt`, where the generation is published last on purpose. Found by `just fuzz` on this target. The random engine `cargo test` runs cannot get here: it was the coverage-guided corpus that produced the crashing inputs these were diagnosed from. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`-Cunsafe-allow-abi-mismatch=sanitizer` disabled rustc's check that every crate agrees about sanitizer flags -- the check that refuses a half-instrumented link. `tests.pkg.dataplane` builds and links without it under `--argstr sanitize thread`, so there was nothing to excuse: `std` is rebuilt from source by `-Zbuild-std` under the same sanitizer as the rest. The sysroot now records what it was built for, and `just fuzz` refuses when that disagrees with the sanitizer it was asked for. The two knobs are independent and a mismatch produced a binary whose green run meant nothing. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…s against A short burst right after the barrier measured when the allocator swap landed rather than what it did: `Everything` spends about a millisecond rebuilding rte_acl before reaching the allocator, by which time the burst was over, so it looked fifty times safer than the masquerade step alone. Sustained, the two are the same order. Also models the router-config await `mgmt` performs between the allocator swap and the generation publish, which turns out to change nothing -- the doc comment records that and what thread sanitizer said, which was nothing, on a build that instruments dpdk and rebuilds std. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The transient the step instrument attributed to the masquerade store is a dataplane defect, not a harness one: an allocator swap can give one public tuple to two live flows, and a reply then reaches the wrong tenant conversation. `set_randomize(false)` was the last deviation this harness had from `mgmt::apply_masquerade_config` and was the obvious suspect. It is not the answer -- the instrument now runs both settings, with the running allocator primed so the swap under test is random-to-random. Signed-off-by: Daniel Noland <daniel@githedgehog.com> Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…r opengrep Two different answers, because there are two different cases. The properties in `packet_processor::fuzz` go through the facade. Some of them run under `concurrency::model_test`, and the `Barrier` two of them synchronise their workers on was a real `std::sync::Barrier` -- invisible to the model checker, which is the case the facade exists for rather than a lint nit. The rest are deliberate and stay, with the suppression the rule provides and the neighbouring code already uses: a model-checked mutex cannot live in a `static` (`dpdk`, `flow-filter`), and an instrumented diagnostic would perturb the schedule it is meant to report on (`tracectl`). Signed-off-by: Daniel Noland <daniel@githedgehog.com>

daniel-noland force-pushed the pr/daniel-noland/pipeline-harness branch from 8cb37c3 to 8027a81 Compare August 26, 2026 17:30

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 8e14aad to 68de4de Compare August 26, 2026 17:30

daniel-noland force-pushed the pr/daniel-noland/pipeline-harness branch from 8027a81 to cf9c73e Compare August 26, 2026 19:36

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 68de4de to bcbd57a Compare August 26, 2026 19:36

daniel-noland force-pushed the pr/daniel-noland/pipeline-harness branch from cf9c73e to fdb5ee2 Compare August 26, 2026 20:41

daniel-noland force-pushed the pr/daniel-noland/model-checking branch 3 times, most recently from be74286 to 95dd658 Compare August 26, 2026 21:13

daniel-noland force-pushed the pr/daniel-noland/pipeline-harness branch 2 times, most recently from 033504b to f2eee32 Compare August 26, 2026 21:25

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 95dd658 to 6446c90 Compare August 26, 2026 21:25

daniel-noland force-pushed the pr/daniel-noland/pipeline-harness branch from f2eee32 to d1f4f0d Compare August 27, 2026 01:29

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 6446c90 to e58b3d3 Compare August 27, 2026 01:29

daniel-noland force-pushed the pr/daniel-noland/pipeline-harness branch from d1f4f0d to b712bef Compare August 27, 2026 01:41

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from e58b3d3 to bc6dcbb Compare August 27, 2026 01:41

daniel-noland force-pushed the pr/daniel-noland/pipeline-harness branch from b712bef to 66a7cd4 Compare August 27, 2026 02:25

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from bc6dcbb to 829e3f8 Compare August 27, 2026 02:25

daniel-noland force-pushed the pr/daniel-noland/pipeline-harness branch from 66a7cd4 to 67eba5b Compare August 27, 2026 04:37

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 829e3f8 to 40659a3 Compare August 27, 2026 04:38

daniel-noland force-pushed the pr/daniel-noland/pipeline-harness branch from 67eba5b to 0294067 Compare August 27, 2026 05:12

daniel-noland force-pushed the pr/daniel-noland/model-checking branch 2 times, most recently from 3a81a5b to 93cb81d Compare August 27, 2026 06:30

daniel-noland force-pushed the pr/daniel-noland/pipeline-harness branch 2 times, most recently from 11b3757 to 7346f90 Compare August 27, 2026 18:00

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 93cb81d to 7295f75 Compare August 27, 2026 18:00

daniel-noland force-pushed the pr/daniel-noland/pipeline-harness branch from 7346f90 to fac79e0 Compare August 27, 2026 18:29

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 7295f75 to bdaa96a Compare August 27, 2026 18:29

daniel-noland force-pushed the pr/daniel-noland/pipeline-harness branch from fac79e0 to 1f1d323 Compare August 28, 2026 02:13

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 0f92aff to f1b4016 Compare August 28, 2026 07:08

daniel-noland force-pushed the pr/daniel-noland/pipeline-harness branch from 7a31802 to 70f9fbc Compare August 28, 2026 07:31

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from f1b4016 to 3d615e7 Compare August 28, 2026 07:31

daniel-noland force-pushed the pr/daniel-noland/pipeline-harness branch from 70f9fbc to 6ee839b Compare August 28, 2026 07:43

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 3d615e7 to 42579bb Compare August 28, 2026 07:43

daniel-noland force-pushed the pr/daniel-noland/pipeline-harness branch from 6ee839b to 747e32e Compare August 28, 2026 09:14

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 42579bb to 76341eb Compare August 28, 2026 09:14

daniel-noland and others added 21 commits August 28, 2026 11:14

daniel-noland force-pushed the pr/daniel-noland/pipeline-harness branch from 747e32e to 706cc12 Compare August 28, 2026 17:16

daniel-noland force-pushed the pr/daniel-noland/model-checking branch from 76341eb to 04fa51a Compare August 28, 2026 17:16

Navigation Menu

Uh oh!

concurrency - #1762

concurrency#1762
daniel-noland wants to merge 21 commits into
pr/daniel-noland/pipeline-harnessfrom
pr/daniel-noland/model-checking

daniel-noland commented Aug 26, 2026 •

edited

Loading

Uh oh!

coderabbitai Bot commented Aug 26, 2026

Draft PR not reviewed

Uh oh!

codecov Bot commented Aug 26, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

daniel-noland commented Aug 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

coderabbitai Bot commented Aug 26, 2026

Draft PR not reviewed

Uh oh!

codecov Bot commented Aug 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

daniel-noland commented Aug 26, 2026 •

edited

Loading

codecov Bot commented Aug 26, 2026 •

edited

Loading