research: multi-core recording via eBPF-ordered sync events (relax single-core serialization)

[chayan-bit]

Gap

README §3.3's soundness table lists "sync-primitive ordering" (sound for race-free programs, full record-time parallelism) as an option, and then the MVP correctly picks single-core serialization. #9 researches deterministic preemption within the single-core model. Nothing researches getting off it.

Single-core serialization is a real cost: it serializes the target under recording, which is exactly what makes recording a production or load-bearing service impractical. And the eBPF vantage point offers something rr never had: a kernel-side total order over sched_switch, syscall entry/exit, signal delivery, and uprobed sync primitives, timestamped by the kernel rather than reconstructed by the tracer.

The open question: for which class of programs does that kernel-side ordering suffice to replay deterministically at full record-time parallelism?

Scope

• Formalize the soundness boundary: kernel-ordered sync events give a total order over synchronization, hence sound replay for programs whose shared-memory accesses are all synchronization-ordered (data-race-free). Lock-free/atomic races remain invisible. Write this down precisely; it is a claim we will be held to.
• Prototype a --parallel recording mode: no core pinning, order derived from eBPF-timestamped sync + sched events.
• Divergence detection (feat: divergence detection via memory checksums #11) becomes load-bearing, not a safety net. In this mode it is the mechanism by which we detect that the DRF assumption was violated. Measure its detection rate against a deliberately-racy corpus — an undetected divergence here is a wrong answer shown confidently, which is the one failure mode this project cannot have.
• Evaluate the prior art on software instruction counters (the rr forks that replaced broken/inaccessible HW counters with lightweight dynamic instrumentation providing deterministic ticks) — a hybrid of kernel-side event capture + userspace ticks may bound the races we currently cannot.
• Decide and document: is --parallel a supported mode, a best-effort mode with a divergence warning, or a dead end?

Explicit non-goal

Do not weaken the default. Single-core stays the sound default; this mode must be opt-in and must announce its assumptions.

Done when

There is a written soundness boundary, a prototype, a measured divergence-detection rate on a racy corpus, and a ship/no-ship recommendation.

Ref: README §3.3, #9, #11. Gap: eBPF-assisted hybrid recording.