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

Reproducing the AWS Outage Race Condition with a Model Checker

wyounas.github.io

Post reply on HN
Print view View original

31–40 of 52 posts

Re: Reproducing the AWS Outage Race Condition with a Model Checker

#31

Post by pjmlp »

jldugger wrote: post #2

Presumably that one guy at AWS who promotes TLA+ is furiously modeling all this himself in more detail for internal analysis.

Problem with TLA+ is that it is a completely unrelated tool to the actual programming, and even when everything is done correctly, it doesn't prevent further code changes breaking the model, unless there are work processes in place to update the related model, revalidate it, and only then push the changes into production.

As mentioned previously, I think the only tools that are really valuable should be able to produce code, naturally with multiple possible languages as backends, that are then used as library from the application code.

Something like Lean, F*, Dafny, even if that isn't exactly the same as TLA+.

Re: Reproducing the AWS Outage Race Condition with a Model Checker

#32

Post by zozbot234 »

pjmlp wrote: post #31
jldugger wrote: post #2

Presumably that one guy at AWS who promotes TLA+ is furiously modeling all this himself in more detail for internal analysis.

Problem with TLA+ is that it is a completely unrelated tool to the actual programming, and even when everything is done correctly, it doesn't prevent further code changes breaking the model, unless there are work processes in place to update the related model, revalidate it, and only then push the changes into production. As mentioned previously, I think the only tools that are really valuable should be able to produ…

The point of TLA+ is to act as a simple "toy model" for the actual system where you can still figure out relevant failure modes by automated means. Real-world code is a lot more complex so "end to end" proofs, while viable in a sense (static type checking is a kind of proof about the code) have very different and more modest goals than something like TLA+.

Re: Reproducing the AWS Outage Race Condition with a Model Checker

#33

Post by pjmlp »

zozbot234 wrote: post #32
pjmlp wrote: post #31

Earlier quoted context omitted.

Problem with TLA+ is that it is a completely unrelated tool to the actual programming, and even when everything is done correctly, it doesn't prevent further code changes breaking the model, unless there are work processes in place to update the related model, revalidate it, and only then push the changes into production. As mentioned previously, I think the only tools that are really valuable should be able to produ…

The point of TLA+ is to act as a simple "toy model" for the actual system where you can still figure out relevant failure modes by automated means. Real-world code is a lot more complex so "end to end" proofs, while viable in a sense (static type checking is a kind of proof about the code) have very different and more modest goals than something like TLA+.

Which on my eyes renders it into a useless academic exercise, regardless of how well renowned the people behind TLA+ happen to be.

Scenario proof modeling that is bound to human translation errors is as useful in practice, as doing PowerPoint driven software architecture.

Every step of the flow requires an expert on TLA+, the actual programming language and frameworks being used, to manually validate everything still means exactly the same across all layers.

Re: Reproducing the AWS Outage Race Condition with a Model Checker

#34

Post by harshaw »

If I were to summarize how we attacked this when I was on AWS (different team)

formal methods. Some of this started a long time ago so not sure if it was TLA, TLA+, or something else. (I am a useless manager type)

fake clients / servers to make testing possible

strict invariants

A simulator to fuzz/fault the entire system. We didn't get this until later in the life of the service but flushed out race condition bugs that would have taken years to do.

We never got to replaying customer traffic patterns which was a pet idea of mine but probably the juice wasn't worth the squeeze.

Re: Reproducing the AWS Outage Race Condition with a Model Checker

#35

Post by zozbot234 »

pjmlp wrote: post #33
zozbot234 wrote: post #32

Earlier quoted context omitted.

The point of TLA+ is to act as a simple "toy model" for the actual system where you can still figure out relevant failure modes by automated means. Real-world code is a lot more complex so "end to end" proofs, while viable in a sense (static type checking is a kind of proof about the code) have very different and more modest goals than something like TLA+.

