Module frontier 

A backend that reads its inputs as of a frontier.

A trace’s accumulations are correct only at or beyond its compaction frontier: a batch may hold a retraction advanced to the frontier beside the insertion it retracts, so an earlier time can show a count no time had. A reader that starts after the trace has compacted must read every update’s time advanced to a frontier since, as TraceFrontier does for a cursor. The proxy tactics hand batches to a backend, which reads their times as stored, so BackendFrontier reads what its inner backend draws as of since.

Advancing is not injective: updates that coincide once advanced are consolidated, since the tactics require consolidated bridges, and a join’s bridges must then still hold keys common to both inputs. Both are done only where a time actually moved.

What since must be

since must be beyond every frontier the trace has compacted by: each of its elements at or beyond some element of each such frontier. Then advancing a stored time, already advanced by a compaction frontier F, by since is advancing the original time by since: with x = advance_F(t), t ≤ x ≤ t ∨ f for some f ≤ s for each s in since, so t ∨ s ≤ x ∨ s ≤ t ∨ f ∨ s = t ∨ s, and the meets over s agree. So merged and unmerged copies of one update land on one time, in any lattice. A reader checks this against the trace’s logical compaction frontier when it imports, as TraceAgent::import_frontier does by taking that frontier as since. In particular, reading as of the meet of the trace’s compaction frontier is not safe in a non-distributive lattice: it advances too little, and leaves times between the meet and the frontier where the trace promises nothing.

Where the work is, and what is exact

Everything below uses only the defining property of Lattice::advance_by: for every t' beyond a frontier F, t ≤ t' ⟺ advance_F(t) ≤ t'; together with t ≤ advance_F(t), that advance_F(t) = t when t is beyond F, and the squeeze t ∨ t' = advance_F(t) ∨ t' for t' beyond F. None of it needs the lattice to be distributive.

Each unit of work carries a bound on the times it is about: the join’s meet of the fresh input’s times (JoinInstance::lower), the reduce’s retire interval (ReduceInstance::lower). When that bound is beyond since, the wrapper changes nothing, for any inner backend:

• A join’s output times are t0 ∨ t1 with the fresh input’s time beyond since, so by the squeeze advancing either input by since leaves every output time as it is: the output is identical to the as-of reading’s.
• A reduce evaluates only at times at at or beyond its lower bound, hence beyond since. Whether a record is in the accumulation there (t ≤ at) and which times it synthesizes (t ∨ at) are the same for t and advance(t), so the retire’s output is identical.

That is the steady state of an operator reading a trace it imported: every unit after the first has its bound beyond the import time. The first unit reads the trace’s history, and only it pays for the read. There the wrapper advances what the inner backend presents, and:

• It is exact when the inner backend presents stored times, or presents them advanced by a bound that since is beyond (every first unit, whose bound is the minimum): the same squeeze as for compaction. It is also exact when since has one element, whatever the backend does.
• In general the inner backend may consolidate on load by its bound lower, and in a non-distributive lattice advance_since(t ∨ lower) need not equal advance_since(t) when since and lower cross. Then the output agrees with the as-of reading at every time beyond since, which is all a trace read as of since promises its readers anyway: for t' beyond since, advance(t ∨ c) ≤ t' ⟺ t ≤ t' ∧ c ≤ t', and c ≤ lower ≤ the fresh time ≤ t'.

The join reads both inputs

Reading one input of a join as of since and reading both agree at every time beyond since, and are identical when the other input’s times are beyond since (the squeeze again). So the join wrapper reads both inputs as of since; a join whose inputs are read as of two frontiers nests two wrappers.

Structs

BackendFrontier

A backend whose inputs are read as of since: every time the inner backend draws is advanced by it, and what then coincides is consolidated.

Functions

read_as_of

Read bridge as of since: times advanced by it, and the bridge consolidated if any moved, as advancing can make records coincide. Returns whether any did; if none, the bridge is as presented, still sorted and consolidated.