remora/docs/protocol/RemoraMultiShot.cfg

SPECIFICATION SafetySpec

CHECK_DEADLOCK TRUE

\* Multi-shot coordination wipe and re-partition (safety only; liveness is Remora.cfg).
CONSTANTS
    Jobs = {j1}
    Workers = {w1, w2}
    InitialWorkers = {w1}
    NoJob = NoJob
    NoWorker = NoWorker
    MaxAttempts = 2
    MaxProgress = 1
    LeaseLimit = 1
    ReservationLimit = 1
    LocalLimit = 1
    GlobalLimit = 1
    FaultsEnabled = TRUE
    FaultServices = {"Coordination"}
    MaxCoordLosses = 2
    MaxPartitions = 2

INVARIANTS
    TypeOK
    StateConsistency
    AllocatedTokensUsed
    LiveProgressWellFormed
    LiveProgressCompatibleWithLiveLease
    AtMostOneLiveLeasePerJob
    AuthorityWellFormed
    CommittedResultConsistent
    CancellationSafety
    PermitSafety
    ResumeValidity
    StagingOwnership

PROPERTIES
    TerminalStateIsImmutable
    FencingTokensMonotonic
    CommitIsFencedCAS
    FailureDispositionHonored
Strengthen JobProtocol model after independent review. Replace tautological invariants with non-trivial ones, allow multi-shot coordination loss and re-partition, fix reap/progress lifecycle, enable deadlock checking via Done, and add stress and multi-shot TLC configs. 2026-07-10 12:43:32 +09:00			`SPECIFICATION SafetySpec`

			`CHECK_DEADLOCK TRUE`

			`\* Multi-shot coordination wipe and re-partition (safety only; liveness is Remora.cfg).`
			`CONSTANTS`
			`Jobs = {j1}`
			`Workers = {w1, w2}`
			`InitialWorkers = {w1}`
			`NoJob = NoJob`
			`NoWorker = NoWorker`
			`MaxAttempts = 2`
			`MaxProgress = 1`
			`LeaseLimit = 1`
Specify fenced activation and source credential contracts Define bounded reservation recovery, exact activation replay fencing, immutable source identities, and deployment-owned secret and target policy boundaries. Align the OpenAPI contract and add a split-store activation safety refinement. 2026-07-14 18:12:28 +09:00			`ReservationLimit = 1`
Strengthen JobProtocol model after independent review. Replace tautological invariants with non-trivial ones, allow multi-shot coordination loss and re-partition, fix reap/progress lifecycle, enable deadlock checking via Done, and add stress and multi-shot TLC configs. 2026-07-10 12:43:32 +09:00			`LocalLimit = 1`
			`GlobalLimit = 1`
			`FaultsEnabled = TRUE`
			`FaultServices = {"Coordination"}`
			`MaxCoordLosses = 2`
			`MaxPartitions = 2`

			`INVARIANTS`
			`TypeOK`
			`StateConsistency`
			`AllocatedTokensUsed`
Weaken live progress to a coordination-only hint (IF-6). Drop LiveProgressAligned in favor of well-formedness and lease-compatible progress, stop durable CAS from clearing Redis progress, and add ambient ClearStaleLiveProgress so TLC matches Postgres + Dragonfly separation. 2026-07-10 14:16:29 +09:00			`LiveProgressWellFormed`
			`LiveProgressCompatibleWithLiveLease`
Strengthen JobProtocol model after independent review. Replace tautological invariants with non-trivial ones, allow multi-shot coordination loss and re-partition, fix reap/progress lifecycle, enable deadlock checking via Done, and add stress and multi-shot TLC configs. 2026-07-10 12:43:32 +09:00			`AtMostOneLiveLeasePerJob`
			`AuthorityWellFormed`
			`CommittedResultConsistent`
			`CancellationSafety`
			`PermitSafety`
			`ResumeValidity`
			`StagingOwnership`

			`PROPERTIES`
			`TerminalStateIsImmutable`
			`FencingTokensMonotonic`
			`CommitIsFencedCAS`
Model durable failure disposition 2026-07-13 16:41:51 +09:00			`FailureDispositionHonored`