Which on my eyes renders it into a useless academic exercise, regardless of how well renowned the people behind TLA+ happen to be. Scenario proof modeling that is bound to human translation errors is as useful in practice, as doing PowerPoint driven software architecture. Every step of the flow requires an expert on TLA+, the actual programming language and frameworks being used, to manually validate everything still…

There's plenty of real-world production use of TLA+, including by Amazon. The "toy model" approach may have limitations of a sort but it's far from purely academic - building simplified models of a complex system is routine practice.

The obvious difference with PowerPoint design is that non-trivial failure modes can be surfaced automatically if they're reflected in the toy model - PowerPoint slides don't do this.

You don't even have to use TLA itself for this purpose, a Lean development could also do this - but then you would have to put together much of the basic formalism (which ultimately works by combining the "modalities" of time, state and non-determinism) on your own.

Re: Reproducing the AWS Outage Race Condition with a Model Checker

#36

Post by pjmlp »

zozbot234 wrote: post #35
pjmlp wrote: post #33

Earlier quoted context omitted.

Which on my eyes renders it into a useless academic exercise, regardless of how well renowned the people behind TLA+ happen to be. Scenario proof modeling that is bound to human translation errors is as useful in practice, as doing PowerPoint driven software architecture. Every step of the flow requires an expert on TLA+, the actual programming language and frameworks being used, to manually validate everything still…

There's plenty of real-world production use of TLA+, including by Amazon. The "toy model" approach may have limitations of a sort but it's far from purely academic - building simplified models of a complex system is routine practice. The obvious difference with PowerPoint design is that non-trivial failure modes can be surfaced automatically if they're reflected in the toy model - PowerPoint slides don't do this. You…

We have all seen how well it gets surfaced automatically at AWS.

Re: Reproducing the AWS Outage Race Condition with a Model Checker

#37

Post by angry_octet »

deegles wrote: post #17
beanjuiceII wrote: post #14

Earlier quoted context omitted.

yea its an entire group of people that have yet to stop the next outage

I'd like to see hard data on the outage rate of systems with and without their input

Its the classic problem that code firefighters get all the attention, but they were also soaking the structure down with gasoline before hand.

Meanwhile the people who took the extra effort to tackle particularly painful parallel systems remove some race conditions early in the design process and are seen to achieve nothing.

Re: Reproducing the AWS Outage Race Condition with a Model Checker

#38

Post by zozbot234 »

pjmlp wrote: post #36
zozbot234 wrote: post #35

Earlier quoted context omitted.

There's plenty of real-world production use of TLA+, including by Amazon. The "toy model" approach may have limitations of a sort but it's far from purely academic - building simplified models of a complex system is routine practice. The obvious difference with PowerPoint design is that non-trivial failure modes can be surfaced automatically if they're reflected in the toy model - PowerPoint slides don't do this. You…

We have all seen how well it gets surfaced automatically at AWS.

There might be plenty of potential failures that we haven't all seen, simply because the problems were fixed after TLA+ modeling brought them up.

Re: Reproducing the AWS Outage Race Condition with a Model Checker

#39

Post by shayonj »

harshaw wrote: post #34

If I were to summarize how we attacked this when I was on AWS (different team) formal methods. Some of this started a long time ago so not sure if it was TLA, TLA+, or something else. (I am a useless manager type) fake clients / servers to make testing possible strict invariants A simulator to fuzz/fault the entire system. We didn't get this until later in the life of the service but flushed out race condition bugs t…

"juice wasn't worth the squeeze" - adding that to my vocab

Re: Reproducing the AWS Outage Race Condition with a Model Checker

#40

Post by pjmlp »

zozbot234 wrote: post #38
pjmlp wrote: post #36

Earlier quoted context omitted.

We have all seen how well it gets surfaced automatically at AWS.

There might be plenty of potential failures that we haven't all seen, simply because the problems were fixed after TLA+ modeling brought them up.

Or it might be that the model doesn't really avoid all possible human failures when translating TLA+ into Java, C++ metatemplate programming, or whatver.
Post reply on HN