remora/docs/protocol/RemoraLocal.cfg

SPECIFICATION SafetySpec

CHECK_DEADLOCK TRUE

\* Local contention: the global limit permits every worker-local slot.
CONSTANTS
    Jobs = {j1, j2}
    Workers = {w1, w2}
    InitialWorkers = {w1, w2}
    NoJob = NoJob
    NoWorker = NoWorker
    MaxAttempts = 1
    MaxProgress = 1
    LeaseLimit = 1
    LocalLimit = 1
    GlobalLimit = 3
    FaultsEnabled = FALSE
    FaultServices = {}
    MaxCoordLosses = 0
    MaxPartitions = 0

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

PROPERTIES
    TerminalStateIsImmutable
    FencingTokensMonotonic
    CommitIsFencedCAS
Add initial draft of Remora model 2026-07-10 11:39:49 +09:00			`SPECIFICATION SafetySpec`

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			`CHECK_DEADLOCK TRUE`
Add initial draft of Remora model 2026-07-10 11:39:49 +09:00
			`\* Local contention: the global limit permits every worker-local slot.`
			`CONSTANTS`
			`Jobs = {j1, j2}`
			`Workers = {w1, w2}`
			`InitialWorkers = {w1, w2}`
			`NoJob = NoJob`
			`NoWorker = NoWorker`
			`MaxAttempts = 1`
			`MaxProgress = 1`
			`LeaseLimit = 1`
			`LocalLimit = 1`
			`GlobalLimit = 3`
			`FaultsEnabled = FALSE`
			`FaultServices = {}`
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			`MaxCoordLosses = 0`
			`MaxPartitions = 0`
Add initial draft of Remora model 2026-07-10 11:39:49 +09:00
			`INVARIANTS`
			`TypeOK`
			`StateConsistency`
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			`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`
Add initial draft of Remora model 2026-07-10 11:39:49 +09:00			`CommittedResultConsistent`
			`CancellationSafety`
			`PermitSafety`
			`ResumeValidity`
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			`StagingOwnership`
Add initial draft of Remora model 2026-07-10 11:39:49 +09:00
			`PROPERTIES`
			`TerminalStateIsImmutable`
			`FencingTokensMonotonic`
			`CommitIsFencedCAS`