[cgcote]

What does this PR do?

Adds a diagnostic Tier-1 formal-methods suite and concrete regression/stress repros for lifecycle, ownership, flush, retry, fan-out, and shutdown failures in the tracer.

This remains a diagnostic draft. It intentionally contains no production fixes. Known-bug models are expected to produce their documented invariant violations, and the corresponding regression/stress tests expose the current implementation behavior.

The suite uses three complementary techniques:

1. small executable TLA+ specifications for one protocol/handoff at a time;
2. generated Java command sequences checked against independent reference models;
3. JCStress probes for concurrency schedules that ordinary unit tests are unlikely to hit.

Executive summary

The investigation has confirmed 11 distinct counterexamples across pending traces, writer flush semantics, remote configuration, telemetry, Data Streams shutdown, and concurrent lifecycle barriers.

The recurring problem is that an acknowledgement is not always bound to all of the work it claims to acknowledge. Examples include a flush marker covering one queue but not upstream/secondary work, a shared counter acknowledging another caller's flush, and remote-config state being treated as globally applied after only partial listener delivery.

These tests prove that the faulty implementation schedules are reachable. They do not establish how frequently customers encounter them.

Suggested priority

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

#	Priority	Area	Counterexample	Potential effect
1	P1 / High	Span sampling	Flush completes while accepted single-span-sampling work remains upstream	Shutdown/manual flush reports success before accepted spans are serialized
2	P1 / High	Pending traces	Flush drain leaves stale queue ownership and a late child cannot obtain a future writer	Missing or incomplete trace
3	P1 / High	Writer secondary queue	PUBLISH_SECONDARY -> FLUSH acknowledges the primary marker before visiting the secondary queue	Accepted traces remain after successful flush
4	P1 / High	Concurrent pending-trace flush	Two callers share flushCounter; one marker can release the other caller before its element is written	Flush returns successfully with owned work still pending
5	P1 / High, product-dependent	Remote config accept	A throwing listener prevents later healthy listeners from receiving configuration and cached state prevents retry	Persistent listener divergence
6	P1 / High, product-dependent	Remote config remove	A throwing listener prevents later healthy listeners from removing configuration and replay is treated as unchanged	Stale configuration remains active
7	P1 / High, product-dependent	Remote config commit	A throwing listener prevents later healthy listeners from committing and replay is treated as unchanged	Applied state remains inconsistent
8	P2 / Medium-High	Data Streams shutdown	A full inbox rejects the poison pill and close() can return with the worker alive	Thread leak, join delay, incomplete final flush
9	P2 / Medium	Long-running traces	A full tracker consumes the ownership transition but retains nothing	Trace can become unowned and remain unwritten
10	P2 / Medium	Tracer flare	A flush drain consumes the dump marker without acknowledging it	Flare preparation can wait indefinitely or lose diagnostic trace data
11	P3 / Low-Medium	Telemetry retry	SEND_FAILURE -> ADD -> SEND_SUCCESS retries an empty buffer instead of the new event	Delivery is delayed and moreData is falsely reported as false

Remote-config findings are correctness defects. Their security significance depends on the affected product/listener; this investigation has not demonstrated a security exploit.

Findings and evidence

1. Single-span-sampling flush bypass

TraceProcessingWorker.flush() places its barrier directly in the primary serialization queue without first synchronizing with the upstream SpanSamplingWorker.

• Model: formal-methods/span-sampling-flush/SpanSamplingFlush.tla
• Invariant: FlushCoversAcceptedCandidate
• Regression: TraceProcessingWorkerTest.flushWaitsForInFlightSingleSpanSampling
• Failure: flush returns successfully with zero serialized traces while one accepted candidate remains upstream

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
• Regression: PendingTraceBufferTest.flushDrainClearsEnqueuedStateBeforeWriting

3. Writer secondary queue bypasses flush

The generated writer state machine records every trace accepted before a flush. The minimal counterexample is:

PUBLISH_SECONDARY -> FLUSH

The serializer observes and acknowledges the primary marker before consuming the already accepted secondary trace.

• Regression: TraceProcessingWorkerStateMachineTest.generatedCommandSequencesRespectFlushBarriers

4. Concurrent pending-trace flush callers share an acknowledgement

One JCStress actor invokes flush(). A second actor enqueues an element, invokes flush(), and records the element's write count when its call returns.

Forbidden result:

writes observed when the owning flush returned = 0

• Probe: PendingTraceBufferConcurrentFlushStressTest
• Result: 6 forbidden outcomes in 913 samples
• Reproduced across five JVM/compiler configurations
• Cause: both callers accept any newer flushCounter value instead of waiting for an acknowledgement tied to their own marker

5-7. Remote-config listener fan-out failures

The fault-injection state machine places a throwing listener before a healthy listener and injects failure independently into:

accept
remove
commit

It then replays identical remote state. In every phase the healthy listener misses the operation, while cached state reports no change and prevents retry.

• Model: formal-methods/remote-config-listeners/ListenerDistribution.tla
• Regressions:
  • ProductStateSpecification.listenerFailureDoesNotPreventLaterListenersFromReceivingConfiguration
  • ProductStateListenerStateMachineTest.generatedListenerFailuresRemainRetryableForHealthyListeners

8. Data Streams shutdown poison pill can be rejected

When the bounded inbox is full, the shutdown POISON_PILL offer can fail. close() then waits for the join timeout and can return while the worker remains alive.

• Model: formal-methods/data-streams-close/DataStreamsClose.tla
• Invariant: close cannot return with the worker alive
• Regression: DefaultDataStreamsMonitoringTest.closeStopsWorkerWhenInboxIsFull

9. Full long-running tracker loses trace ownership

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

• Model: formal-methods/long-running-traces/TrackerOwnership.tla
• Invariant: LiveTraceHasOwner
• Regression: LongRunningTracesTrackerTest.fullTrackerLeavesOverflowTraceForBufferFallback

10. Flush consumes tracer-flare dump marker

FLUSH_ELEMENT bulk-drains subsequent elements through Element.write(). DUMP_ELEMENT has a no-op write(), so its marker disappears without incrementing dumpCounter.

• Model: formal-methods/flush-dump-marker/FlushDumpMarker.tla
• Invariant: WaitingDumpHasOwner
• Regression: PendingTraceBufferTest.flushDrainDoesNotConsumeTracerDumpMarker

11. Empty telemetry retry masks a newly queued event

The generated telemetry state machine extracts event identifiers from the real serialized request body and compares them with a queued/retry/delivered reference model.

Minimal counterexample:

SEND_FAILURE -> ADD -> SEND_SUCCESS

The first empty failed request creates an empty retry buffer. The next send retries that empty buffer instead of taking the new event, then reports false even though the event remains queued.

• Model: formal-methods/telemetry-retry/TelemetryRetryOwnership.tla
• Regression: TelemetryServiceStateMachineTest.generatedRetrySequencesPreserveAcceptedEventOwnership

Positive evidence

Not every explored protocol failed.

The bounded continuation lifecycle model passes, and two JCStress probes cover:

• release racing with resume + close;
• two resume + close operations racing with release.

All 156 JVM/compiler configurations observed exactly one finalization: no continuation leak and no double finalization. This is narrow positive evidence for that counter protocol, not proof of unrelated scope-manager behavior.

Method and contract vocabulary

Every modeled asynchronous handoff identifies:

1. the owner before and after the handoff;
2. receiver rejection and capacity behavior;
3. barrier semantics for flush and close;
4. terminal states: delivered, explicitly dropped, cancelled, or retryable;
5. a minimal Java schedule for every counterexample.

The central contracts are:

• Ownership: accepted work remains queued, in flight, retry-buffered, delivered, explicitly dropped, or cancelled.
• Flush barrier: successful flush covers causally prior accepted work across upstream and secondary stages.
• Close barrier: close returns only after the worker has stopped and accepted work has a terminal state.
• Fan-out: all healthy listeners receive a phase, or incomplete delivery remains retryable.
• Per-command acknowledgement: a caller is released only by completion of its own marker/barrier.

Generated implementation state machines follow three rules:

1. schedules are deterministic and bounded;
2. the oracle is an independent reference model, not internal queue state;
3. exploration continues after known defects and retains the shortest schedule for each distinct cause.

Recurring failure patterns

1. Control messages share a bounded data queue and use best-effort offers even when loss breaks shutdown or flush.
2. One barrier covers only one pipeline stage while work remains upstream, secondary, or in flight.
3. A global counter/generation acknowledges “some command completed,” not “this caller's command completed.”
4. Fan-out state advances before every healthy listener completes the phase.
5. Empty retry state is treated as useful buffered work and masks newly queued work.
6. Ownership transitions happen before downstream capacity is secured.

Validation

• Tier-1 TLA+ models reproduce their documented invariant violations or documented passing result.
• Generated writer, remote-config, telemetry, and saturation state machines produce minimized implementation schedules.
• Continuation JCStress probes pass all 156 tested configurations.
• Concurrent pending-trace flush JCStress probe finds 6 forbidden outcomes in 913 samples.
• Focused regression tests reproduce the predicted failures.
• Spotless checks pass.
• git diff --check passes.

What has and has not been established

Established:

• Each reported counterexample maps to an implementation schedule and a concrete contract violation.
• Several defects reproduce deterministically; concurrent flush reproduces probabilistically across multiple compiler modes.
• No production fixes were used to manufacture passing behavior.

Not established:

• customer incidence or frequency;
• end-to-end loss rates under representative workloads;
• security exploitability of remote-config divergence;
• absence of other bugs in components whose bounded models or probes passed.

Recommended next experiments

The highest-yield next step is a systematic control-message saturation audit:

1. find unchecked offer(STOP), poison-pill, flush, report, and dump operations;
2. pause the consumer and fill the queue;
3. invoke flush() or close();
4. verify the command remains owned/acknowledged, the worker terminates, and accepted data is delivered or explicitly dropped.

Then:

• expand JCStress to flush versus close, multiple writer flush callers, and more continuation schedules;
• run concurrency probes across the supported JDK matrix;
• use a fake Agent intake endpoint to compare accepted versus received traces;
• replay remote-config updates across repeated polls with throwing and healthy listeners;
• measure thread survival and join latency under saturated Data Streams and metrics queues.

Scope and review intent

This PR establishes reproducible evidence and helps decide fix order. It contains formal models, run documentation, generated state-machine tests, deterministic regressions, and JCStress probes. It deliberately contains no production fixes and should remain draft / do-not-merge until 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.94 s	13.93 s	[-0.6%; +0.6%] (no difference)
startup:insecure-bank:tracing:Agent	12.85 s	12.95 s	[-1.4%; -0.1%] (maybe better)
startup:petclinic:appsec:Agent	17.03 s	16.91 s	[-0.1%; +1.6%] (no difference)
startup:petclinic:iast:Agent	16.39 s	16.95 s	[-7.6%; +1.0%] (no difference)
startup:petclinic:profiling:Agent	16.60 s	16.14 s	[-1.5%; +7.1%] (no difference)
startup:petclinic:sca:Agent	16.97 s	16.77 s	[+0.2%; +2.1%] (maybe worse)
startup:petclinic:tracing:Agent	16.11 s	16.07 s	[-0.4%; +0.9%] (no difference)

Commit: 54bea739 · 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.