Did anyone else ever publish a meaningful response? I thought Antirez's response was reasonable but I also recognize the inherent bias. I'd love to see responses from other experts, ideally written such that non-experts can reasonably understand.
I recall several people on twitter (I follow a lot of distributed systems people / cs professors as it is part of my job to build these things) who agreed with Martin's analysis.
Honestly given Antirez's response I'm genuinely surprised no one has written a TLA+ or similar formal verification proof. Then the outcome is binary; either redlock is sound and works as expected, or it is not.
Amazon's AWS Architect, James Hamilton is a big fan of this approach, as are most of the heavyweights in distributed systems:
Let me be clear, I think redis is a well engineered piece of software and I have been constantly impressed with the way antirez runs the project.
Specifically for the question of a locking service, I need more availability than what a single node can offer. I'm not sure if you are advocating for using redis cluster as a locking service, but since it intentionally doesn't offer write safety during a partition that does not seem advisable.