Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Modeling Redux with TLA+

hillelwayne.com

Post reply on HN
Print view View original

21–30 of 34 posts

Re: Modeling Redux with TLA+

#21

Post by elcapitan »

pron wrote: post #20
elcapitan wrote: post #10

Is it possible to compile algorithms from PlusCal to a traditional programming language? That way you could have a provable subcore of algorithms in your actual software project, and just autogenerate the code for the algorithms, instead of going manually from proven algorithm to hand-written implementation.

There is a PlusCal -> Go compiler[1] and, as I mentioned in a comment on a thread linked in another response to your question, there are tools to translate C and Java code to TLA+ for verification. But as a relatively experienced TLA+ user, I see almost no value in doing the first, and little practical value in the second. The kind of properties you want to reason about in TLA+ are so global and fundamental, that the…

Thanks for your extensive answer!

> The kind of properties you want to reason about in TLA+ are so global and fundamental, that the code you'd end up writing would both be too far removed from the high-level spec, and the process of translation would be negligible in the grand scheme of things, so that an automatic translation, if it is able to produce usable code at all, wouldn't really save you any time.

Hm - the examples in the Go compiler project look relatively good though - would it make sense to use something like this for small portions of a system? I understand that modelling and transpiling an entire system is close to impossible, but a more manageable use case may be a collection of business logic algorithms that are subject to frequent change. In that case you would still want to validate each version after a change, and it would save a lot of time to just autogenerate that particular algorithm in implementation code.

Re: Modeling Redux with TLA+

#22

Post by yoran »

raister wrote: post #9
fouc wrote: post #3

> TLA+ is a formal specification language. It’s a tool to design systems and algorithms, then programmatically verify that those systems don’t have critical bugs. It’s the software equivalent of a blueprint. Very cool.

Cool and impossible to apply to real world projects due to budget or deadlines.

There is an [interesting paper](http://lamport.azurewebsites.net/tla/formal-methods-amazon.p...) about how they use TLA+ at AWS to find bugs in their algorithms, and eventually prove correctness. So if you use AWS and rely upon its correctness, you have indirectly used a real-world application of TLA+. Someone else mentioned Facebook here, I think they also use formal methods.

Sure, formal methods are irrelevant for your standard CRUD application. However, the use case of AWS got me interested in applying TLA+ to this real-time collaboration feature that we have in the application that I develop. It involves multiple clients communicating over WebSockets, locking and unlocking resources, etc... Expressing the algorithm to TLA+ has:

1. vastly improved my understanding of what is going on and what the potential bad scenarios are. Simply taking a step away from the code, model the high-level algorithm and writing down the invariants that should always hold, makes a big difference.

2. identified real bugs that can occur (and probably have).

So yeah, you can't apply formal methods for everything. But I was pleasantly surprised by how easy it is to express a distributed algorithm in TLA+ and start proving statements about it. Somehow TLA+ manages to bridge the gap between engineering and more theoretical computer science.

Re: Modeling Redux with TLA+

#23

Post by pron »

elcapitan wrote: post #21
pron wrote: post #20

Earlier quoted context omitted.

There is a PlusCal -> Go compiler[1] and, as I mentioned in a comment on a thread linked in another response to your question, there are tools to translate C and Java code to TLA+ for verification. But as a relatively experienced TLA+ user, I see almost no value in doing the first, and little practical value in the second. The kind of properties you want to reason about in TLA+ are so global and fundamental, that the…

Thanks for your extensive answer! > The kind of properties you want to reason about in TLA+ are so global and fundamental, that the code you'd end up writing would both be too far removed from the high-level spec, and the process of translation would be negligible in the grand scheme of things, so that an automatic translation, if it is able to produce usable code at all, wouldn't really save you any time. Hm - the e…

Sure, it's possible to generate particular subroutines by compiling PlusCal to code, but the gains are far too small compared to the total gains of using TLA+. The kind of subroutines you'd want to model at the code-level in TLA+ would normally be very complex concurrent routines, using low-level operations that the PlusCal-to-source compiler would likely not know about (say, memory barriers), and in any case, you'd spend 98% of the time figuring out the algorithm in TLA+, anyway. Compilation would, therefore, save you 2% of your effort. As to the correctness of the generated code, we're talking very small routines here, that a careful manual translation is unlikely to get wrong.

In short, the likelihood that a PlusCal compiler would know to use your chosen libraries so that you wouldn't need to modify the code anyway is low, and even if it did, the savings in both correctness and effort would be slim.

A more interesting possibility would be compiling TLA+ properties into code-level specifications (such as Java's JML or C's ACSL), i.e., extracting various local properties from global ones, as that's actually "interesting" work.

In general, though, you must be careful when learning about new techniques reported in research papers. In formal methods (and in many other research areas) there's a HUUUUUGE gap between what has been achieved "in the lab" and what can be made into a practical and affordable tool for industry use. TLA+ is one of a handful of formal method tools that's been put to good use in industry.

Re: Modeling Redux with TLA+

#24

Post by elcapitan »

pron wrote: post #23
elcapitan wrote: post #21

Earlier quoted context omitted.

Thanks for your extensive answer! > The kind of properties you want to reason about in TLA+ are so global and fundamental, that the code you'd end up writing would both be too far removed from the high-level spec, and the process of translation would be negligible in the grand scheme of things, so that an automatic translation, if it is able to produce usable code at all, wouldn't really save you any time. Hm - the e…

Sure, it's possible to generate particular subroutines by compiling PlusCal to code, but the gains are far too small compared to the total gains of using TLA+. The kind of subroutines you'd want to model at the code-level in TLA+ would normally be very complex concurrent routines, using low-level operations that the PlusCal-to-source compiler would likely not know about (say, memory barriers), and in any case, you'd…

That makes total sense. Thanks!

Re: Modeling Redux with TLA+

#25

Post by moocowtruck »

RubenSandwich wrote: post #18
lou1306 wrote: post #15

Earlier quoted context omitted.

And about optimizing compilers, neural networks, and static program analysis four decades ago. Computer science is a fast-moving field, sure. But not all of today's research bring tangible results by the end of the week, and we should be comfortable with that.

I generally agree, but formal methods I can say with confidence will get adopted in the future. Here is why: Testing is fastly becoming adopted by everyone in our industry, why? Becuase you cannot afford to not write tests if your system is large/important enough. However our current testing methods cannot not prove the absence of bugs, as Dijkstra is fond of saying. So the best we can tell our clients currently on t…

formal methods don't magically make a specification bug-free/secure though, nor does it mean you won't making bugs in the formal verification code you're writing.. so what are you actually proving? other than just another layer of testing essentially? can anyone tell a client that a system has been 'proven' correct? I think when we use these words with people who don't completely understand the implications we need to be more precise what that means... that's what leslie lamport is all about ! being precise!

Re: Modeling Redux with TLA+

#26

Post by sseveran »

mettamage wrote: post #12
raister wrote: post #8

Earlier quoted context omitted.

I don't see the relevance on knowing Leslie Lamport to learn about TLA+ - what is the matter? One thing has nothing to do with the other... Would be valuable to learn that he dresses like a clown or like indiana jones in conferences and my preference on learning TLA?

"Would be valuable to learn that he dresses like a clown or like indiana jones in conferences and my preference on learning TLA?" Of course not. That question is too simple, and you know it! ;) Could you also ask a question that completely gives a counter example? Could you think of a question that does help learning TLA+ because you know something about Leslie Lamport? Have it as a fun exercise for 10 minutes, or no…

Plus his website has a bunch of good resources linked from it.

http://www.lamport.org

Re: Modeling Redux with TLA+

#27

Post by andrewflnr »

raister wrote: post #8
mettamage wrote: post #2

Sidenote: I remember that my teacher Maarten van Steen (who taught distributed systems at my university) talked about Leslie Lamport and I remember that he started TLA+. If you don't know about any of this, I invite you to take a look. Background info on Lamport [1]. Maarten van Steen offers his book for free on distributed systems. See [2]. 1. https://en.wikipedia.org/wiki/Leslie_Lamport 2. https://www.distributed-s…

I don't see the relevance on knowing Leslie Lamport to learn about TLA+ - what is the matter? One thing has nothing to do with the other... Would be valuable to learn that he dresses like a clown or like indiana jones in conferences and my preference on learning TLA?

Affect my decision to learn TLA? Probably not. Entertaining? Interesting? Something I would want to know? Yes.

Re: Modeling Redux with TLA+

#28

Post by hwayne »

mpiedrav wrote: post #6
ajmurmann wrote: post #5

Hillel gave a pretty interesting talk on TLA+ at last year's StrangeLoop: https://youtu.be/_9B__0S21y8 If you are new to TLA+ and just want to get the basic idea and use cases, I recommend the talk. Edit: I think he also brought home made granola or something. So attending his talks in person has benefits.

It was 7 lb (3.18 kg) of sesame brittle. Indeed, an entertaining and practical talk on TLA+.

_That said_, I've been making a lot of homemade granola recently. Maybe I should try bringing that next time!

Here's a recipe I really like: https://www.epicurious.com/expert-advice/how-to-make-granola...

Re: Modeling Redux with TLA+

#29

Post by nickpsecurity »

elcapitan wrote: post #10

Is it possible to compile algorithms from PlusCal to a traditional programming language? That way you could have a provable subcore of algorithms in your actual software project, and just autogenerate the code for the algorithms, instead of going manually from proven algorithm to hand-written implementation.

Although TLA+ can't, that is used extensively in some other tools like the B method, Circus for concurrency, Eshersoft's Perfect, and some provers (Isabelle/Coq). That's a good thing in my book for critical software given it knocks out errors people introduce in implementations. The only drawback is it creates simplistic code that might not be what you're wanting in performance, readability, or even security (eg side channels). Even with those drawbacks, it can become a reference implementation to equivalence check/test your hand-coded implementation against. In security, one might also mix verified/hardened implementations for untrusted input and optimized ones for trusted inputs if they come from separate, authenticated places.

Lots of tradeoffs one can make with spec-to-code generation. TLA+ just isn't in that game for most languages yet. Fortunately, it's straight-forward to convert TLA+ specs to code. Thinking about how to model or fix your algorithm is where the trouble will be. ;)

Post reply on HN