A follow-up thread from the #801 investigation (see the closing comment there and #802): the reduce driver has a nearby, weaker hazard that we believe is content-safe but could transiently malform its retirement interval. Filing so the analysis doesn't get lost.
The pattern. reduce_with_tactic maintains its retirement upper as
input.for_each(|cap, batches| { ... upper_limit.clone_from(batch.upper()); ... });
source_trace.advance_upper(&mut upper_limit);
antichain_join_into(&upper_limit, &frontier.frontier(), &mut joined); // upper = join
Why it cannot lose content (unlike the join pre-#802): the input frontier participates in the joined upper, and any in-flight batch's message capability holds that frontier back, so the retirement interval can never advance past undelivered content. This is the structural reason the #801 bug lived in the join (whose acknowledged is pure batch bookkeeping) and not here.
The residual hazard: advance_upper can lift upper_limit through empty trace regions whose batch messages are still undelivered (empty batches are transmitted when capabilities permit). When such a late empty batch arrives, upper_limit.clone_from(batch.upper()) regresses it below lower_limit (the previous joined upper). Normally advance_upper immediately re-lifts through the same empty region — its precondition is an empty trace batch with lower() == upper_limit exactly — and the frontier join repairs the rest. But if trace merges have meanwhile absorbed that empty region into a neighbor below (physical compaction only pins boundaries at-or-above the previous upper), the exact-boundary match fails, and the joined upper can end up not-greater-or-equal to lower_limit on some coordinates: a malformed interval [lower, upper).
We have never observed this (the release-mode tiling assert at the end of the tactic's batch construction would fire loudly, and it never has across extensive contended and simulated runs, including the #801 repro workloads). Consequences if it ever occurred look like assert failures rather than silent corruption, which is the right failure mode — but the invariant is currently maintained by coincidence of timing rather than by construction.
Suggested hardening, in the spirit of the span asserts added to the join in #802:
- make
upper_limit explicitly monotone (only clone_from a received upper when it is at-or-beyond the current value, mirroring the join's guarded acknowledged update), and/or
assert! at retirement time that lower_limit ≤ upper_limit as frontiers, so a malformed interval is named at its source instead of surfacing as a downstream tiling failure.
count/threshold use advance_upper only to advance compaction and process every received batch; they have neither the join's skip guard nor this interval shape to maintain.
A follow-up thread from the #801 investigation (see the closing comment there and #802): the reduce driver has a nearby, weaker hazard that we believe is content-safe but could transiently malform its retirement interval. Filing so the analysis doesn't get lost.
The pattern.
reduce_with_tacticmaintains its retirement upper asWhy it cannot lose content (unlike the join pre-#802): the input frontier participates in the joined upper, and any in-flight batch's message capability holds that frontier back, so the retirement interval can never advance past undelivered content. This is the structural reason the #801 bug lived in the join (whose
acknowledgedis pure batch bookkeeping) and not here.The residual hazard:
advance_uppercan liftupper_limitthrough empty trace regions whose batch messages are still undelivered (empty batches are transmitted when capabilities permit). When such a late empty batch arrives,upper_limit.clone_from(batch.upper())regresses it belowlower_limit(the previous joined upper). Normallyadvance_upperimmediately re-lifts through the same empty region — its precondition is an empty trace batch withlower() == upper_limitexactly — and the frontier join repairs the rest. But if trace merges have meanwhile absorbed that empty region into a neighbor below (physical compaction only pins boundaries at-or-above the previous upper), the exact-boundary match fails, and the joined upper can end up not-greater-or-equal tolower_limiton some coordinates: a malformed interval[lower, upper).We have never observed this (the release-mode tiling assert at the end of the tactic's batch construction would fire loudly, and it never has across extensive contended and simulated runs, including the #801 repro workloads). Consequences if it ever occurred look like assert failures rather than silent corruption, which is the right failure mode — but the invariant is currently maintained by coincidence of timing rather than by construction.
Suggested hardening, in the spirit of the span asserts added to the join in #802:
upper_limitexplicitly monotone (onlyclone_froma received upper when it is at-or-beyond the current value, mirroring the join's guardedacknowledgedupdate), and/orassert!at retirement time thatlower_limit ≤ upper_limitas frontiers, so a malformed interval is named at its source instead of surfacing as a downstream tiling failure.count/thresholduseadvance_upperonly to advance compaction and process every received batch; they have neither the join's skip guard nor this interval shape to maintain.