METHODS & TOOLS / INTERACTIVE EDITION · ETCD 3.6.6

History workbench

Can these completed operations belong to one legal register execution?

Illustrative model check — not real cluster telemetry

One integer register, initial 0. Reads return the current value; writes replace it. All operations are completed, each client is sequential, and intervals use one comparable clock. No pending/timeout calls, transactions, causality messages or leases.

Choose a history

Completed operations (JSON; value is write input or read result)

id and client: nonempty strings. type: read/write. value: safe integer. start/end: finite numbers, start < end. Same-client intervals cannot overlap. Inputs stay in your browser; no storage or analytics.

Model
Search states (1–100,000)

How to read the answer

PASS gives one witness order. FAIL means every legal order was exhausted under this model. INCONCLUSIVE means the 12-operation size cap or search budget was reached; it is never counted as a pass. INVALID means malformed or unsupported input. A passing finite history does not prove an implementation correct.

The search enumerates topological orders of precedence edges and the register state, memoizing chosen-set/value pairs. Real-time precedence uses end ≤ next start. Sequential mode retains only same-client edges. See chapters 2–3 for interpretation and the downloaded source for the independent permutation-oracle tests.