TLA+ Formal Modeling and Programmers: Avoiding the Imperative “Brainwash”
I use the term brainwash as satire. Of course, the programmer imperative sensibility is quite important if you want to ship product, which is the bottom line.
But I've found the imperative mentality in my own work on TLA+ modeling initially confusing. I offer the following write-up to help clarify several important points (focusing on TLA+ Pluscal) in a technical note with example models, Python code. It's the first in a series on modeling a distributed key-value store I'm working on:
https://github.com/rodgarrison/tla_note1
Beyond basics I also give a recipe to use TLA+ at the command line for those of us who prefer it over IDEs. TLA's toolbox IDE is nice; still I prefer command line development when possible.
In the paper:
- program behavior versus model states
- deadlock
- termination
- coverage (label) checks
- setting up TLA+ on the command line
Hope it helps. As I note in the abstract I got some help of my own from the TLA Google Group. For the uninitiated - what is TLA? The PDF https://github.com/rodgarrison/tla_note1/blob/main/doc/tla.p... will do much better. TLA is an acronym for Temporal Logic of Actions originally written by L. Lamport of PAXOS fame. The PDF contains numerous links to videos, books, docs, because TLA is widely supported and used. TLA is like SPIN (http://spinroot.com/spin/whatispin.html) another well known model checker based on Promula not TLA syntax. And these tools fit into a larger universe of formal verification including, for example, COQ, Isabelle, Verdi, Dafny. The purpose of these tools (indeed they are all toolsets) is to: - allow one to precisely state what safety and liveness properties a system should have. Sometimes we don't even know what those conditions are until we sit down and try typing it up. - find counter examples to those safety, liveness conditions e.g. does my buffer overflow? did I deadlock? is one of my threads waiting forever? did my account balance ever go wrong? where? why? People like these tools esp. for concurrent and distributed work where the program paths, call sequences is highly exponential and highly combinatorial and where one wants some assurance all the threads really work and get to the right post conditions and system behaviors.