Concurrency testing and schedule exploration

Take two atomic variables x and y, both initially zero. Thread A stores one to x and then loads y into a local result a. Thread B stores one to y and then loads x into b. First assume all four operations are sequentially consistent and the harness preserves each thread’s program order. A schedule is an interleaving of the two ordered pairs. Choose which two of the four positions belong to A; that gives six possible interleavings before any reduction.

The result a=b=0 is impossible under this SC model. For A to read zero, its load must precede B’s store in the single order. For B to read zero, its load must precede A’s store. Combined with the store-before-load order in each thread, those constraints form a cycle. If the implementation instead uses relaxed atomics, the zero-zero result can be allowed; enumerating only SC interleavings misses that behavior. Using unsynchronized plain C++ integers introduces data races and undefined behavior, not a valid relaxed-memory experiment.

A queue test can assign each produced item a unique identifier and check that accepted items are returned exactly once, respecting the required FIFO relation. Checking only a final item count misses duplication paired with loss. For a claimed linearizable object, record invocation and response intervals and test whether some legal sequential history respects real-time precedence. Overlapping calls may be ordered either way when the specification permits it; imposing one arbitrary ordering can falsely reject correct implementations.

State the harness boundaries explicitly: thread count, operation count, initial states, input values, allocation behavior, scheduling points, fairness assumptions, and language memory model. A bounded search that completes proves only that its explored model has no counterexample to that oracle within those bounds. It does not establish an unbounded progress property or cover omitted allocator reuse. Partial-order reduction can avoid schedules equivalent for the checked property, but requires a justified independence relation; it is not permission to skip inconvenient interleavings.

When exploration finds a failure, preserve both the input and the controlled execution decisions. Minimize the trace while keeping the failure: fewer threads, fewer items, and fewer preemptions make the violated invariant easier to see. A deterministic replay is especially useful for the last-item race, a missed wakeup, or a reclamation window. The harness must still model the synchronization operations actually used by the implementation; replacing real atomics with unrelated mocks can accidentally remove the bug.

Use complementary checks rather than treating one tool as universal. Dynamic race detection checks observed executions for certain races, while history checking addresses an abstract object specification. Stress tests exercise real allocation, hardware, and integration paths but provide uncertain schedule coverage. The probability lab illustrates only an assumed fixed independent chance of observing a failure per trial: predict the zero-failure bar as trial count increases. Real executions are often correlated and their failure probability is unknown, so the lab cannot certify the safety of concurrent software.