The System Model — the Assumptions an Algorithm Is Proven Correct Inside
two hierarchies of assumptions on the left and right · safety and liveness properties along the bottom
«abstract» TimingModel
network delay : bounded?
pause + clock error : bounded?
Synchronous
known upper bound on delay,
pauses and clock drift
PartiallySynchronous
bounded most of the time,
sometimes exceeded
Asynchronous
no timing assumption at all,
not even a clock
timing assumptions
«abstract» FaultModel
crash : allowed? recovery : returns?
behavior : honest or arbitrary?
CrashStop
stops once, never comes back
CrashRecovery
restarts later, memory lost
Limping (fail-slow)
answers health checks, no work
Byzantine
may lie, forge, or contradict itself
fault assumptions
The practical combination
partially synchronous
+ crash-recovery
delays, pauses and slow nodes
are all allowed to be unbounded
algorithms are proven inside
exactly this world
Safety — nothing bad happens
a violation has one moment in time
once broken, it cannot be undone
e.g. token uniqueness, monotonic order
Liveness — something good eventually
may be false now, may become true
the definition says "eventually"
e.g. availability, eventual consistency
How an algorithm uses them
safety must hold in every situation
liveness may assume a recovery
"if the network comes back and a"
majority survives, a reply arrives"
Models are simplifications: crash-recovery assumes stable storage survives a crash, yet a misconfiguration can wipe the disk and break the model itself.