Distributed systems — Analyses — Jack Vanlightly

Distributed systems

Verifying Kafka transactions - Diary entry 3 - Getting confidence in the TLA+ spec

One thing I forgot to write about yesterday was how I get confidence that the TLA+ specification is doing what I expect. The thing about model checking a spec is that because there are usually millions or billions of states to explore, you can’t always see that certain states that should be reachable do get reached. It’s common to have a specification bug that causes your spec to have valid areas of the state space be unreachable, without you knowing it. This is why TLA+ practitioners learn to be a skeptical bunch and treat early success with great cynicism.

This is what I did to get confidence in this initial specification.

Share

Verifying Kafka transactions - Diary entry 2 - Writing an initial TLA+ spec

Strap in and fire up your nerd engines—this one's gonna be intense!

In my previous diary entry, I explained I would begin the formal modelling of Kafka transactions by implementing a tiny initial piece of the protocol - how a producer obtains a producer id. In this post I will discuss some aspects of the TLA+ specification I have written of this initial model.

Share