Re: [RFC] Property-based testing for Postgres

On Mon, 2026-11-03 at 08:28 -0800, Jeff Davis wrote:
> For something in core, I think a few strong examples in this area would
> be the best route.
>
> AI can create tons of these tests, and that some percentage will find
> bugs that others have missed, which is valuable. But carrying all those
> tests in core doesn't sound very appealing to me.
>
> Let's first look at the high-value testing areas and get feedback from
> the people that work in those areas.

Yes, complete agreement here.

I'm not proposing to carry a few hundred generated properties; the value isn't
the volume, it's a small number of properties that stand as a net under code
that is hard to get right and likely to be re-optimized. The scalar
round-trips in the first patch were a mechanism demo.

So, concretely, three examples in high-value areas, as the starting point for
the "get feedback from the people who work there" step you're asking for:

Example 1: a data-structure model test (binaryheap)

binaryheap.c is the shared binary heap behind merge append and the executor's
bounded sorts. A heap has a crisp model, a priority queue, so the test drives
the real structure and a trusted reference (a sorted array) through the same
random operations and requires they agree on a few properties:
* pop order is sorted,
* binaryheap_first() is the minimum, and
* a heap built incrementally (sift-up each) and one built with binaryheap_build
(Floyd's bulk heapify) pop in the same order.

Those are two different algorithms that must behave identically. A regression
test pins one hand-chosen input, this asserts the equivalence across every
input including the empty heap, a single element, all-equal values, and
INT_MIN/INT_MAX.

The hope is that if someone rewrites binaryheap_build it will fail the day it
diverges from the properties that define it and when it fails there will be a
minimal array and seed that reproduce the issue.

Example 2: a plan-results differential (nbtree index scans)

The skip-scan work (92fe23d93aa plus the long tail of follow-up fixes;
premature array advancement, NULLs advancing skip arrays, DESC commute
strategy, row-compare robustness) made nbtree scan-key handling a dense bug
surface.

The property is a differential oracle: the same query under a forced index scan
and under a forced sequential scan must return the same rows, over a
randomly-shaped index (column count, ASC/DESC, NULLS FIRST/LAST) and a predicate
mixing equality, inequality, IN-lists, and IS NULL, with a random ORDER BY
direction for backward scans.

The nice thing about PBT is that it does NOT need to know the right answer. It
never computes an expected row set, it only knows the two paths must agree, so
any divergence is a bug in the index path by construction. Plan results, not
plan shape EXPLAIN output is cost-model dependent and is not a target; the
rows a correct plan returns are.

Example 3: transaction isolation across concurrent backends (isolation)

MVCC is the case everyone agrees is tricky and worth a net, so this example
keeps that framing but drives it the way the bugs actually arise. Two
concurrent backends, each property asserting the documented guarantee of an
isolation level:

- under SERIALIZABLE, the classic write-skew pair (each txn reads a set and
writes based on it) cannot both commit. At least one must fail with a
serialization error. A phantom is likewise prevented;
- under REPEATABLE READ, a txn's repeated read returns the same value even
after a concurrent committed update (snapshot stability);
- under READ COMMITTED, a new statement sees a concurrently committed change
and not an uncommitted one;
- two txns locking rows in opposite order deadlock with exactly one victim.

The oracle is the documented guarantee, not a generated reference: a
SERIALIZABLE anomaly committing, a REPEATABLE READ snapshot shifting, or a
deadlock taking down both sessions would each be a serious isolation bug. The
interleaving between the two sessions is driven randomly, so this asserts the
guarantee holds across the schedules a fixed isolation spec does not enumerate.
An isolation spec pins one hand-written interleaving, this explores many.
The SSI write-skew in my first mail is exactly a multi-session schedule bug,
and ser_write_skew_prevented here is the property that corresponds to it. It
rounds out the set with a third distinct area: a data structure, an
access-method optimization, and concurrent transaction semantics.

These three are in the attached v2. It drops v1's scalar round-trips entirely
(base64, bytea, uuid, and the rest. The mechanism demo you rightly flagged)
and keeps only the plumbing plus binaryheap, nbtree, and isolation. But I
don't think the patch is the interesting artifact right now. The question you
posed is: which areas are worth a standing property, according to the people who
own them. The heap, nbtree, and the MVCC/SSI machinery are my guesses;
the committers in planner selectivity, SSI, and the executor would each have a
better one.

On Peter's reply in this thread: that's the case in point. A B-roll of
unreported correctness bugs, and the LP_DEAD-deletion-on-a-promoted-standby one
he attached is exactly the shape where a property earns its place, it's a
correctness invariant (an index must not drop an item a recovery-era snapshot
still needs) that no fixed regression test is likely to stumble onto, and it
lives in the nbtree/recovery area I'm pointing at. I'm not claiming the PBT
engine would have found that specific bug; I'm saying the area it's in is
precisely the "high-value, hard to get right, worth a net" category, and that
the AI wave Peter describes is the argument for having reproducible nets rather
than against it: a shrunk, seed-replayable counterexample is the artifact that
turns "AI found something odd" into "here is the minimal case, fixed."

> AI can create tons of these tests ... But carrying all those tests in
> core doesn't sound very appealing to me.

Agreed.

The discipline the README argues for is the guard against that. A property
belongs in core only where a disagreement is unambiguously a bug (a round-trip,
a model, two paths that must agree), and a good unit test beats a contrived
property. The job is to keep the set small and sound, not to let a generator
flood it. I'd rather land binaryheap, nbtree, and isolation, see whether the
heap, nbtree, and isolation folks find them worth keeping, and let that set
the bar for anything else.

best.

-greg