Is Redlock Safe? Reply to Redlock Analysis
antirez.com
antirez.com
First, Antirez claims that requiring the "materialization" store to be able to tie break with a monotonically increasing token requires linearization? This is completely false. The monotonically increasing token allows for eventual consistency. That's the entire point of it. It's monotonically increasing.
For anyone who claims that once you have coordination (locking) in your system you already lost is completely ignoring the research coming out of BOOM (Berkeley Orders of Magnitude). You can design your system to push the coordination out to the edge and way from your "choke points" and use these monotonically increasing tokens to keep your bottlenecks coordination free.
Secondly, Antirez's argument that you can use a compare & swap in a transactional storage layer is also wrong. This is not possible to write safely.
I'm not even going to touch his argument that using system clocks in a distributed locking algorithm is safe...
This discussion is very interesting and I would like to read up a bit more on your argument and why is this so.
I know that distributed systems are hard, but this is a problem that I find interesting to learn more about.
Martin provided a number in his original blog post, I also elaborated a bit more on my various points in other comments.
I read a bit on BOOM and it's not a field I'm keeping up with so I figured it would be no point in more references if I didn't understand the more shallower levels of the discussion first.
Sorry about that, I tried to jump a bit too soon, and thanks for answering :)
Could you elaborate on this? I'm not sure I'm as pessimistic as you on this one point.
I believe that antirez's proposal is the former, but if he has a safe algorithm that does not require a linearizable CAS operation in the storage layer and is safe w/ redlock, I would love to hear it.
I also provided an example of how to use Cassandra which is eventually consistent safely with a locking service that provides monotonic tokens.
Please do
If I have a 5 second lock that expires at 12:01:00 and my clock is off by 1 second I could write at 12:01:01 potentially after someone else has a lock, or worse, after someone else has written.
> The client computes how much time elapsed in order to acquire the lock, by subtracting from the current time the timestamp obtained in step 1. If and only if the client was able to acquire the lock in the majority of the instances (at least 3), and the total time elapsed to acquire the lock is less than lock validity time, the lock is considered to be acquired.
or daylight savings change?
or ntp updates which change the time?
Since the system clock can change relative to itself at any time, what effect does that have on the algorithm?
> VM live migration "pause"?
System clock will take a larger step than usual. It won't go backwards.
> daylight savings change?
None. System clock is UTC for a reason.
> ntp updates which change the time?
NTP only drifts the clock (under normal operation).
System clock will take a larger step than usual. It won't go backwards.
Assumes that checkpoint and restore to a previous time won't happen.
NTP only drifts the clock (under normal operation).
Unless it's a system like this. Note that this was pulled at about 1pm EST.
Waiting for clock tick...
...got clock tick
Time read from Hardware Clock: 2016/02/09 22:36:50
Hw clock time : 2016/02/09 22:36:50 = 1455057410 seconds since 1969
Tue 09 Feb 2016 02:36:50 PM PST -1.038948 seconds
'Under normal operation' is not really a high bar for distributed systems. After all, the network is reliable 'under normal operation' too.
Or migration to a host whose clock is behind the original host's clock.
If someone forks a VM from a running snapshot, you're screwed whether they mess with the clock or not.
That shouldn't be an assumption. NTP may jump the clock if the difference is too high, I've had it once that a system was connected to two different NTP servers and they each had a different clock and the system would jump the clock every now and then based on what NTP server it though was more correct.
A client can never know with certainty that it has successfully acquired the lock because, for example, the process could freeze between reading the current time from hardware and the steady_time function returning.
You can not rely on time, for safety. Only for advice.
This is not eventual consistency, this is refusing any new write with ID < past_ID, which requires linearizability.
Second, about eventual consistency, the Token ID even when increasing may not be casually related with the work performed while the lock is hold. if you need just a random order when there are concurrent accesses, you can lexically order the random token IDs, for what is worth.
Compare & Swap: could you argument that? If you want to avoid races in a read-modify-write scenario, you can set the token, do your work, and only write if the token is still the same, so that if your write succeed is because the state of the shared resource is still the same to when you started operating on it.
2. If your data store can always accept the write only if
your token is greater than all the past tokens, than it’s a
linearizable store. If you have a linearizable store, you
can just generate an incremental ID for each Redlock
acquired, so this would make Redlock equivalent to
another distributed lock system that provides an
incremental token ID with every new lock. However in the
next point I’ll show how this is not needed.
3. However “2” is not a sensible choice anyway: most of the times the
result of working to a shared resource is not writing to a linearizable
store, so what to do? Each Redlock is associated with a large random
token (which is generated in a way that collisions can be ignored. The
Redlock specification assumes textually “20 bytes from /dev/urandom”).
What do you do with a unique token? For example you can implement Check
and Set. When starting to work with a shared resource, we set its state
to “`<token>`”, then we operate the read-modify-write only if the token
is still the same when we write.
* process A acquires lock
* process B acquires a lock on the same resource after a time out and sets it's lock id on the resource
* process A sets it's lock id on the resource
* process A writes a new version of the resource
* process B attempts and fails to write a new version of the resource
if it's not correct, would you say redlock prevents it? how?
now consider what happens if the resource is only one of a group of resources that need to be transactionally updated
the bottom line is that distributed transactional locking requires linearization and redlock is plainly not linearizable. please reconsider it's continued development and steer users towards something safer like zookeeper
I don't think you understand Martin motivations. He says that the system has to reject the write with a lower ID, in order to protect from concurrent accesses, and to do so in a way that the client attempting a stale write is notified.
If you mount an eventually consistent system returning the object with higher version, there is nothing of linearizable about it. If the shared resource is a list of names, one client will try to add "Hellen" with version 8, one will try to add "Josh" with version 9. Only one name will end in the list in your schema, and the client adding "Josh" will not even know that the write failed.
So the goal is, when race conditions happen, to avoid them in some way. While I believe that when you use a distributed lock the problem is very often that you don't have other controls over the shared resource, if you really need to do that, a random token is equivalent: using CAS you can reject one of the writes if two clients are writing at the same time.
Note also that when it happens that, because of delays, the clients are accessing concurrently, the lock ID has little to do with the order in which the operations were indented to happen. Back to "add name to a list" problem:
T0: Client A receives new name to add from web.
T0: Client B is idle
T1: Client A is experiencing pauses.
T1: Client B receives new name to add from web.
T2: Client A is experiencing pauses.
T2: Client B receives a lock with ID 1
T3: Client A receives a lock with ID 2
...
So the client that received the name before, can do the operation after, or you can have delays in any other part of the system.
using a random token is not equivalent to using a linearizable lock, see: https://medium.com/@talentdeficit/redlock-unsafe-at-any-time...
i am not sure what your point about delays and concurrent clients is, of course a system can't infer order from events that happen outside of it's visibility. the lock system can only provide synchronization at the point the lock is acquired
If you write to a store like cassandra using a monotonic token, the result will converge correctly. If you require to never read "stale" data, you can read / write w/ quorum. There is no linearization in the storage layer in this case.
In this case the lock is not superfluous and you have safety.
Regarding CAS, I said that your argument (in support of redlock) was wrong. I would be happy to respond to a proposed algorithm, but as someone else mentioned, either the storage layer can provide a CAS operation, in which case your lock is not required and the workers read, mutate, CAS, OR if the storage layer has any weaker semantics then it is not possible to ensure safety with a token.
Yeah, so Optimistic Concurrency Control. Possibly a Redlock-like lease scheme could be used to improve performance in the high-contention case.
He's using it relatively, ie. if (stop time - start time <= $got_lock_fast_enough) { continue... } Is this not legit?
Personally, though, I don't see why it's so hard to just say "this distributed lock system requires that soft real-time guarantees can be made of the host platform. If the platform misses the algorithm's scheduling deadline, the system breaks. If the platform has no way of providing for a soft real-time deadline (because e.g. it's running in a VM that can be paused), the software will detect this and fail to start."
Do you think NASA quibbles about how to make a perfect consensus bit-coding algorithm between the fault-tolerant processors of a mars probe? No; they just use hardware+firmware that provides a hard real-time platform, allowing the algorithm itself to be simple.
It doesn't take a lot to have backwards time travel, NTP can do that for you as well in some bad configurations.
It's very hard to rely on time in a distributed system. If you want a simple algorithm just don't rely on time at all, use it for logs so a human can correlate things when debugging an issue but don't assume time will flow at the same rate for all systems. Do use a monotonic clock always for internal timers, time does move backwards in systems.
In short, you CANNOT rely on time in any way shape or form for safety. You can only use it as advice & to get liveliness.
Martin's point is that Redlock pays the cost of other safe locking algorithms w/o the benefit of safety.
http://www.cse.buffalo.edu/~demirbas/publications/augmentedT...
1. Most of the times when you need a distributed lock system that can guarantee mutual exclusivity, when this property is violated you already lost. Distributed locks are very useful exactly when we have no other control in the shared resource.
In context, Sanfilippo seems to be arguing that providing monotonic logical timestamps or sequence numbers is futile, since a system that relies on locks that break is going to fail one way or another.
That is probably true, but wildly misses the point: when a sound system that relies on distributed locks fails, it doesn't silently corrupt data. But that's exactly what happens in the "unfenced" lock-breaking scenario Kleppmann describes.
There are worse things than crashing, is the point.
slightly later
The argument about storage servers taking fencing tokens being "linearizable" also seems flimsy: aren't they "linearizable" (in whatever sense Sanfillippo means) in the case Kleppmann because because the lock service arranges for them to be? That's functionality Kleppmann says is missing from Redlock.
You want to modify locked resource X. You set X.currlock = token. Then you read, do whatever you want, and when you write, you "write-if-currlock == token". If another client did X.currlock = somethingelse, the transaction fails.
Edit: note that I noticed some confusion about this. Any other client is free to replace X.currlock even if set to a past value.
try
token=lock.aquire
val=raw(shared, key, token)
do_things
awar(shared, key, val, token)
fail("Can't do!")
lock.release
When things go wrong, the do_things may be executed more than once, in parallel, but the key is safe and guaranteed to have no lost updates to its value.
Doesn't it mean that this can happen?
A: X.currlock = Token_ID_A
A: resource read
A: is X.currlock still Token_ID_A? yes
B: X.currlock = Token_ID_B
B: resource read
B: is X.currlock still Token_ID_B? yes
B: resource write
A: resource write
https://en.wikipedia.org/wiki/Test-and-set
https://en.wikipedia.org/wiki/Test_and_test-and-setThe monotonic sequence provides that detection means. So in the example you gave, the tardy (expired) tx commit would abort since its lock id would break the monotonic sequence of accepted lock-ops (which clearly can have gaps, 1, 2, 4, 6, 7, ... etc.[)]
"Note that, with careful optimization, only 14 gajillion messages are necessary. This is still too many messages; however, if the system sends fewer than 14 gajillion messages, it will be vulnerable to accusations that it only handles reasonable failure cases, and not the demented ones that previous researchers spitefully introduced in earlier papers in a desperate attempt to distinguish themselves from even more prior (yet similarly demented) work."
from James Mickens' "The Saddest Moment" - https://www.usenix.org/system/files/login-logout_1305_micken...
Personally I'd prefer stronger proofs than even those, but I think those papers get us to the point where implementation issues are as important as theoretical issues.
In my personal opinion, Redlock is not at the point where we even need to consider the implementation.
The fact that a protocol (e.g. Raft) has been proven correct sets the floor but it is certainly not sufficient to assume correctness of an implementation.
Indeed. This is where tools like Jepsen and good fuzz testing can help.
Proofs will typically show the limitations of an algorithm, for instance the original paxos paper notes that the contained algorithm does not provide liveliness.
A system based on an algorithm with a proof has some chance of being correct, while a system based on an algorithm with no proof while technically it may have a non-zero probability of being correct that probability approaches zero.
Having worked on such systems and having talked to some people who have worked on debugging issues with paxos implementations at extreme scale while it is virtually impossible to to ensure that the system will be able to make forward progress it is possible to ensure that the state of the state machine remains correct.
When I look at an implementation of such an algorithm to evaluate it I pay very careful attention to the test suites. The more bizarre the tests they contain the more likely the implementation is to handle very weird network edge cases.
Raft isn't. (I actually don't believe Paxos or Zookeeper do either, but I only understand Raft, so let me speak for that one.) Directly from the link in the post you're responding to:
> Consensus algorithms for practical systems typically have the following properties:
> They ensure safety (never returning an incorrect result) under all non-Byzantine conditions, including network delays, partitions, and packet loss, duplication, and reordering.
This applies to Raft, as well: Raft-the-algorithm will behave correctly during these events. The paper linked to above provides a proof of such.
> The fact that a protocol (e.g. Raft) has been proven correct sets the floor but it is certainly not sufficient to assume correctness of an implementation.
These are two separate things, and you need both. You need to know that an algorithm is sound, that it accomplishes what it sets out to do. You also need to know that a particular implementation of an algorithm is correct.
(While I said I haven't read the ZK paper, it does mention,
> Paxos does not require FIFO channels for communication, so it tolerates message loss and reordering.
)
For example, a lot of people say, "updating a bank balance". But even that can easily be eventually consistent. You send increments and decrements and settle up at the end. Yes, your balance might go negative, but that's what ATM limits are for -- the most you could go negative is that limit. Most other systems can be written the same way. And for non-numeric values, there are always vector clocks or timestamps or quorum to determine which update came next, or you could send a client a list of all recent updates and let the client "do the right thing".
Hope you're doing well BTW!
I didn't expect it to be a perfect system but I don't want to deal with setting up a queuing system right now when there simply isn't enough activity taking place.
Will it fail at some point? Possibly, but it's a great intermediary solution as you state. I for one would be curious to see other solutions to this problem. Are there any resources you'd recommend?
Banks have generally solved this by batching updates, but yes, it could be unsettling for the customer in a similar situation. There are ways around that though, for example you update a cache that stores the data instantly and then let the eventually consistent source of truth update the cache again if it is not in sync, or perhaps have a short timeout on the cache, so the customer gets a consistent and smooth experience but the source of truth is still accurate, eventually.
Leader election generally[1] requires consensus among distributed processes, and global locks generally[1] require consensus as well. The benefit of this is that both problems can be solved on top of a common consensus implementation which is what http://atomix.io does.
1: I say generally because you can do fancy things with fancy clocks to avoid running operations through a quorum under certain circumstances, but these carry caveats that preclude them from being reliable enough to use in many use cases.
Also, eventual consistency is a weak requirement that, when sufficient, enables a certain level of fault tolerance and low latency not achievable with other consistency levels (see [1]), although other consistency levels may offer good-enough fault-tolerance and latency (rivaling EC in many cases). EC is not in general the solution to the problem of "how do I best distribute my data?"
[1]: http://www.bailis.org/blog/when-does-consistency-require-coo...
Absolutely, but if you can avoid using global locks, which are error prone and reduce reliability, isn't that a good thing?
In other words: if you set out to create Bitcoin in 1998, you might end up running into distributed consensus problems that are difficult enough that you decide to "solve an easier problem"—such that you end up creating Paypal instead.
I think that while this may be true for many requirements, consistency is among the least flexible ones. Besides, losing consistency usually makes your system more complicated, not less. Weak consistency has some real benefits (latency in some cases, tolerance for more failure modes), but simplicity is not usually one of them.
> In other words: if you set out to create Bitcoin in 1998, you might end up running into distributed consensus problems that are difficult enough that you decide to "solve an easier problem"—such that you end up creating Paypal instead.
I don't think that the design problems behind Bitcoin are any easier than distributed consensus, which, BTW, is not necessary for quite a few consistency levels.
""" If you read the Redlock specification, that I hadn't touched for months, you can see the steps to acquire the lock are:
1. Get the current time.
2. … All the steps needed to acquire the lock …
3. Get the current time, again.
4. Check if we are already out of time, or if we acquired the lock fast enough.
5. Do some work with your lock.
...
The above also addresses “process pauses” concern number 3. Pauses during the process of acquiring the lock don’t have effects on the algorithm's correctness. """
What if the process GCs for 2 minutes between 4 and 5? Then the lock times out, but the process still does its work with the lock, even though another process may think it has the lock as well.
This is a specific example of the criticism that you cannot rely on clock checks for correctness that has been made elsewhere.
As a RDBMS aficionado, that whole stack made me puke, BUT, to all the really smart people here having a PHD in distributed systems, please : try to help antirez build something that works. Many developers are trying to reach the shore of consistent systems after having been lost in the ocean of "NoSQL is great for everything".
Note : and i'm not saying redis is to blame here. It's obviously a great software. It's mostly the users that are to blame in this case.
In practice, failure detectors mean timeouts. What I am arguing is that you can have systems that adapt their timeouts for failure (such as our one), based on the current level of network congestion or load or whatever. The setting/changing of the timeout is averaged over a period of time, to ensure it is high enough to not give false positives. You could do the same approach at the per message level, but for all possible messages, it may be prohibitive. If you have a small number of messages, it may work. The problem with messages, compared to failure detection, however, is the following: how do you figure out you have had a false positive? For failure detection it's easy: the timeout expired, butre i'm still alive and my heartbeat arrives late, so we increase the timeout for that node. Vector clocks (fencing tokens) make it easier to reliably find out if messages arrive very late (identify false positives).
I would encourage everyone to be civil and patient, and if you have the time, expand on what you're writing so that those of us who are not experts can learn something.
Reading through the original description of Redlock[1] and your "rebuttal" is interesting. The algorithm described in the spec isn't safe if a GC pause or process pause happens between <checking how long it took to acquire a majority> and <doing work and releasing the lock>. You don't even touch this argument (pretending to not understand which step is the problem and defending that everything before the gap I just described is safe).
You claim that fenced tokens require linearizablity. I don't know if this is true, but even if it is all you've proven is that the solution offered isn't good enough. The fact that something that tries to fix your system doesn't fix it properly doesn't mean that your system isn't broken.
Longer answer: provided that things never go wrong it works. But the assumption that things never go wrong is false. In particular the whole basis of the original point is that there is no true universal time, and this post (essentially) says "provided that there is universal time then I can't see what you are complaining about"
Swing and a miss.
1. Try real time kernel extensions.
2. Try a time bomb or watchdog process as you suggested.
3. Put monitoring systems to avoid load to go over a certain level.
4. Tune the Linux scheduler params.
5. Use TTLs that are comparatively very large compared to the work you need to do with the lock hold.
> 1. Distributed locks with an auto-release feature (the mutually exclusive lock property is only valid for a fixed amount of time after the lock is acquired) require a way to avoid issues when clients use a lock after the expire time, violating the mutual exclusion while accessing a shared resource. Martin says that Redlock does not have such a mechanism.
The section "Distributed locks, auto release, and tokens" talks about why Martin's solution isn't right (I'm not well-read enough to tell if that argument is correct), but never actually argues that Redlock has a mechanism to avoid violation of mutual exclusion due to timeouts.
Perhaps I'm missing some background here: does such a mechanism exist?
I'm also not a distributed systems expert, but this is how I interpreted the arguments. AntiRez is responding to the scenario where a client acquires a lock, hangs, a new client acquires a lock, and the old client comes back and tries to write something based off of a now stale lock. As demonstrated in this image [0]
So the random token ensures that even though many clients may "think" they have a lock, only up to a single client can ever actually have one. The write in the diagram which corrupts the database shouldn't happen, because you'll need to check that your lock token matches the service. [1] (excuse the terrible MSPaint modifications).
Which covers the common cases of lock timeout. But the clients aren't the only part of the system that can violate the mutex. Martin seems to have already thought of this rebuttal:
You cannot fix this problem by inserting a check on the lock expiry just before writing back to storage. Remember that GC can pause a running thread at any point, including the point that is maximally inconvenient for you (between the last check and the write operation).
[ ... ]
If you still don’t believe me about process pauses, then consider instead that the file-writing request may get delayed in the network before reaching the storage service. Packet networks such as Ethernet and IP may delay packets arbitrarily
Martin's fix [2] is similar to the token method suggested, except: A) the write-if-token-matches logic is handled directly by the storage layer. B) It uses an auto-incrementing token.
He spends a few paragraphs making the point that redlock cannot generate good fencing tokens, because it has no good auto-increment consensus. But I don't see how a random token is any worse than an incrementing one if you're just going to straight up reject requests where the token doesn't match. Antirez addresses this, without addressing A.
I would also really like someone to correct me if I'm missing something. The Redlock implementations are very bare-bones with tests or examples of how to actually use them. The Ruby library has a more "advanced" example, which says this at the point where they try writing to the file system:
# Note: we assume we can do it in 500 milliseconds. If this
# assumption is not correct, the program output will not be
# correct.
[0] http://martin.kleppmann.com/2016/02/unsafe-lock.png
[1] http://i.imgur.com/8rezAaX.png
[2] http://martin.kleppmann.com/2016/02/fencing-tokens.png
[3] https://github.com/antirez/redlock-rb/blob/master/example2.r...
No, random tokens are not worse per se, they just have no place in the algorithm Martin described. It's a completely different system. In that system incremental tokens presume a mechanism that gives you a way to have some order of events. And one can rely on that order to decide which requests with which tokens to reject.
> About claim 1: This is not an issue, we assumed that we can count time approximately at the same speed, unless there is any actual argument against it.
https://aphyr.com/posts/299-the-trouble-with-timestamps
> Timestamps, as implemented in Riak, Cassandra, et al, are fundamentally unsafe ordering constructs. In order to guarantee consistency you, the user, must ensure locally monotonic and, to some extent, globally monotonic clocks. This is a hard problem, and NTP does not solve it for you. When wall clocks are not properly coupled to the operations in the system, causal constraints can be violated. To ensure safety properties hold all the time, rather than probabilistically, you need logical clocks.
> A somewhat less safe but reasonable option is to use NTP rigorously on your machines, and sync it to TAI or GPS instead of POSIX time or UTC. Make sure you measure your clock skew: everyone I know who says they run NTP has discovered, at one point or another, that a node was way out of sync. If you want rough correspondence to POSIX time, you can still ensure monotonicity by running your own NTP pool and slurring leap seconds over longer time frames.
Clock skew is a very real problem and virtually impossible to avoid 100% of the time. Particularly when you have things like leap seconds where the fundamental concept of how many seconds in a day get changed.
https://en.wikipedia.org/wiki/Leap_second
System clocks are fundamentally unsafe if you just use NTP. That isn't to say you can never do it. Some use cases it is "safe enough" [e.g. Analytics, Metrics] where the occasional fuck up isn't substantial but Antirez isn't making that argument with Redlock as far as I can tell.
> “Okay, so maybe you think that a clock jump is unrealistic, because you’re very confident in having correctly configured NTP to only ever slew the clock.” (Yep we agree here ;-) he continues and says…)
That still isn't reliably safe because there is no guarantee all nodes will perform the slew identically.
https://www.youtube.com/watch?v=EYJnWttrC9k
https://mesoscon2015.sched.org/event/3Aot/keynote-silence-is...
For data which absolutely must never violate the lock then the underlying data storage has to be involved. The vast majority of times where a distributed lock is used is where the underlying storage doesn't provide any support and the distributed lock is good enough, failures are exceptional and not disastrous.
If you want perfect correctness then you can just not have auto-release but practically this will cause more problems than it solves.
In general, I don't understand why one would build a system that attempts to approximate consensus without just using one of the proven consensus algorithms. Redlock is not the only one here, there are other systems that do this as well.
[1] https://github.com/atomix/atomix-jepsen
[2] https://www.datastax.com/dev/blog/testing-apache-cassandra-w...
[3] https://foundationdb.com/blog/call-me-maybe-foundationdb-vs-...
It is a bit of work and learning curve writing a Jepsen test suite, but it's not too bad, particularly with the excellent docs that Kyle has recently written:
https://github.com/aphyr/jepsen/blob/master/doc/scaffolding....
For example Consul did their own Jepsen testing[1] in which they passed them, but Kyle pointed out [2] that they passed them only because they changed timeouts from 1 s to 300 ms effectively making the race condition window smaller.
[1] https://www.consul.io/docs/internals/jepsen.html [2] https://aphyr.com/posts/316-call-me-maybe-etcd-and-consul
The best method we currently have for demonstrating that large systems are safe is to try really hard to prove that they are unsafe and fail.
A lock should result in linearized access (all resources updated while holding the lock should be updated in the same order based on the time when the lease was granted). A counter is enough to put the updates in order. Giving leases a unique id doesn't do that - the network could reorder writes seen by two different resources. Fencing ensures that if the network does reorder writes, one of them fails.
The lock is acting sort of like a clock that ticks whenever it hands out a lease. The resources effectively update their local clock whenever they see an update with a new token from the central clock, and use this local clock to detect stale writes.
Note that fencing doesn't guarantee that writes don't happen late - all updates could be delayed by 10 seconds and it wouldn't catch it. But it isn't feasible to prevent this on systems with bad clocks connected by a flaky network.
> ... The good thing is that distributed systems are, unlike other fields of programming, pretty mathematically exact, or they are not, so a given set of properties can be guaranteed by an algorithm or the algorithm may fail to guarantee them under certain assumptions. In this analysis I’ll analyze ..
Saw no mathematics in your article.
Specifically the paper entitled Time, Clocks and the Ordering of Events in a Distributed System. [1]
This is basically the seminal paper on distributed systems and should be required reading for anyone considering playing with distributed locking mechanisms.
[1] http://research.microsoft.com/en-us/um/people/lamport/pubs/t...
TLA+ seems pretty good at this. Why would this be a waste of effort?
For instance, the issue around the usage of fencing tokens to reject any late usage of a lock is unclear just because the protected resource and its access are themselves unspecified. Is the resource distributed or not? If distributed, does the resource has a mean to ensure that tokens are increasing over all the nodes? Does the resource have a mean to rollback any effects done by a client which session is interrupted by a timeout?
Likewise for the timing arguments. It seems clear to everyone that timeouts provide only some protection rather than a guarantee. A more precise timeline of the worst case scenario will help to estimate that protection given the misc timeout values and clock shifts.
I believe the "first" write fails, because the token being passed in is no longer "the lastest", which indicates their lock was already released or expired.
Is it not useful to do so?