Locks, leases, fencing tokens, FizzBee
9 comments
·March 18, 2025peheje
Can someone explain to me how it makes sense that you want to define a locking mechanism using.. locking mechanism (the "atomic"). 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?
Also won'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?
OJFord
Well it's not a general purpose programming language defining the actual lock this way, it's checking a locking algorithm; so the atomic in the specification of the algorithm is just saying given that these steps do occur atomically, how will it behave.
The algorithm we're checking is using Redis, and the atomic read/write in the example is a behaviour Redis gives you.
macintux
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.
legerdemain
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're building.
shermantanktop
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?
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.
singron
If you can model your mutation as a database transaction, then that's probably the best. In the past, we've wanted these kinds of solutions when performing actions that weren't in a transactional database. E.g. third party APIs, multiple databases, non-transactional databases, work assignments, rolling restarts and other risky control plane changes. Also a lot of databases can degrade performance when transactions are held open (e.g. in postgres, an open transaction will prevent the cleanup of dead tuples across all tables, which can cause pathological slowdowns in certain workloads), so you might want to move long-held locks out of your database.
shermantanktop
Oh absolutely. I have a horror story about Hibernate and annotations taking a lock while listing objects in S3. Someone added a million objects to the bucket and…bad things ensued.
sriram_malhar
Depends on the consistency guarantee and workload.
If it is just linearizability (atomic key-value storage) then write-through caches work simply and correctly. You reap the benefits on the read side.
You can fix this scenario by incrementing the next_token when you commit the critical section instead of when you enter (if that'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.
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.