Multi-version concurrency control in TLA+

In the previous blog post, we saw how a transaction isolation strategy built on multi-version concurrency control (MVCC) does not implement the serializable isolation level. Instead, it implements a weaker isolation level called snapshot isolation. In this post, I’ll discuss how that MVCC model can be extended in order to achieve serializability,...

A play in one act Dramatis personae Scene 1: A meeting room in an office. The walls are adorned with whiteboards with boxes and arrows. EM: So, do you think the team will be able to finish all of these features by end of the Q2? TL: Well, it might be a bit tight, but … Continue reading The carefulness knob →

Concurrency is really, really difficult for humans to reason about. TLA+ itself was borne out of Leslie Lamport’s frustration with the difficulty of write error-free concurrent algorithms: When I first learned about the mutual exclusion problem, it seemed easy and the published algorithms seemed needlessly complicated. So, I dashed off a simple...

This is one of my favorite bits from fellow anglophone Québécois Norm McDonald: One of the goals I believe that we all share for post-incident work is to improve the system. For example, when I wrote the post Why I don’t like discussing action items during incident reviews, I understood why people would want to … Continue reading If you don’t...

If you’ve ever sat at a stop light that was just stuck on red, where there was clearly a problem with the light where it wasn’t ever switching green, you’ve encountered a liveness problem with a system. A liveness property of a specification is an assertion that some good thing eventually happens. In the case … Continue reading A liveness example...