Every time this topic comes up, it seems people invariably divide into one of two groups. In the first group are those who trust in the odds and play the probability game. In the other, those who demand absolute guarantees. Neither group seems fully capable of understanding the other's standpoint.

Let me add my own perspective: Distributed locks are a fallacy. They can be beneficial in decreasing contention, under the assumption that "most of the time, only one actor will be active". However, by themselves, they offer no solid guarantees. The blog post addresses this point by introducing the concept of fencing tokens. These tokens have the potential to provide concrete guarantees, but they require the cooperation of downstream systems for enforcement, which isn't always possible.

I was really surprised to see Antirez argue for the probability approach.

I don't know why you say neither group understands each other when I literally said in my comment that my approach is probabillistic.

Also, how is configuring an infinite timeout (and checking whether the client is actually gone before manually breaking the lock lease) not an absolute guarantee?

I guess it’s an absolute guarantee, but you lose liveness unless there is some other party handling those cases where the client is truly gone

An infinite timeout works in theory, but it is impractical at scale.

Okay but then I really don't know what point you're trying to make. Either an infinite timeout, or non-absolute mutual exclusion guarantee: we have to pick either one. The right choice depends on the workload. There is no perfect solution that lets you have your cake and eat it too.

Redlocks don't use anything proabilistic, not in the sense that the lock may fail to guarantee what it promises at random.

While that may be true, it’s generally not possible to use red locks to build a correct system is mutual exclusion is a strict requirement

what would you define as a correct system?

Elaborate?