An Introduction to Model Checking with TLA+
This month, I’m challenging myself to complete an online university lecture series in Introduction to Model Checking. The course is taught by Joost-Pieter Katoen, one of the authors of Principles of Model Checking. Katoen notes that the course is focused on theory more than application. However, since I have a little experience in the field, I’m using the course and exercises as an excuse to practice using TLA+ and it’s related tools, the algorithm language Pluscal and the TLC Model Checker. While watching the first four lectures, and reading the first two chapters of the textbook, I’ve been able to write some simple specs, but also find three of the same examples in other TLA+ learning resources. Some links, thoughts and reflections below.
The first lecture includes an example bug in NASA’s Deep Space-1 spacecraft. There are three processes — one that increments a variable, one that decrements that variable if it is greater than zero, and one that resets that variable at a value limit. The question is if the variable can have an unexpected value, like -1 (which isn’t between zero and the value limit). The answer, unfortunately for NASA, is yes. There’s a trace where the value can be reset and then the value can be decremented, leading to a value of -1. What was interesting about modeling this in TLA+ is that I usually model a multi-process system with multiple instances of the same process. Doing so here resulted in a simple example where the value could be incremented once and decremented twice. But this isn’t the actual problem, and is a good reminder that a model needs to be an appropriate representation of the software.
What I learned is that I can use TLA+ to model separate processes by giving each process a separate value. So one process gets the value 1, another gets the value 2 and the third value 3. In this way, each process is able to do only its relevant function. The TLC Model Checker found a trace where the value reaches 200, it gets reset to 0, and then is decremented. We found the bug!
A section in Chapter 2 focuses on the Alternating Bit Protocol. This is featured in the TLA+ Video Lecture series, hosted by TLA+ creator Leslie Lamport. While the previous and following examples use Pluscal, the video lecture series focuses on TLA+ itself. The two videos on the Alternating Bit Protocol features two separate specifications: a simple one without a lossy channel, and one using lossy channels in the form of sequences. I hadn’t watched this far in the lecture series before (I had only watched up to about five or so), but this section provides a good introduction to the concept of fairness. While fairness doesn’t appear in the textbook until Chapter 3, it’s something I’ve had issues with in TLA+ before. While I didn’t fully understand it after one viewing of this section, I hope watching it again after reading in the textbook may clear things up. I’d also like to try and implement the Alternating Bit Protocol in Pluscal, since the video lecture series doesn’t use that. I might leave that for another day.
Almost all of the other examples from Chapter 2 and the first exercise set are mutual exclusion algorithms. I count four specific algorithms: Peterson’s algorithm is given in the textbook, the Fast algorithm is given in the 2018 exercises, Pnueli’s algorithm and Djikstra’s both appear in the Chapter 2 exercises. They all can be modeled in Pluscal relatively similarly.
Fortunately, there are pre-existing resources for Peterson’s algorithm and the Fast algorithm. The Peterson algorithm is used in a TLAPS Tutorial, which was my first exposure to the TLA+ Proof System (now called the Proof Manager, I think). I have really only used TLA+ for model checking and proof theorems are like model checking on steroids. There are not a lot of resources for TLAPS/TLAPM it seems, as this question recently came up on the TLA+ Google Group. I’d like to learn about Coq, which is a popular theorem prover used in the Software Foundations series. Maybe when I get to Coq I’ll also try some theorem proving in TLA+.
The Fast algorithm is given in the Pluscal C Manual (p. 12-13), which I was looking at since I learned Pluscal using the Pascal style (favored by learning material created by Hillel Wayne, like learntla.com). I was actually just trying to remind myself about some syntax when I stumbled across the example and realized that the algorithm is basically the same as the one given in Exercise 3 from the 1st problem set of 2018. There are some slight differences between the two, but it’s basically the same.
The fact that these six or so examples can be modeled in TLA+ should not be surprising. This is an introductory course and these are common examples. TLA+ is a powerful, flexible tool for writing specifications and checking models. I probably won’t need to write a mutual exclusion algorithm anytime soon, but tracking the possible interleaving of multiple process executions is a valuable skill to practice. Same thing with writing multi-process programs in TLA+. And I actually learned something about how to use Pluscal from even the very simple Deep Space-1 example.
What’s really nice about this? I don’t have access to a lot of solutions material for the exercises. This is actually an important part of the process — otherwise, I won’t get feedback and can’t improve. One way that I can check my answers is by first using pen and paper and then writing the specification in TLA+ and check it. The models can confirm if my answer is correct. This has been helpful with a few questions so far, and I’m curious if it’ll be more helpful as I progress into more complex material.
I’d like to think that all this extra work in TLA+ helped reinforce what I’m learning in Principles of Model Checking. I like being able to replicate the theoretical examples in applications and I’m particularly pleased with the variety of learning material involved: a conference tutorial, guided lecture series and the language reference manual. I was going to post the specs for the others on Github, but I’ll leave them as exercises to the reader. They certainly were good exercises for me!
