PRACTICAL TLA+: PLANNING DRIVEN DEVELOPMENT

by Hillel Wayne

Learn how to design complex, correct programs and fix problems before writing a single line of code. This book is a practical, comprehensive resource on TLA+ programming with rich, complex examples. Practical TLA+ shows you how to use TLA+ to specify a complex system and test the design itself for bugs. You’ll learn how even a short TLA+ spec can find critical bugs. Start by getting your feet wet with an example of TLA+ used in a bank transfer system, to see how it helps you design, test, and build a better application. Then, get some fundamentals of TLA+ operators, logic, functions, PlusCal, models, and concurrency. Along the way you will discover how to organize your blueprints and how to specify distributed systems and eventual consistency. Finally, you’ll put what you learn into practice with some working case study applications, applying TLA+ to a wide variety of practical from algorithm performance and data structures to business code and MapReduce. After reading and using this book, you'll have what you need to get started with TLA+ and how to use it in your mission-critical applications. What You'll LearnWho This Book Is ForThose with programming experience who are new to design and to TLA+.

Genres: Programming, Technology, Software, Computer Science, Technical

248 pages, Paperback

Reviews

[Rafael · Rating 5 out of 5]

As far as I know, this is the first book covering in depth the algorithm language PlusCal (formerly called +CAL). PlusCal is meant to replace pseudo-code for writing high-level descriptions of algorithms. An algorithm written in PlusCal is translated into a TLA+ specification that can be checked with the TLC model checker.

Frederick P. Brooks already reflected on formal methods in his very well known essay "No Silver Bullet: Essence and Accident in Software Engineering":

"Much of the effort in modern programming goes into the testing and repair of bugs. Is there perhaps a silver bullet to be found by eliminating the errors at the source, in the system design phase? Can both productivity and product reliability be radically enhance by following the profoundly different strategy of proving designs correct before the immense effort is poured into implementing and testing them?"

If you want to embrace this strategy to prove and better understand your designs before writing code, then PlusCal could be a great tool to add to your designer's tool belt.

Hillel Wayne has authored an invaluable book for anyone interested in deep dive into fomal methods through Dr. Lamport's TLA+ and, specifically, the PlusCal language. That is not a surprise coming from someone who made available the excellent and free LearnTLA.com tutorial.

The first part (first 6 chapters) of the book describes the syntax and semantics of PlusCal, and the second part (last 5 chapters) shows, through detailed examples, how you can apply the language to different contexts like algorithms, data structures, business logic or MapReduce.

I think the second part is the most valuable contribution, because the author not only shows examples in its final and functional form, but the incremental development process and the dead ends you can run into. This way the book answers the critical gap you will face once you understand the language, that is, how on earth I can put this new knowledge into practice in my daily development tasks?

[Bugzmanov · Rating 4 out of 5]

I'm a big fan of Hillel's blog and his presentations and I had high expectations for this book. And it's a good book, it lays out pluscal syntax foundations and does a good job of showing that the modeling technique is applicable in multiple vastly different scenarios: validating invariants of data structures, checking temporal properties for concurrent code, looking for gaps in business requirements, etc.

However, I was expecting some kind of revelation, like the one you get from learning about property-based testing. The whole new world, so to say.
I didn't get that from this book. Overall it left me with the impression "it's very hard to make it useful for real use cases". For instance, the whole chapter about using the technique for checking data structures - is actually validating the simplest data structure out there - linked list.
And the model the book ends up with is neither simple nor short. I can't imagine how much harder it would be to validate things like concurrent skip list.
The chapter on map-reduce is more about validating simple business logic implemented in MR framework and skips most of the meaty details of failure-handling and self-healing. I would be more delighted if it provided some kind of validation of the framework itself.

Overall, it's a great introduction to the topic, but it feels like I'll need to read something else before I would be able to apply the technique to anything real.

UPD 2022: After re-reading this book, I still think this is pretty good intro to pluscal. And to get most out of it I recommend you not just follow along with the author, but try to implement models by yourself and then compare with the proposed solution. Watching Lamport lectures on TLA+ in parallel helps a lot, as this book is not that great at presenting TLA+ side of things. And it's essential to understand TLA+ for debugging purposes.
My main problem with tla+ & pluscal that most of the issues are not googleable. TLA+ questions are almost absent on stack overflow. Treating this book a a collection of exercises helps you to build good grasp on the syntax.
This book alone is not enough to become proficient in modeling with tla+ & pluscal. But it is a good start.

[Lojicholia · Rating 3 out of 5]

We read this as a reading group at work; it was the starting point for our “learn modeling” group. I think as a whole it’s an ok introduction to TLA+: it provides a comprehensive review of the system and its nuances. Having said that, I do wish the book presented fundamental concepts upfront, and then focused on practical examples. For example, refinements are introduced in chapter 9, but mentioned earlier in the book. Additionally, I wish there was more focus on the “practical” side: examining actual algorithms and systems. Chapters 9 and 10 were the closest to what I would be doing at work, and they felt lacking. As a contrast, the tamarin manual proves a simple cryptographic system in chapter 3.

All told, not a terrible book for learning TLA+, but the group consensus was that it could be better organized and slightly more practical.

[John · Rating 5 out of 5]

I found this book to be an excellent guide to the world of "using a tool to help you think good about software design." A few points:
- it's not just for doing fancy distributed systems, you can also use it to help reason about complex product requirements
- since it's a tool for reasoning about systems in general, you don't even need to limit yourself to software!
- the first half is a little bit dry so I quit after that. Don't do this, I went back to it and the second half is so worth it - lots of insights and practical advice and wonderfully written examples.

Also it's quite short. So: if you want another way to think about the behavior of systems pick this book up and read the whole dang thing.

[Xavier Shay · Rating 5 out of 5]

Does what it says on the tin. I didn't know anything about TLA+ beforehand, save the name and that enabled formal verification maybe? Didn't see how it could be useful to my day to day. Now I do! Particularly liked the final two chapters, walking through designing a library system and map reduce, including dead ends. Already see places where I want to start using these techniques.

[Nate Smith · Rating 5 out of 5]

This is a fantastic tour of TLA+. The examples are all very practical and easy to follow. It was worth taking the time to work through them all, I feel like I have a decent handle on writing my own models. The algorithms chapter was a bit of a slog, followed by three chapters of excellent examples that were easy to map to real-world systems.

[James · Rating 4 out of 5]

Good overview of how to use TLA plus. I don't personally like TLA Plus; while the ideas are fascinating, I think the language is inelegant and crufty. But this book does a good job cutting through that and teaching you what you need to know.

[Taras Boiko · Rating 4 out of 5]

It helped a lot to watch Lamport videos before reading. Some things where clearer instead of "it is so because it is so."

[Alex · Rating 3 out of 5]

Great way to jump right into PlusCal. Make sure you do the TLA+ video course first.

[Stephen Adams · Rating 4 out of 5]

A really good introduction to TLA+ and PlusCal. The author is able to set out the basics of using the toolbox and modelling systems clearly and succinctly.

I wish the author had expanded more on when he felt it was necessary to use TLA vs PlusCal. A second edition of the book could also benefit from some concrete examples of TLA+'s use in industry.

Overall though it is a very good introduction to TLA+ and the mindset that you must approach formal software specification.

[Eduardo · Rating 5 out of 5]

This is a very gentle introduction to the formalism of Leslie Lamport's TLA+ specification language. It serves as a nice first step before Specifying Systems. I also enjoyed the focus on PlusCal, which looks a lot less alien to most software engineers.