Concurrent correctness properties

Concurrency Properties

Use this skill when testing operations that may execute in parallel across requests, workers, or webhook deliveries (e.g., concurrent credit redemptions, stock reservations, seat assignments, unique slug claims, or idempotent retries).

Why Random Seeds Alone Do Not Reproduce Races

A PRNG seed only fixes the generated inputs; OS thread scheduling and network I/O timing remain non-deterministic unless the test either:

1. Controls Interleaving Points: Uses deterministic schedulers (fc.scheduler in fast-check, barrier hooks, or controlled async promise queues) to systematically permute the order in which pending async steps resolve, OR
2. Synchronizes Simultaneous Contention: Uses a barrier (Promise.all / CountDownLatch / asyncio.gather) to fire $N$ conflicting operations against the same row/resource at the exact same instant and checks linearizability afterward.

Core Concurrency & Linearizability Invariants (Lamport)

1. Linearizability Against Sequential Specification:
   • When $N$ operations execute concurrently on the same entity (e.g., 5 parallel requests each trying to spend 40 credits from a 100-credit wallet), the final state and the set of [succeeded, rejected] responses must match some valid sequential ordering of those operations:
     • Exactly $\lfloor 100 / 40 \rfloor = 2$ requests may succeed; the remaining $3$ must fail with insufficient funds; final balance must be $20$ (never $-100$ or $60$).
2. Same-Key Concurrent Idempotency:
   • Firing $N \ge 2$ parallel requests with the exact same idempotency_key must result in at most one side effect / state mutation; all callers must either receive the single committed result or a clean conflict/in-progress status—never duplicate charges or duplicate records.
3. Conservation Under Contention (No Lost Updates or Write Skew):
   • Concurrent deposits, withdrawals, transfers, or inventory reservations across shared accounts must preserve the exact sum of balances and never overwrite each other's updates.
4. Deadlock & Orphan-Lock Freedom:
   • Generated transfers between accounts $(A \to B)$ and $(B \to A)$ in parallel must complete or abort cleanly within a bounded timeout without deadlocking or leaving stuck reservation locks.

Designing Concurrent Property Tests

• Keep concurrency fan-out small and targeted ($2$ to $5$ parallel operations hitting $1$ or $2$ shared keys): bugs that occur under 50 threads almost always manifest with $2$ threads and $1–2$ shared resources, which shrinks and debugs far faster.
• Log the exact resolution order (scheduler.report() or operation start/finish timestamps) whenever a counterexample occurs.

Checklist

• Are concurrent operations targeted at the same account, inventory item, or idempotency key to force real contention?
• Is the outcome verified to be linearizable (matching a valid sequential execution with exact balance/stock conservation)?
• Is async step ordering controlled or logged (e.g., via a deterministic promise scheduler or barrier) so race failures can be replayed?
• Are bidirectional operations ($A \to B$ and $B \to A$) tested for deadlock freedom and clean rollback?