ms2k
a3f502f6b6
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.
41 lines
967 B
INI
41 lines
967 B
INI
SPECIFICATION SafetySpec
|
|
|
|
CHECK_DEADLOCK TRUE
|
|
|
|
\* Combined contention: both local and deployment-wide limits constrain work.
|
|
\* 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.
|
|
CONSTANTS
|
|
Jobs = {j1, j2}
|
|
Workers = {w1, w2}
|
|
InitialWorkers = {w1, w2}
|
|
NoJob = NoJob
|
|
NoWorker = NoWorker
|
|
MaxAttempts = 1
|
|
MaxProgress = 1
|
|
LeaseLimit = 1
|
|
LocalLimit = 1
|
|
GlobalLimit = 2
|
|
FaultsEnabled = FALSE
|
|
FaultServices = {}
|
|
MaxCoordLosses = 0
|
|
MaxPartitions = 0
|
|
|
|
INVARIANTS
|
|
TypeOK
|
|
StateConsistency
|
|
AllocatedTokensUsed
|
|
LiveProgressWellFormed
|
|
LiveProgressCompatibleWithLiveLease
|
|
AtMostOneLiveLeasePerJob
|
|
AuthorityWellFormed
|
|
CommittedResultConsistent
|
|
CancellationSafety
|
|
PermitSafety
|
|
ResumeValidity
|
|
StagingOwnership
|
|
|
|
PROPERTIES
|
|
TerminalStateIsImmutable
|
|
FencingTokensMonotonic
|
|
CommitIsFencedCAS
|