Find a legal sequential explanation that respects real-time order

If operation a responds before operation b is invoked, any legal linearization must place a before b. If their intervals overlap, the order of their response events alone does not determine their abstract effect order. A slow response can belong to an operation that took effect earlier. The checker must find an order satisfying both the required precedences and the sequential specification's results. For a register, writes update one value and reads return the most recent preceding write in that sequential order, starting from the declared initial value.

Capture invocation and response boundaries in a harness with a justified ordering mechanism, or preserve reliable causal edges. Comparing unsynchronized timestamps from separate machines can manufacture false non-overlap edges. Operation identity, arguments, result type, and client order also belong in the history. A timeout may mean the operation did not execute or that its response was lost; the API's semantics determine how it should be represented. Treating every timeout as a known no-effect failure can make a legal execution appear inconsistent or conceal an actual contract violation.

For an incomplete history, the standard definition permits adding responses to some pending invocations, then considering the completed portion. The resulting sequential history must match each retained operation's arguments and return value, preserve per-client behavior, and respect required real-time precedence. Already completed successful operations cannot simply be dropped because they make the check difficult. A pending write may explain a later read if a suitable completion and ordering exists, even though the original client never received a response. This captures uncertainty about execution without declaring uncertainty equivalent to failure.

Retries require a deliberate object contract. Two transport calls with the same idempotency identity may represent attempts at one logical effect, while ordinary register writes are separate operations even when their values match. The checker model must encode whichever semantics the service promises. Similarly, a history of individual key operations does not automatically establish multi-key transaction guarantees. State the object scope, initial state, result meanings, and failure classification. A checker reporting unknown or exhausting resources has not produced either a valid sequential witness or a definitive violation.

A rejected complete history with sound capture and a correct sequential model is a concrete inconsistency witness. A passing finite history shows that at least one legal explanation exists for that history; it does not show that every untested schedule will pass. General linearizability proofs must connect all allowed implementation executions to the abstract object, often through invariants and refinement. Crash durability is a further contract dimension: ordinary linearizability does not, by itself, specify which state survives a machine or storage failure. Include those semantics when the service promises them.

The modular instrument supplies a tiny sequential reference operation: add one modulo four. Reset, set m=4 and a=1, predict the sequence 0,1,2,3 after zero through three transitions, then take three Steps. Its state sequence is legal by construction and contains no invocation intervals or overlapping clients. It therefore cannot check linearizability, pending responses, or durability. The value of the illustration is narrower: a concurrent history needs a sequential contract to explain its observations, and that contract must be stated before a checker can search for an explanation.