Mini Checker: Precedence, Orders, Register Rule Diagram

Precedence first, order second

Record every op with invoke time and return time; pending ops keep no return
Draw real-time precedence: op done before another starts must come first
Overlapping ops may linearize in any order: that freedom is the whole search

The register rule per order

Walk each candidate order: a read returns the latest preceding write
A stale read after a completed write rejects that order, not the history yet
A timed-out write is indeterminate: the checker tries both branches

What sampling cannot prove

Bounded search fits small histories; production traces need sampling plus model checks
A passing sample never proves the next execution linearizable
Pair the checker with version probes and divergence monitors in production