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

41 lines
967 B
INI
Raw Normal View History

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
\* Combined contention: both local and deployment-wide limits constrain work.
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
\* Shrunk from 3 jobs to 2 so TLC finishes in minutes; Local=1 and Global=2
\* still force both limiters to bind under two live workers.
Add initial draft of Remora model
2026-07-10 11:39:49 +09:00
CONSTANTS
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
Jobs = {j1, j2}
Add initial draft of Remora model
2026-07-10 11:39:49 +09:00
Workers = {w1, w2}
InitialWorkers = {w1, w2}
NoJob = NoJob
NoWorker = NoWorker
MaxAttempts = 1
MaxProgress = 1
LeaseLimit = 1
LocalLimit = 1
GlobalLimit = 2
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
Copy permalink