Skip to content

DDIR: a differential-testing sweep over random lambda programs - #980

Merged
frankmcsherry merged 1 commit into
TimelyDataflow:master-nextfrom
frankmcsherry:ddir-difftest
Oct 22, 2026
Merged

frankmcsherry merged 1 commit into
TimelyDataflow:master-nextfrom
frankmcsherry:ddir-difftest

Conversation

@frankmcsherry

@frankmcsherry frankmcsherry commented Oct 20, 2026 •

Copy link
Copy Markdown
Member

Now directly on master-next. One commit; it no longer waits on #981 or #982. It adds interactive/tests/difftest.rs and a pointer in interactive/README.md, and nothing outside tests changes. #978 and #986 fixed bugs this harness found, and #981/#982 fix the one it found that is still open (below).

What it is. An #[ignore]d test that generates random, well-typed lambda programs over random update streams. Each case is checked against oracles that need no reference implementation.

  • Programs: declared inputs of several shapes; map, value, filter, flatmap, join, negate, concat and difference, arrange, the reductions, delay, join_function; small and nested iterative scopes.
  • Feeds: 3–30 epochs of inserts and retractions over small values, so keys collide. Some cases use ints of every storage width; some have one big epoch.

The oracles, each comparing every export after every epoch with another way of computing it:

  • workers: 2–5 workers against 1.
  • scratch: the accumulated input evaluated from scratch.
  • optimize: the program unoptimized.
  • delta: every join as a delta join.
  • ahead: every row fed up front at its future time.
  • split and bind: the program cut into a producer and a consumer. The consumer imports what the producer publishes, as containers or arrangements (split), or has its inputs bound to the producer's traces (bind).
  • reinstall: the split consumer dropped, and installed again later. Off for now, see below.
  • explain: every row regenerated by its explanation alone.
  • On one worker, every snapshot also round-trips through a binary frame and feed text, taps sum to the contents, and a keyed peek matches the contents at its key.

Off until #982: late installs. One switch, LATE_INSTALLS, is false.

Running it. A seed always generates the same case. A failure is minimized and printed as a case file, with the rows each side has that the other lacks and the commands that replay it, by seed or from the file. The module docs cover running, picking oracles and replaying.

DIFFTEST_SEED=0 DIFFTEST_CASES=1000 cargo test --release -p interactive --test difftest -- --ignored --nocapture
  • DIFFTEST_ORACLES=workers,delta runs only those oracles.
  • DIFFTEST_SEED=<seed> DIFFTEST_CASES=1 replays one case.
  • DIFFTEST_CASE_FILE=<file> checks a printed case, edited by hand if you like.
  • With every oracle on, it runs about 25 cases a second.

What it skips, deliberately

  • The explain oracle skips programs that read or set times, whose answers depend on arrival.
  • A min loop's step filter reads the node or the label, never both. A filter that weighs a label against the node it flows to isn't label propagation. A node can hold a label it can't pass on, in place of one it could, and the loop need not have a fixed point. Sweep seed 5021723 cycled with period 3; a plain simulation of the program confirms it, and DDIR computed it correctly.

Checks:

🤖 Generated with Claude Code

https://claude.ai/code/session_019XsakwFGwtESwZ1gSYwG4o

tests/difftest.rs, an ignored test: random, well-typed lambda programs over
random update streams (inserts, retractions and repeated rows over small
values so keys collide, ints of every storage width, floats, a declared
sum, list keys, long and big epochs), checked against oracles that need no
reference implementation. Each compares a program's exports after every
epoch with another way of computing them: two to five workers; evaluating
the accumulated input from scratch; the unoptimized program; every join as
a delta join; every row fed ahead at its future time; the program split
into a producer and a consumer that imports (as containers or
arrangements) or binds; and explanations regenerating each row. On one
worker every snapshot also survives a binary frame and a feed-text round
trip, taps sum to the contents, and a keyed peek is the contents at its
key.

A seed always generates the same case. A failure is minimized and printed
as a case file, with the rows each side has that the other lacks and the
commands that replay it, by seed or from the file. interactive/README.md
points to it. Run with
DIFFTEST_SEED=0 DIFFTEST_CASES=1000 cargo test --release -p interactive \
  --test difftest -- --ignored --nocapture

Late installs are off (`LATE_INSTALLS`): the consumer of `split` and `bind`
is installed with its producer, and the `reinstall` oracle (drop the
consumer, install it again later) does not run. A consumer installed late
imports traces whose history has been compacted, and does not converge
until each import reads its trace as of the time it starts (TimelyDataflow#982). The late
epoch is still drawn, so turning the switch on changes no case.

The explain oracle skips programs that read or set times, and big epochs
that explode a collected list, which is quadratic in explain's flatmap
lookup.

A `min` loop's step filter reads the node or the label, not both. One that
weighs a label against the node it flows to is not label propagation: a node
can hold a label it cannot pass on in place of one it could, and the loop
need not have a fixed point (sweep seed 5021723 cycled with period 3, which
a plain simulation of the program confirms; DDIR computed it correctly).

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019XsakwFGwtESwZ1gSYwG4o
@frankmcsherry
frankmcsherry merged commit 96c8508 into TimelyDataflow:master-next Oct 22, 2026
7 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant