Bounded Buffers with TLA+ and Coyote
I’ve been exploring formal methods for the better part of the past year, ever since a graduate course on Automated Verification put the field onto my radar. I’ve had some interesting experiments with model checking using TLA+, but this is really only half the story of formal methods: verifying the design is correct. The other half is verifying that the implementation is correct.
For a while, I was checking simple C programs with CBMC which was pretty quick to get off the ground. Most recently, I’ve been exploring Coyote, which like TLA+ is from Microsoft Research. With some digging, a post on HackerNews caught my eye: “TLA+ and Coyote pair quite well actually. Verifying the high level design in TLA+ while checking subtle bugs as you translate that design to an implementation.”
Fortunately, Coyote comes with a nice number of samples, including the Bounded Buffer problem, which comes from the Extreme Programming wiki. The nice thing about canonical examples like this is that people tend to implement them in a variety of languages and frameworks. Fortunately, a few people have implemented the Bounded Buffer in TLA+ (and Pluscal, which compiles down to TLA+). For this article, we’ll focus on Hillel Wayne’s version since it comes with a nice description.
Just to be clear: none of the following is my original code. I’m interested in two things: understanding the Bounded Buffer problem, and understanding how TLA+ and Coyote can pair with each other.
Let’s start like we likely would if we were designing the Bounded Buffer from scratch: with the TLA+ spec. Even this is not quite starting from scratch, as the original Extreme Programming challenge provides an implementation in Java. I’m not going to summarize Hillel’s post (now would be a good time to read it if you haven’t yet), but I’d like to point out that Hillel is able to model a solution to the bug and verify that it works correctly. This is a great application of TLA+ — not just identifying a bug, but confirming that it can be resolved with a change to the design.
With Hillel’s TLA+ spec in hand, let’s turn to the Microsoft Research blog. First it’s worth installing Coyote. There’s a trivial example for the BoundedBuffer in the Research blog which is easy enough to code up and add to the sample. There are a few methods in the sample which can be run. It’s easy enough to encounter the bug by following the blog. You can also see the solution in the method TestBoundedBufferNoDeadlock — why is there no deadlock? Compared to the minimal deadlock implementation, there’s an additional boolean passed as a parameter to the BoundedBuffer constructor. This ultimately updates the class from notifying a thread to notifying all threads — which is exactly the same fix that Hillel found in TLA+.
The takeaway for me is that not only can TLA+ and Coyote find the same bug, but they can also verify the same fix. This is the sort of thing that I want in formal methods — a way to discover correct approaches and verify correct solutions. The poster on Hacker News seems to be right — TLA+ and Coyote pair quite well!
