Locks, leases, fencing tokens, FizzBee

You can fix this scenario by incrementing the next_token when you commit the critical section instead of when you enter (if that&#x27;s possible for your domain). This essentially makes it an optimistic lock instead of a pessimistic lock. Two threads can get the same fence token, but only one will be able to commit.<p>You can often rephrase and algorithm without a commit step into one that has one, although sometimes it can feel more complicated. E.g. instead of doing A and B in a critical section, commit an intent to do A and B, and then let an idempotent process execute that intent.

Can someone explain to me how it makes sense that you want to define a locking mechanism using.. locking mechanism (the &quot;atomic&quot;). Does this mean that in an actual implementation you would have to drop down to some hardware-level-atomic operation, and is that even practical?<p>Also won&#x27;t fencing token require some kind of token manager, that ensures you must present the highest token to do the action, and that you have to ask to get a new token, and that when you fail because your token is too old you must re-request one, is this modelled?

Very nice write-up. First time I’ve finished an article about formal proofs and thought to myself I’d like to give it a try.

Remind me again why I would want to pull consistency guarantees out of an actual datastore (which is designed to provide those guarantees) and force-fit that problem into a fancy caching layer?<p>The Kleppman critique about efficiency vs correctness is exactly right. Redis for efficiency is great as a work-saving optimization. Redis for correctness (assuming it is possible) asks a remote system to enforce behavior at a far remove from the place where correctness is evident, which is system state, usually data in a datastore.

The creator of FizzBee presented it at the most recent meeting of the SF Systems Club. The talk was some kind of meandering hybrid between presentation and tutorial and went far over time, but FizzBee itself sounds rich in features and simple to use. Its creator is pitching it as an easy-to-use verification tool for software teams in industry to document and verify the systems they&#x27;re building.