Skip to content

P2: Prove concurrent closing-expiry convergence across repositories #45

Description

@YueZh127

Objective

Add deterministic cross-repository regression proof for the existing closing-expiry compare-and-set contract. This is a verification gap discovered while reviewing #27, not evidence that Talos needs another production teardown mechanism.

Review origin and fixed baseline

Verification gap

The current suite does not directly force two independent expiry sweepers to observe the same expired closing Task version and then prove that only the winning terminal CAS performs externally observable teardown effects. The production premise is already refuted, but this concurrency contract should be locked down against future regression.

Acceptance criteria

  • Use deterministic barriers around two separate TaskService instances so both observe the same expired closing Task version before either guarded replacement resolves.
  • Run the same service-level contract against MemoryRepository and a real standalone MongoRepository.
  • Start the target machine with activeLeases=2; finish at exactly 1.
  • Preserve an unrelated reservation and profile lease.
  • Release the target reservation and generation-bound profile lease exactly once.
  • Persist exactly one completed task.state_changed event and one task.completed event for the expired Task.
  • Cover worker-result-wins and teardown-result-wins orderings at service level for both repositories.
  • In each winner ordering, assert the persisted SessionActionResult is exactly the immutable winning result; loser and duplicate retries cannot overwrite it.
  • After terminalization, assert pendingActionId is absent and the target Task contains no action left in pending or dispatched state.
  • Preserve P0: Bind terminal action retries to immutable dispatch credentials #29 immutable dispatch binding: a legitimate worker retry remains bound to the original dispatch claim/generation/binding, while stale or mismatched credentials cannot observe or replace the winner.
  • Prove the losing sweeper performs no lease/profile release, event, or action-result effect.
  • Keep non-interactive lease expiry/requeue and existing complete, cancel, queued-close, and closing-expiry contracts passing unchanged.
  • Use no sleeps, timing assumptions, process-local locks, timeout increases, client retries, or test-only production behavior.
  • If a reproducible bypass of the existing guarded CAS is found, stop and amend this issue with the concrete production defect before changing teardown implementation.

Scope and dispatch gate

Activity

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

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions