Account for counted sequence contention in population estimates - #9

--estimate-population true reported the estimate unavailable on every real capture. On each one, selectedIntervals - receivedObservations equalled sequenceContentions: the kernel counted every interval it dropped because it couldn't allocate a correlation sequence, and the estimator rejected any contention at all.

Collector (jonoffcpu_cookie.bpf.c)

• allocate_sequence now retries the compare-and-swap from the value the winning CPU left, up to 16 attempts. Before, it dropped the interval after one lost race. Each lost attempt means another CPU took a sequence, so the loop always makes progress and its cost is capped.
• Zero is still the exhaustion sentinel. Sequences are still unique, and the cookie is still epoch << 32 | sequence. sequenceContentions still counts an interval that loses all 16 attempts.

Correlator

• The loss is accounted only when all of these hold: selected - sequenceContentions == rows == received == written, every other failure counter is zero, and nothing else is wrong. In that case the estimate is available and the report shows:
  • accountedLoss {intervals, fraction, reason: "sequence-contention"}
  • sourceCoverageComplete: false
  • an assumptions entry saying contention is independent of an interval's stack and duration
• The estimate is scaled by selected / received in the same exact fixed-point arithmetic. The stack profile's per-entry estimates are scaled the same way, and its estimateAvailable is now true when the estimate is available.
• New option --max-accounted-loss F, default 0.01, allowed range 0 ≤ F < 1. A loss above it gives unavailable with accounted-loss-above-limit, and accountedLoss is still reported. The option is added in the current hand-parsed CLI style, kept small so the picocli migration can rebase over it.
• Any gap the counters don't explain keeps today's reasons (nonzero-sequenceContentions, selected-source-row-count-mismatch, …).
• Docs updated: OFFLINE.md, the README correlator options table (--estimate-population and --max-accounted-loss) and the native README.

Verified

• ./gradlew spotlessCheck :jonoffcpu-agent:check :jonoffcpu-correlator:check -PnativeArchitectures=x86_64 -PnativeLibcs=glibc passes. New OfflineCorrelatorTest cases cover:

  • zero contention keeps the exact estimate
  • counted contention gives available, accountedLoss and the 3/2 scale
  • a loss above the limit is refused
  • an unexplained mismatch, or another nonzero failure counter, keeps today's reasons
  • through the CLI: the report, the profile's estimateAvailable and the scaled profile total; a limit of 1 is rejected

• cargo fmt --check passes. The collector builds in the pinned container (x86-64 only).

• Privileged kernel proofs run on Linux 7.1.5, 16 CPUs, x86-64. The verifier accepts the loop. These pass: sequence-boundary (exhaustion sentinel still ends at 0, 0 contentions), sched-exit, transport, offcpu-reason and collector-smoke.

• The packaged agent smoke passes (x86-64 glibc, 1447 matched samples).

• Contention stress: a throwaway variant of the sequence-boundary proof, not committed. It ran 96 threads doing 20 µs sleeps on 16 CPUs, with the sequence starting at 1.

  BPF code	sequenceContentions	Selected intervals
  Old	24,167 and 24,615	about 300k per run
  New	0 in 3 runs	about 300k per run

• E235 broker capture (acceptance 1): status: available, accountedLoss.intervals = "713", fraction = 0.00169794, estimatedDurationNanos = 15378600234629, stackProfile.estimateAvailable = true. With --max-accounted-loss 0.001 it is unavailable with accounted-loss-above-limit.

Not verified

• arm64: covered by CI only.
• musl packaged smoke: covered by CI.
• run-task-lifetime-proof.sh: not run successfully. Run on its own it exits with "runner must bind the outer PID namespace identity", because it needs the run-lifetime-gates.sh setup, which I did not run.
• Acceptance 4, a rerun of the Pulsar high-rate scenario with the new collector, has not been done. The stress above is the only evidence so far.