MyDistributed.Systems

TLA+ and P are formal specification languages that let us formally define the behavior of our system and have a model checker reason about its correctness. In this post, I want to share some practical tips on using these awesome tools. I am not going to explain the basics and I assumes the reader is already familiar with these languages. If you are not, you can learn more about TLA+ at  Leslie Lamport's website . For P, a great place to start is the official website . I also wrote a blog post on P that explains P with examples. TLA+ vs. P While both TLA+ and P are formal specification languages, they are used for different purposes. Proving vs. Testing The main difference between TLA+ and P is that TLA+ is used to  prove , while P is used to  test ,   the correctness. While both use model checking, only TLA+ is used for exhaustive model-checking where we explore all possible executions of a given specification. Thus,  when the model checker does not find a bug, you are guaranteed

P is the name of a domain-specific language for asynchronous event-driven programming. With P, we can specify a system as a set of interacting state machines which talk to each other by sending events. That makes P a suitable language for modeling distributed systems where nodes talk to each other asynchronously via messages. P originally developed by Microsoft and according to its Github repository, it is currently being used extensively inside Amazon AWS for model-checking complex distributed systems. In this post, we want to see how we can use P to catch bugs in our protocols.