ms2k/remora
SHA256
Watch
0
Code Releases Activity
remora/docs/protocol/Remora.cfg

49 lines
1.1 KiB
INI
Raw Normal View History

Add initial draft of Remora model
2026-07-10 11:39:49 +09:00
SPECIFICATION Spec
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
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
\* Fair Spec + liveness under coordination faults. Fault budgets are 1 so
\* temporal checking finishes in minutes; multi-shot budgets are covered by
\* RemoraMultiShot.cfg (safety-only).
Add initial draft of Remora model
2026-07-10 11:39:49 +09:00
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
Add initial draft of Remora model
2026-07-10 11:39:49 +09:00
LocalLimit = 1
GlobalLimit = 1
FaultsEnabled = TRUE
FaultServices = {"Coordination"}
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 = 1
MaxPartitions = 1
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
Model durable failure disposition
2026-07-13 16:41:51 +09:00
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
EventuallyDispatched
Add initial draft of Remora model
2026-07-10 11:39:49 +09:00
EventuallyReaped
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
EventuallyAuthorizedResolved
Add initial draft of Remora model
2026-07-10 11:39:49 +09:00
EventuallyTerminal
Add eventual cleanup liveness and fix cancel quiescence gaps. Encode zero-orphan intent as EventuallyNonWinnerStagingCleaned and EventuallySystemQuiescent under recovery. Stop authorized attempts on FinalizeCancel and do not re-publish cancel notices after terminal so fair behaviors can reach SystemQuiescent (TLC-checked on Remora.cfg).
2026-07-10 14:46:55 +09:00
EventuallyNonWinnerStagingCleaned
EventuallySystemQuiescent
Copy permalink