What TLA+ Can't Check
Hi everyone,
I wrote a new blog post, Breaking the Limits of TLA+ Model Checking. It's the first (non-learntla) TLA+-related content I've put out in what, almost two years? It also comes with a GitHub project with all the software artifacts: the spec, the graphing software, the scripts, etc. It's about how to test the things that TLA+ can't natively check, like hyperproperties and probabilistic properties.
So what do I mean by "things that TLA+ can't check?" I spent ten minutes writing and rewriting two paragraphs carefully defining the differences between the language and the model checker before giving up and saying "this is a newsletter, nobody wants to read this." So here's the oversimplification. In TLA+ we have a spec that has multiple behaviors, or traces. Properties in TLA+ are things that are true for every behavior. Some such properties:
- "Two threads can't both be in the critical section": True if in every behavior, there isn't state where more than one thread is in the cs.
- "The light cannot go straight from green to red": True if in every behavior, there isn't state where the light is green followed by a state where the light is red.
- "The algorithm eventually gets the right answer": True if in every behavior, there is a state where the answer is correct.
(I have a more formal treatment about these kinds of properties here.)
So in every case of an expressible property, we can express it in terms of every behavior sharing a property. This is based on what you can write in the TLA+ formalism. []P for "P is always true", <>P for "P is eventually true".
Notice something missing from those? How about "It's possible for this value to be 3?" It's true if at least one behavior has a state where the value is 3. This is a reachability property, and TLA+ can't naturally check it!
By "naturally" I mean there's no way to use TLA+ notation to write a reachability property. But if we're sufficiently clever, we can mimic it in the model checker. To test "S is reachable":
- Express the property "state S never happens"
- Make that an invariant of the system
- Run the model checker.
- If S is reachable, the model checking will fail, and give you an error trace.
This is such a well-known idiom that Leslie Lamport himself used it in his TLA+ video course!
However, you can't extend this to say "S and P are both reachable." If you write "S never happens and P never happens", as soon as the model checker finds S it'll stop. You'll never "check" that P is reachable! Instead you have to make two separate invariants and check them in separate runs. And don't get me started on "S is reachable from every possible starting state", good fucking luck mimicking that. This is the problem with mimicry: you're working against the language to shoehorn stuff in.
I don't see this as a problem with TLA+. It's a standard capability/tractability tradeoff: the more properties you can natively express, the harder it is to model check them all. I find it more interesting to see what the limits are. And also I like categorizing types of properties, because I just love taxonomies in principle.
Other impossible properties
The blog post covers two other inexpressible properties: hyperproperties and probabilistic properties.
Hyperproperties are defined over sets of behaviors, instead of individual behaviors. Consider a numerical method with a lot of optimization parameters. A hyperproperty would be something like "changing parameter X by 10 changes the accuracy of the answer by at most 1%." Hyperproperties are really hard to model and check, but thankfully aren't commonly things we're interested in... for now. I talk a bit more about them here.
Probabilistic properties are a little more common: properties which need to hold for some percentage of behaviors. When someone says they their 95th percentile response time is 100ms, they're saying that in 95 out of 100 program behaviors, the response time is no more than 100ms. This is outside of TLA+'s scope because it doesn't hold for all behaviors, but it's still a thing we're often interested in. More on probabilistic properties here.
There are other, even more exotic inexpressible properties, your imagination is the only limit here. There's also some properties that seem in TLA+'s wheelhouse but can't be done due to other tradeoffs in the formalism. There's no way to say "X happens within five steps of Y" without adding an auxiliary variable, and that has its own mimicry problems.
How we break this
So if there's limits to what TLA+ can express, and mimicry only gets us so far, what can we do to test the really weird stuff?
Easy. Step outside of TLA+.
This might mean "using a different formal language", but it can also mean using other classes of tools entirely. In the article's case, I generate the whole state space, serialize it to disk, and import it into graph analysis software. From that point, verifying properties reduces to writing the right graph algorithm. It doesn't necessarily make verification easy, but it does make it possible. I hit a few dead ends getting it set up, which is why I wrote up the whole project and then provided all of the files, with notes. Go check it out!
(Oh man I just realized: this it might even make the Forbidden Operator verifiable! That's an exciting one, and would 100% count as doing a Language Crime.)
This isn't the only cool thing I've been doing with TLA+ recently. I'm doing a consulting gig and as part of it have developed a lot of really exciting new techniques. The one I'm most excited about? I think I might have found a principled way to do spec composition. I'll write it up once it's fully battle-tested. If you're interested in top-level TLA+ work, I'm available for specification and training =)
If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.
My new book, Logic for Programmers, is now in early access! Get it here.