It’s a choice between at-least-once and at-most-once right? Without a timeout you get at-most-once since the lease holder may die off and never complete the task, and so the task of a completed 0 times.
I’m building a system right now and we’re going to use lease/heartbeats etc etc to elect leaders and whatnot, all this discussion seems very practical to me.
Exactly. It comes down to whether the consequences of these race conditions are acceptable or not. Sometimes (known and understood) race conditions are okay for performance reasons. Shoot, that's the whole philosophy behind eventual consistency. Sometimes they aren't, such as bank transactions. It's all situational.
Eventual consistency isn't a philosophy, and it's not the idea that race conditions are acceptable. It's a consistency model with specific properties and guarantees.
These races we're talking about don't produce eventual consistency, but inconsistency. Different systems require different levels of correctness, but if you're not familiar with the underlying theory then your trade-offs are going to be uninformed decisions rather than informed ones.
A race condition is the lack of determinism in a sequence of events that can lead to undesirable effects. Eventual consistency is an approach (and consistency model, design philosophy, whatever you want to call it) that accepts this lack of determinism as a compromise because the possible sequences are accounted for, since the system can still act on stale data until an update is fully pushed out (which is still undesirable, but an accepted compromise).
I haven't looked at Redlock for a while, but I'm assuming you're all across the historical objections to it from distributed systems researchers: https://martin.kleppmann.com/2016/02/08/how-to-do-distribute...