Invariants

This document lists formal invariants that the engine enforces. These are design goals that tests and runtime logic are built to preserve.

Runtime vs test-only invariants

• Runtime invariants: Enforced by the engine at runtime (e.g. token state machine, join count, external task single-owner, lock expiry). Violations are rejected or corrected by the runtime (e.g. CAS failure, ownership check).
• Test-only invariants: Verified by tests and replay (e.g. “replay produces the same final state as live execution”, “under concurrency only one claim succeeds per token”). They are not asserted in production code; tests and CI fail if they are violated.

1. Token invariants

• Exactly-once completion: A token can only reach a final state (Completed, Terminated) once. It cannot be re-executed after completion.
• Valid state transitions: Only allowed transitions are enforced (e.g. Ready → Executing → Waiting or Completed). Invalid transitions (e.g. Completed → Executing) are rejected.
• Single owner: At most one executor owns a token at any time. The claim mechanism (CAS on token version/status) ensures that only one worker can advance a given token.
• Idempotent transitions: Where the spec allows it, repeating the same transition is safe (no double side effects).

See Execution Model (Token & Concurrency) for the token lifecycle and claim algorithm.

2. Join invariants

• All branches required: A parallel join node only produces a single outgoing token when all incoming branches have arrived. The expected count is fixed at compile time; the runtime tracks arrivals per join key (process instance + gateway).
• No partial join: Join state is updated atomically; a join either waits for more tokens or emits one and clears.

3. External task invariants

• Exactly one owner: An external task is either unclaimed (READY) or held by one worker (LOCKED). Fetch-and-lock and complete/fail all check ownership; a task cannot be completed by a different worker than the one that locked it.
• Lease-bound: Locks expire; expired tasks return to READY. The engine does not rely on in-memory state for ownership.
• Retries monotonic: Retry count only decreases; the engine decides when to retry or fail finally.

4. Timer and persistence invariants

• Timers are persistent: Timer state is stored in the persistence layer, not only in memory. After a crash, the scheduler can recover by re-reading timers.
• Execution is crash-safe: Progress is driven by persisted state. Re-running the scheduler after a restart continues from the last committed state.

See Crash Recovery & Rehydration and Database Schema.

5. Testing invariants

Tests are written to assert these invariants under concurrency and failure:

• Token claim: Concurrent workers; only one succeeds per token. See Testing Strategy.
• Join: Multiple tokens arriving at a join; exactly one merged token proceeds when all have arrived.
• External task: Lock, complete, and fail only by the owning worker; idempotent complete/fail where specified.

Adding or changing behavior should preserve these invariants; new tests should be added when extending the engine.

6. Invariant violations in errors

When the runtime rejects an operation because it would violate an invariant, it returns an error that carries an invariant violation kind (InvariantViolationKind). This makes failures identifiable in logs, crash post-mortems, and issue reports, and supports future tooling (e.g. Execution Inspector UI).

• TokenFinalizedTwice — Token already in a final state (Completed/Terminated); corresponds to §1 (Exactly-once completion).
• JoinIncomplete — Parallel join advanced before all branches arrived; corresponds to §2 (All branches required).
• ExternalTaskLeaseConflict — Complete or fail called by a worker that does not hold the task lock; corresponds to §3 (Exactly one owner).
• TokenInvalidTransition — Invalid token state transition; corresponds to §1 (Valid state transitions).

REST API: when an external-task complete or fail call fails with an invariant violation, the response includes a X-Invariant-Violation header with the kind name (e.g. ExternalTaskLeaseConflict).