Skip to content

Repository navigation

I/O verification suite — TLA+, Turmoil, loopback, otelcol oracle, benchmarks #1314

New issue
New issue
Open
Open
I/O verification suite — TLA+, Turmoil, loopback, otelcol oracle, benchmarks#1314
Labels
P2: mediumMinor bug, missing validation, metric inaccuracyarchitectureSystemic design improvements that eliminate classes of bugscomponent:input/fileFile input, tailing, globbing, rotation, and file checkpointscomponent:input/otlpOTLP receiver inputcomponent:output/commonCross-cutting output behavior spanning multiple sinkscomponent:pipelinePipeline orchestration, batching, runtime flow, and worker coordinationcomponent:processor/checkpointCheckpoint persistence, replay, and checkpoint protocol behaviorenhancementNew feature or requestperformancePerformance optimizationproductionRequired for production readinessresearchRequires research/investigation

Description

@strawgate
strawgate
opened on Apr 6, 2026

Problem

A correct-by-construction I/O architecture is not complete until its guarantees are checked at the right layers. Right now the repo has important verification assets, but they are not yet assembled into one deliberate architecture-level strategy.

This issue is the full verification and performance-validation track for the architecture umbrella.

Desired end-state

  • architecture-level protocol/lifecycle rules are modeled where they should be model-checked
  • local pure invariants are proved where proof pays off
  • stateful correctness properties are exercised with proptest and deterministic integration tests
  • distributed and crash/recovery behavior are exercised in Turmoil
  • OTLP wire semantics are checked by loopback and oracle-style tests
  • benchmark validation protects the architecture's performance goals
  • non-core pure seams have an explicit Kani boundary contract so reviewers and CI can tell which files are proof-required, recommended, or exempt

Scope

1. TLA+

  • update or extend specs for the protocol/lifecycle rules that must hold independent of implementation shape

2. Kani / local proofs

  • prove local pure invariants and transition helpers where proof materially reduces risk
  • define the repo contract for Kani-targetable pure seams outside logfwd-core
  • add file/module-level proof expectations and exemption taxonomy for async/IO-heavy seams
  • add a machine-readable Kani boundary manifest and fast CI checker so proof-required files do not drift silently

3. Proptest / stateful testing

  • add randomized stateful tests where file lifecycle, retries, or boundary sequences are hard to cover exhaustively by hand

4. Turmoil / fault simulation

  • expand deterministic faulted end-to-end scenarios for the final architecture

5. OTLP loopback + oracle

  • sink->receiver loopback semantic equivalence
  • otelcol differential checks at the right CI tier

6. Benchmark validation

  • component-level throughput/latency validation with disciplined benchmark methodology

Design stance

Verification should match the seam. We should not force one technique everywhere, and we should not claim architecture guarantees without naming how they are enforced.

For Kani specifically: prefer semantic local pure modules first, promote to seam folders when the domain grows, and do not centralize all proof-worthy logic into one shared crate or one blanket pure/ tree.

Relationships

Depends conceptually on:

Relates to:

Activity

  1. strawgate
    added
    enhancementNew feature or request
    productionRequired for production readiness
    P2: mediumMinor bug, missing validation, metric inaccuracy
    architectureSystemic design improvements that eliminate classes of bugs
    on Apr 6, 2026

  2. github-actions commented on Apr 6, 2026

    @github-actions
    github-actionsBot
    on Apr 6, 2026 – with GitHub Actions
    Contributor

    tl;dr: This issue needs a human decision before implementation: #1314 says checkpoint advancement should happen only on successful delivery, but current code/spec intentionally advance checkpoints on reject, and that semantic choice changes drain/liveness behavior.

    Recommendation

    Outcome B — Needs human decision.

    What's unclear

    1. Should rejected batches advance checkpoints (current behavior), or should checkpoints advance only on success (new behavior requested in I/O verification suite — TLA+, Turmoil, loopback, otelcol oracle, benchmarks #1314)?
    2. Should I/O verification suite — TLA+, Turmoil, loopback, otelcol oracle, benchmarks #1314 be blocked until File appender output — new component with rotation, cleanup, path templates #1313 lands file output/appender support, since one required path is OTLP receiver → pipeline → file appender?

    Options

    1. Keep current semantics (reject advances checkpoint) and reword I/O verification suite — TLA+, Turmoil, loopback, otelcol oracle, benchmarks #1314 acceptance criteria to match current design invariants.
    2. Change to success-only checkpoint advancement and update Rust + TLA + simulation expectations (risk: poison data can stall progress/drain).
    3. Split I/O verification suite — TLA+, Turmoil, loopback, otelcol oracle, benchmarks #1314 into (a) verification work that can land now, and (b) appender-dependent tests after File appender output — new component with rotation, cleanup, path templates #1313.

    Recommendation

    I recommend Option 1 + Option 3: keep reject-advances-checkpoint semantics (already codified in Rust and TLA), and split/gate appender-dependent verification behind #1313. Please add label needs-decision.

    Findings
    Evidence Observation Why it matters
    crates/logfwd/src/pipeline.rs:977-983 success=false path uses ticket.reject() then machine.apply_ack(receipt) Rejects currently participate in checkpoint progression.
    tla/README.md:179-189 Spec explicitly documents “Rejected batches advance the checkpoint.” Current design intent conflicts with “checkpoint only on successful delivery.”
    tla/PipelineBatch.tla:18-19 Property includes RejectAdvancesCheckpoint Semantics are formalized, not incidental.
    crates/logfwd-config/src/lib.rs:759-763 `OutputType::File OutputType::Parquet` rejected as not implemented
    crates/logfwd-output/src/lib.rs:669-671 Unsupported output types error out Confirms file output path is not yet available at sink factory level.
    .github/workflows/ci.yml:290 Turmoil simulation suite already runs in CI #1314 subtask 5.2 is partially present already.
    .github/workflows/ci.yml:323-333 ShutdownProtocol and PipelineBatch TLC jobs run in CI TLA coverage for existing specs is already wired.
    .github/workflows/bench.yml:167,174 Benchmark matrix is continue-on-error and --mode binary Nightly bench exists but is not strict threshold gating and not Docker oracle validation.
    crates/logfwd-io/tests/it/transport_e2e.rs:428-490 Receiver roundtrip exists for OTLP protobuf decode Receiver-side coverage exists; full sink→receiver semantic loopback is still a separate gap.
    Verification

    I validated the key claims with direct repository commands:

    $ grep -nE "Rejected batches advance the checkpoint|ticket.reject\(|apply_ack\(" tla/README.md crates/logfwd/src/pipeline.rs | head -n 12
tla/README.md:179:### 2. Rejected batches advance the checkpoint
crates/logfwd/src/pipeline.rs:980:                ticket.reject()
crates/logfwd/src/pipeline.rs:982:            let advance = machine.apply_ack(receipt)
    $ grep -nE "output type is not yet implemented|not yet supported" crates/logfwd-config/src/lib.rs crates/logfwd-output/src/lib.rs | head -n 12
crates/logfwd-config/src/lib.rs:761: ... output type is not yet implemented
crates/logfwd-output/src/lib.rs:670: "output '{name}': type {:?} not yet supported"
    $ grep -nE "turmoil_sim|PipelineBatch|ShutdownProtocol" .github/workflows/ci.yml | head -n 15
290: run: cargo test -p logfwd --features turmoil --test turmoil_sim
323: ShutdownProtocol — safety
329: PipelineBatch — safety
332: PipelineBatch — liveness
    $ grep -nE "continue-on-error|--mode binary|otelcol" .github/workflows/bench.yml | head -n 20
143: AGENTS="logfwd,vector,fluent-bit,filebeat,otelcol,vlagent"
167: continue-on-error: true
174: --mode binary \
    Detailed Action Plan (post-decision)
    1. Resolve checkpoint semantic decision in I/O verification suite — TLA+, Turmoil, loopback, otelcol oracle, benchmarks #1314 explicitly (reject advances vs success-only).
    2. If keeping current semantics, update I/O verification suite — TLA+, Turmoil, loopback, otelcol oracle, benchmarks #1314 wording to match existing contract in:
      • tla/README.md:179-189
      • tla/PipelineBatch.tla:18-19
      • crates/logfwd/src/pipeline.rs:977-983
    3. Land non-appender-dependent verification first:
      • Add OTLP sink→receiver semantic loopback test under crates/logfwd-io/tests/it/.
      • Add otelcol differential oracle tests (ignored/nightly path).
      • Wire nightly oracle execution in workflow (separate from PR CI fast path).
    4. After File appender output — new component with rotation, cleanup, path templates #1313 lands file appender support, add OTLP receiver→pipeline→file appender end-to-end assertions.
    5. Add benchmark threshold gate job (not continue-on-error) for I/O verification suite — TLA+, Turmoil, loopback, otelcol oracle, benchmarks #1314 target metrics.
    Related Items
    Type Link Relevance
    Issue #1315 Parent I/O correctness refactor; #1314 is Phase 5 verification slice.
    Issue #889 Roadmap tracks #1314 and links it to Phase 7 verification extensions.
    PR #1290 In-flight OTLP/file-IO oracle contract work that overlaps #1314 scope.
    File crates/logfwd/src/pipeline.rs:967-995 Current checkpoint advancement behavior on ack/reject.
    File tla/PipelineBatch.tla:14-26 Formal batch/checkpoint properties and modeled scope limits.
    File .github/workflows/bench.yml:152-176 Nightly benchmark matrix behavior (continue-on-error, binary mode).

    Note

    🔒 Integrity filtering filtered 15 items

    Integrity filtering activated and filtered the following items during workflow execution.
    This happens when a tool call accesses a resource that does not meet the required integrity or secrecy level of the workflow.

    What is this? | From workflow: Issue Triage

    Give us feedback! React with 🚀 if perfect, 👍 if helpful, 👎 if not.

  3. coderabbitai
    added
    performancePerformance optimization
    researchRequires research/investigation
    on Apr 6, 2026

  4. strawgate commented on Apr 6, 2026

    @strawgate
    strawgate
    on Apr 6, 2026
    OwnerAuthor

    Updated this issue to represent the full verification/performance-validation track for the architecture umbrella, not just a grab-bag of extra tests. The focus is now explicit: verification matched to the seam and tied to the final I/O architecture.

  5. strawgate commented on Apr 6, 2026

    @strawgate
    strawgate
    on Apr 6, 2026
    OwnerAuthor

    Following the pure-function-isolation fan-in, verification ownership is now split into one explicit policy batch plus several local-seam extraction batches:

    This should make the verification story more operational: reviewers and CI can tell which files are Kani-required, while implementation slices stay local to the owning crates.

  6. strawgate
    added
    component:pipelinePipeline orchestration, batching, runtime flow, and worker coordination
    component:processor/checkpointCheckpoint persistence, replay, and checkpoint protocol behavior
    component:input/otlpOTLP receiver input
    component:input/fileFile input, tailing, globbing, rotation, and file checkpoints
    component:output/commonCross-cutting output behavior spanning multiple sinks
    on Apr 10, 2026

  7. strawgate commented on Apr 10, 2026

    @strawgate
    strawgate
    on Apr 10, 2026
    OwnerAuthor

    Queued low-conflict verification execution work-units:

    These were intentionally scoped away from current high-conflict open PR surfaces (#1764/#1759/#1753/#1738/#1733).

  8. strawgate commented on Apr 10, 2026

    @strawgate
    strawgate
    on Apr 10, 2026
    OwnerAuthor

    Tightened execution scopes and proof gates on child work-units for first-pass quality:

    These are now strict enough to assign without additional interpretation drift.

  9. strawgate commented on Apr 11, 2026

    @strawgate
    strawgate
    on Apr 11, 2026
    OwnerAuthor

    Partial-resolution status update (April 11, 2026):

    Recent verification slices landed under this scope:

    Recommendation:

  10. strawgate commented on Apr 11, 2026

    @strawgate
    strawgate
    on Apr 11, 2026
    OwnerAuthor

    Queued next Turmoil bug-finding wave (post-PR #1809 merge):

    1. Scenario matrix expansion focused on app invariants (not throughput thresholds)
    • mixed faults in one run: hold/release + one-way partition + crash/bounce + checkpoint flush crash
    • assertions: checkpoint monotonicity, no post-stop side effects, eventual drain under stable tail
    1. Low-capacity stress lane
    • intentionally small to detect simulator-pressure edge cases while asserting graceful runtime outcomes
    1. Formal bridge pass
    • map replayed Turmoil failures to explicit TLA states/transitions
    • identify pure reducer boundaries for ack/checkpoint advancement and add/extend Kani proofs

    I can take this as the next branch as soon as #1809 is merged.

  11. strawgate commented on Apr 24, 2026

    @strawgate
    strawgate
    on Apr 24, 2026
    OwnerAuthor

    Deep-Dive Research: I/O Verification Suite

    Current State (Code-Verified)

    Rich verification already exists:

    • 7 TLA+ specs: PipelineMachine, ShutdownProtocol, PipelineBatch, DeliveryRetry, FanoutSink, TailLifecycle, WorkerPoolDispatch
    • Turmoil actively used: RuntimeBarrierEvent enum with PipelinePhase, BatchSubmitted, AckApplied, etc. Entire input_pipeline.rs has cfg(not(feature = "turmoil")) guards
    • 14 benchmark files in logfwd-bench/benches/
    • 12 scenario benchmarks in bench/scenarios/

    Gaps

    1. No loopback I/O test — no closed-loop byte-level verification (Generator→pipeline→output→verify)
    2. No otelcol oracle — no conformance comparison with reference OpenTelemetry Collector
    3. Turmoil covers orchestration, not data content — barriers verify state transitions, not bytes
    4. No network fault injection — turmoil's network simulation not used for partitions/latency
    5. No end-to-end proptest — property tests used in components but not across full pipeline
    6. No deterministic replay

    Recommended Phase 1: Loopback Harness

    ArrowIpc output + ArrowIpc input already exist. Loopback test: Generator → pipeline → ArrowIpc output → ArrowIpc receiver → validate batch equality. Zero external dependencies.

    Complexity: XL (meta across TLA+, Turmoil, loopback, oracle, benchmarks)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    P2: mediumMinor bug, missing validation, metric inaccuracyarchitectureSystemic design improvements that eliminate classes of bugscomponent:input/fileFile input, tailing, globbing, rotation, and file checkpointscomponent:input/otlpOTLP receiver inputcomponent:output/commonCross-cutting output behavior spanning multiple sinkscomponent:pipelinePipeline orchestration, batching, runtime flow, and worker coordinationcomponent:processor/checkpointCheckpoint persistence, replay, and checkpoint protocol behaviorenhancementNew feature or requestperformancePerformance optimizationproductionRequired for production readinessresearchRequires research/investigation

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions