[DOC][RFC] property-based testing

[devarajabc]

Property-Based Testing in jserv/rbtree

The jserv/rbtree test suite leverages property-based testing (PBT) to verify the correctness, consistency, and robustness of its red-black tree implementation. PBT is achieved by encoding data structure invariants as executable specifications and systematically generating diverse test cases to check those invariants across a wide range of scenarios.

This document explains:

• How properties are specified and checked

• How test cases are generated

• How the framework validates correctness and detects subtle bugs

---

1. Specification Definition

jserv/rbtree defines four property types, each with a dedicated mechanism to check correctness:

Property Type	Goal	rbtree Example
Classical	Maintain internal invariants	5 red-black properties always hold
Round-trip	Operations cancel out or restore state	insert+delete = no-op
Catastrophic	No crash under bad input	Delete non-existent keys won't segfault
Differential	Cross-check correctness	Cached tree vs. Standard tree

1.1 Classical Properties

The 5 classical red-black tree invariants are explicitly tested in multiple locations:

• Root is black
• Red nodes have black children
• Every path to a leaf has the same number of black nodes
• Nodes are in in-order traversal order
• If a node N has exactly one child, the child must be red

The Classical Properties for binary search tree

• For every node, all values in its left subtree are less than the node's value, and all values in its right subtree are greater than the node's value

Ref : Property-Based Testing in Practice

[jserv]

Don't post content generated by ChatGPT (or other LLMs) unless you can fully confirm its accuracy.

Looking at rand_u32 function below in tests/rb-tests.c, this is not a pure Linear Congruential Random Number Generator (LCRNG), though it does incorporate some LCG-like elements.

/* Fast 32-bit RNG - rapidhash variant
 * Reference: github.com/Nicoshev/rapidhash
 */

/**
 * Advance state and return a new 32-bit pseudo-random value
 *
 * @state : Pointer to RNG state (modified)
 * Return New pseudo-random 32-bit value
 */
static inline uint32_t rand_u32(uint32_t *state)
{
    *state += 0xe120fc15u;
    uint64_t tmp = (uint64_t) (*state) * 0x4a39b70d;
    uint32_t mix = (uint32_t) ((tmp >> 32) ^ tmp);
    tmp = (uint64_t) mix * 0x12fad5c9;
    return (uint32_t) ((tmp >> 32) ^ tmp);
}

It is not a “pure” LCG in the usual sense of state transition and output are both the linear-congruential value.

Internally the state update is indeed linear-congruential with parameters $a=1$, $c=0xe120fc15$, modulus $2^{32}$. That is an additive LCG (sometimes called a Weyl sequence). However, the value returned to the caller is not that state. It is the state after it has been passed through two rounds of multiplicative/xor-mix hashing identical in spirit to SplitMix32. Those nonlinear mix steps destroy the simple linear structure that characterises a classic LCG’s output stream, so the function is better described as “counter-based RNG with SplitMix-style output permutation” (or, as the comment says, a Rapidhash variant) than as an LCG.

So, while the underlying recurrence is linear, the generator a caller sees is emphatically not an LCG.

Pure LCRNG would look like:

static inline uint32_t rand_u32_lcg(uint32_t *state)
{
    *state = (*state * 0x4a39b70d + 0xe120fc15u);
    return *state;
}

[devarajabc]

Remove the "Unsure Part".