Managing Accounts in Coyote and Pluscal
Building off the previous examples of the Bounded Buffer in TLA+ and Coyote, this time I did a little reverse engineering. If there’s an example in Coyote, we should be able to model it in TLA+… right?
My path to learning TLA+ started with Pluscal, and mostly the work of Hillel Wayne, who’s book Practical TLA+ is on my desk as I write. Hillel was also nice enough to help out with this example, so be sure to sign up for his newsletter.
The difference between Pluscal and TLA+ is probably more technical than this, but my informal understanding is that TLA+ is a math language for state machines, while Pluscal is a language for distributed and concurrent algorithms that gets translated to TLA+. After learning Pluscal, I spent some time learning TLA+, and after a few months in the mathematical wilderness, I’m ready to come back to Pluscal again. Since Coyote is for concurrent systems, it makes sense to write models for Coyote in Pluscal.
Here’s the basic example in the Account Manager sample for Coyote: We want to create an account, but we have an asynchronous controller (which could be behind a REST API, for example). We also have an asynchronous database. The problem is that, due to concurrency, we might create the same account twice. The video from Pantazis Deligiannis does a great job introducing the sample and working through it.
The question driving this post is, can we model this problem in Pluscal? If so, what might the differences be?
First of all, it’s fairly straightforward to model the bug in Pluscal. I got the bug easily enough, but struggled with the invariant, so I messaged Hillel. He was nice enough to help me — instead of creating an invariant, I needed to add an assert. I’m still learning Pluscal/TLA+ so this was very helpful. With a little spit and polish, I was able to create the buggy version in Pluscal.
Now, how to fix the bug? We don’t want to make the same account twice. In the Coyote video, we avoid this by adding a try/catch. In some ways, this makes a lot of sense. But in other ways, it doesn’t make sense in TLA+. TLA+ doesn’t have a try/catch (that I’m aware of — what does an exception mean?). Instead, I went with the solution from Hillel’s book for the Bank Server — don’t use two states to model a transaction when one will do. My solution worked! This is basically abstracting out the concurrent database, but at the same time… TLA+/Pluscal has to abstract something. It’s operating at a higher level. It’s not going to be as specific as Coyote. If we really wanted to get granular, we could probably abstract a concurrent database, but honestly… who has the time?
There are a lot of things that I am liking about formal methods. The ability to prove correctness is high on the list. The confidence that it provides in different versions of the same problem is also helpful. But the rabbit hole I need to avoid is overworking the problem. If I can abstract a bug free solution in one model, and then I figure out how to implement it in another (say, with a try/catch for a concurrent database, instead of forcing something sequential), I might not need to model the how — just the what. I can just say that it’s an implementation concern and leave it to the implementation.
Am I right? I don’t know. I hope to get some more feedback on both the implementations and the models. But my plan is to work through a few of these tutorials and exercises for a couple different programs like Pluscal, P, Dafny and Coyote. Frankly, who has the time to model ever single detail of every single component? The entire point is that there’s a higher level of abstraction that can give you some level of confidence. So for tonight, here’s my confidence — both the model and the implementation can create the bug, and both the model and implementation can be bug free. Case closed. There are plenty more bugs to stomp.
