After posting my last Kafka transactions diary entry, JP (the Fizzbee maintainer) wrote a refactored version using non-atomic actions and a different way of representing the network. It’s a very interesting variant and I’m tempted to switch over to his version.

When an action is not atomic, execution of an action could yield at any moment to a different action in a different role instance or even the same role instance. With this yielding we can also replace explicit message passing with direct invocation of a function on another node. The invocation and the response can all yield to other concurrent events happening across the system.

Let me use a simple example to demonstrate - Ping-Pong.

Symmetry reduction in TLA+ is a clever trick for cutting down the size of the state space we need to explore during model checking. Think about a distributed system with interchangeable components—servers, nodes, or processes that behave identically. Without symmetry reduction, the model checker wastes time exploring states that are essentially duplicates, differing only in the labels we’ve assigned to these components. Symmetry reduction says, “Hey, if swapping the identities of these components doesn’t change the behavior of the system, let’s treat those states as one.” This massively reduces the computational effort while keeping the results valid.

In this post, I’ll show some simple examples of symmetry using trivial specs where we can actually visualize the state space. The idea is to build a mental model of how symmetry reduction works.