Published on 2024-02-02 | Last update: 2024-02-07 | 12 min read What problem are they trying to solve? What's the "happened-before" relation? What's a logical clock then? How can we get a total ordering? How can we solve the mutual exclusion problem using Lamport clocks? The TLA+ specification Conclusion References Last weekend I wanted to get some inspiration to write some TLA+ spec and I got my hands back on the paper Time, Clocks, and the Ordering of Events in a Distributed System by Leslie L...