[cgcote]

What does this PR do?

Adds four small TLA+ models and four deterministic regression tests for lifecycle and concurrency failures in tracer-core.

This remains a diagnostic draft. It intentionally contains no production fixes, so all four regression tests fail on the current implementation. The models, configuration, run instructions, and tests are the complete scope; continuation experiments and unrelated components are excluded.

Suggested priority

These priorities are relative engineering triage recommendations, not incident severity declarations.

Rank	Priority	Finding	User impact	Required interleaving / scope
1	P1 / High	Single-span-sampling flush bypass	A successful writer flush can return while an already accepted sampling candidate is still upstream. RemoteWriter.close() then interrupts the sampling pipeline, allowing sampled spans to be silently lost during normal shutdown.	Single-span sampling enabled; shutdown or explicit flush overlaps sampling.
2	P1 / High	Pending-trace flush leaves stale queue ownership	The flush drain writes a trace without clearing isEnqueued. A later child cannot requeue the trace, so that child span is never sent.	CoreTracer.flush() drains a trace with an unfinished child; child finishes afterward.
3	P2 / Medium	Full long-running tracker loses trace ownership	The worker is told that the full tracker accepted a trace even though it retained nothing, bypassing the fallback path. Finished spans may remain unreported indefinitely.	Experimental long-running traces enabled and tracker at capacity.
4	P2 / Medium	Flush consumes tracer-flare dump marker	A dump marker behind a flush marker is drained through a no-op write(), without incrementing dumpCounter. Flare preparation then waits indefinitely.	Tracer flare preparation races with CoreTracer.flush() in the modeled order.

Why findings 1 and 2 are first

Both can silently lose trace data through public lifecycle operations without buffer saturation or an explicitly experimental feature. Finding 1 also affects shutdown, where no later activity can recover the accepted spans. Finding 2 leaves the trace permanently ineligible for requeue after the flush drain.

Finding 3 has comparable ownership-loss consequences but requires the experimental long-running trace feature and tracker saturation. Finding 4 blocks diagnostic flare generation rather than application tracing, and requires a narrower command ordering.

Findings and evidence

1. Single-span-sampling flush bypass

TraceProcessingWorker.flush() places its barrier directly in the primary serialization queue. It does not first synchronize with the upstream SpanSamplingWorker.

• Model: formal-methods/span-sampling-flush/SpanSamplingFlush.tla
• Invariant: FlushCoversAcceptedCandidate
• TLC counterexample: 5 states
• Regression: TraceProcessingWorkerTest.flushWaitsForInFlightSingleSpanSampling
• Current failure: flush returns successfully with expected: <1> serialized trace but was: <0>

2. Pending-trace flush leaves stale queue ownership

The normal worker path clears isEnqueued before writing. WriteDrain.accept writes without clearing it, so a later child finish cannot requeue the trace.

• Model: formal-methods/pending-trace-flush/FlushDrainOwnership.tla
• Invariant: PendingChildHasWriter
• TLC counterexample: 3 states
• Regression: PendingTraceBufferTest.flushDrainClearsEnqueuedStateBeforeWriting
• Current failure: expected: <0> for isEnqueued, but was: <1>

3. Full long-running tracker loses trace ownership

LongRunningTracesTracker.add transitions TO_TRACK -> TRACKED, but addTrace drops at capacity and add still returns true. The pending-buffer worker therefore skips its fallback write path.

• Model: formal-methods/long-running-traces/TrackerOwnership.tla
• Invariant: LiveTraceHasOwner
• TLC counterexample: 4 states
• Regression: LongRunningTracesTrackerTest.fullTrackerLeavesOverflowTraceForBufferFallback
• Current failure: tracker reports acceptance with expected: <false> but was: <true>

4. Flush consumes tracer-flare dump marker

FLUSH_ELEMENT bulk-drains subsequent elements through Element.write(). DUMP_ELEMENT is a CommandElement with a no-op write(), so its marker disappears without acknowledgement.

• Model: formal-methods/flush-dump-marker/FlushDumpMarker.tla
• Invariant: WaitingDumpHasOwner
• TLC counterexample: 4 states
• Regression: PendingTraceBufferTest.flushDrainDoesNotConsumeTracerDumpMarker
• Current failure: TimeoutException while waiting for flare preparation

Validation

• All four TLC runs reproduce the documented invariant violations: 3, 4, 4, and 5 states respectively.
• Focused Gradle run executes four tests and produces four predicted failures.
• ./gradlew :dd-trace-core:spotlessJavaCheck passes.
• git diff --check passes.

Scope and review intent

This PR is intended to establish reproducible evidence and help decide fix order. It contains only formal models, run documentation, and regression tests. It deliberately does not include production fixes and should remain draft / do-not-merge until the findings are split or fixed.

[dd-octo-sts]

🟢 Java Benchmark SLOs — All performance SLOs passed

Suite	Status
Startup	🟢 pass

SLO thresholds are defined here based on automatically generated metrics. A warning is raised when results are within 5% of the threshold.

PR vs. master results

Scenario	Candidate	master	Δ (95% CI of mean)
startup:insecure-bank:iast:Agent	13.91 s	13.89 s	[-0.5%; +0.8%] (no difference)
startup:insecure-bank:tracing:Agent	12.84 s	12.92 s	[-1.3%; +0.0%] (no difference)
startup:petclinic:appsec:Agent	17.71 s	17.53 s	[+0.0%; +2.1%] (maybe worse)
startup:petclinic:iast:Agent	17.35 s	17.41 s	[-1.2%; +0.5%] (no difference)
startup:petclinic:profiling:Agent	17.10 s	17.12 s	[-1.3%; +1.0%] (no difference)
startup:petclinic:sca:Agent	17.64 s	17.59 s	[-0.9%; +1.5%] (no difference)
startup:petclinic:tracing:Agent	16.13 s	16.57 s	[-6.9%; +1.6%] (no difference)

Commit: f0c63233 · CI Pipeline · Benchmarking Platform UI

---

Load and DaCapo benchmarks can be triggered manually in the GitLab pipeline. Results will appear in the Benchmarking Platform UI after completion.