Order and commutativity

Most units are called by people, one request at a time, in the order things happened. Some are fed by another system instead: a scanner, a payment provider, a telephone switch, each sending events as they occur. A feed cannot promise order. Events arrive late, out of order, and, because a sender retries until it hears back, sometimes twice. A unit fed by events has to end in the same state whatever order they come in.

That property has a name. Two calls commute when making them in either order leaves the same state. A unit can declare that some of its contracts commute, and the verifier looks for the pair that does not.

Declaring it

A parcel tracker keeps, for each parcel, the first and the last time a scanner saw it:

row Parcel { id: id, first: int(0, 1000), last: int(0, 1000) }
unit Tracking {
    state parcels: Parcel[4];
    commutes { scanned };
    contract scanned(parcel: id, at: int(1, 1000)) {
        case parcel in parcels => Seen: parcels[parcel].last := at;
        else => Seen: parcels += [Parcel { id: parcel, first: at, last: at }];
    }
}

commutes { scanned }; declares that calls to scanned commute with each other. A set may name several contracts of the unit, commutes { picked_up, delivered }; the verifier draws the same contract twice as readily as two different ones, so a set of one is a real question.

What the verifier does with it

From a sampled state, the verifier draws two calls from the set, each with its own sampled arguments, and makes them in both orders on two copies of the state. Two successes that leave different states are a counterexample, and so is one order that succeeds while the other fails. When both orders fail, there is nothing to compare, and the verifier moves on.

verify FAILED: 1 failure(s):
[1] Tracking: scanned(9, 226) and scanned(9, 231) do not commute: the two orders leave different states
  scanned(9, 226) then scanned(9, 231): Tracking { parcels: [Parcel { id: 1, first: 876, last: 223 }, Parcel { id: 3, first: 369, last: 25 }, Parcel { id: 5, first: 281, last: 42 }, Parcel { id: 9, first: 226, last: 231 }] }
  scanned(9, 231) then scanned(9, 226): Tracking { parcels: [Parcel { id: 1, first: 876, last: 223 }, Parcel { id: 3, first: 369, last: 25 }, Parcel { id: 5, first: 281, last: 42 }, Parcel { id: 9, first: 231, last: 226 }] }
  state Tracking { parcels: [Parcel { id: 1, first: 876, last: 223 }, Parcel { id: 3, first: 369, last: 25 }, Parcel { id: 5, first: 281, last: 42 }] }

Read it. The state has no parcel 9, and the two calls are scans of parcel 9 at 226 and at 231. In the order they happened, the row says first 226, last 231. In the other order, the scan at 231 creates the row and the scan at 226 overwrites last: the parcel was last seen before it was first seen. With :=, the last scan to arrive wins, not the last scan to happen. The other three rows are whatever the sampler drew, and they are the same in both states; only parcel 9 differs.

Updates that commute by construction

x max= e sets x to the larger of x and e, and x min= e to the smaller. A maximum does not care about order: the larger of three times is the same whichever two were compared first. So a case whose deltas are max= and min= commutes by construction. The fix is the first case’s line; the example and the scenario are new too, and the next sections read them.

row Parcel { id: id, first: int(0, 1000), last: int(0, 1000) }
unit Tracking {
    state parcels: Parcel[4];
    commutes { scanned };
    contract scanned(parcel: id, at: int(1, 1000)) {
        case parcel in parcels => Seen: parcels[parcel].first min= at, parcels[parcel].last max= at;
        else => Seen: parcels += [Parcel { id: parcel, first: at, last: at }];
        examples {
            { parcels: [Parcel { id: 1, first: 100, last: 300 }] } (1, 300) => Seen;
        }
    }
}
scenario a_late_feed {
    Tracking.scanned(1, 300) => Seen;
    Tracking.scanned(1, 100) => Seen;
    Tracking.scanned(1, 300) => Seen;
}

scenario a_late_feed
  Tracking.scanned(1, 300) => Seen
  Tracking.scanned(1, 100) => Seen
  Tracking.scanned(1, 300) => Seen
  Tracking = Tracking { parcels: [Parcel { id: 1, first: 100, last: 300 }] }
3 step(s), all as expected

verify: 1 examples, 3 scenario steps, 2000 sampled checks and 1000 commutativity checks passed

The scenario sends a scan at 300, a late one at 100, and the one at 300 again. The row ends with the truth, first 100 and last 300. The verifier’s line has a new count, a thousand commutativity checks, next to the examples, the scenario steps and the sampled checks.

Idempotence: the same call twice

A repeated event is the feed’s other habit. A call is idempotent when making it twice leaves the state that making it once leaves. max= and min= are idempotent as well: the larger of 300 and 300 is 300. The example says so for one state: the scan at 300, sent again to a row that already has it, answers Seen and names no after-state, which means nothing changed, and the verifier holds the example to that.

The commutativity check does not stand in for that example. Count the scans as well, with scans += 1 (the program is book/failures/order-count.vish). Addition commutes, so every commutativity check still passes. But a scan delivered twice is counted twice, and the example catches it:

verify FAILED: 1 failure(s):
[1] Tracking.scanned example 1: the example gives no after-state, which means unchanged, but the state changed: before Tracking { parcels: [Parcel { id: 1, first: 100, last: 300, scans: 2 }] } after Tracking { parcels: [Parcel { id: 1, first: 100, last: 300, scans: 3 }] } (write the after-state, or `unchanged`)

Commutativity says the order of the feed does not matter; idempotence says its repetitions do not. A unit fed by events needs both, and each is checked by its own statement: commutes for the order, and an example that repeats a call for the repetition. A number that counts events is right only if the feed never repeats itself; the first and last times are right whatever it does.

Why it is worth declaring

Without the declaration, a unit fed out of order is correct only if something upstream sorts the events and removes the duplicates first: a buffer, a sequence number, a queue with exactly-once delivery, each its own program with its own failures. With it, the unit takes events as they come, and the verifier has looked for an order that matters and found none. The feed’s disorder stops being a problem to engineer around and becomes a property of the unit, stated in one line and checked.

Try

In order-scans.vish, refuse late scans instead of absorbing them: add case parcel in parcels && at < parcels[parcel].last => fail Late; as the first case. The verifier now reports two failures. The scenario’s late scan answers Late at step 2, and the commutativity check reports scanned(9, 226) and scanned(9, 231) do not commute: one order succeeds and the other fails (Late). Refusing an event for arriving late makes the outcome depend on the order, which is the one thing a feed does not control.

Keyboard shortcuts