Live data from Hacker News

Reproducing the AWS Outage Race Condition with a Model Checker

wyounas.github.io

11–20 of 52 posts

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

#11
post #4

Real world systems often have to deviate from the "pure" version used to run formal methods on. This could be how long you keep transaction logs for, or how long rows are tombstoned for, etc. The longer the time period, the costlier it usually is, in total storage cost and sometimes performance too. So you have to compromise with where you set the time period for. Let's imagine that the process usually takes 1 minute…

In my mind, anything that has an actual time period is bound to fail, eventually. Then again, I hang around QA engineers a lot, and when you hear about the selenium troubles of "wait until an element is on the page" stories, you realise it relates to software in general. QA people deal with problems and edge cases most devs will never deal with. They’re your subject-matter-experts of 'what can go wrong'. Anyway, the…

>You can't trust anything "will resolve in time period X"

As is, this statement just means you can't trust anything. You still need to choose a time period at some point.

My (pedantic) argument is that timestamps/dates/counters have a range based on the number of bits storage they consume and the tick resolution. These can be exceeded, and it's not reasonable for every piece of software in the chain to invent a new way to store time, or counters, etc.

I've seen a fair share of issues resulting from processes with uptime of over 1 year and some with uptime of 5 years. Of course the wisdom there is just "don't do that, you should restart for maintenance at some point anyway" which is true, but it still means we are living with a system that theoretically will break after a certain period of time, and we are sidestepping that by restarting the process for other purposes.

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

#12
post #4

Real world systems often have to deviate from the "pure" version used to run formal methods on. This could be how long you keep transaction logs for, or how long rows are tombstoned for, etc. The longer the time period, the costlier it usually is, in total storage cost and sometimes performance too. So you have to compromise with where you set the time period for. Let's imagine that the process usually takes 1 minute…

In my mind, anything that has an actual time period is bound to fail, eventually. Then again, I hang around QA engineers a lot, and when you hear about the selenium troubles of "wait until an element is on the page" stories, you realise it relates to software in general. QA people deal with problems and edge cases most devs will never deal with. They’re your subject-matter-experts of 'what can go wrong'. Anyway, the…

Yeah... it has felt kind of ridiculous over the years how many times I have tracked some but I was experiencing down to a timeout someone added in the code for a project I was working with, and I have come to the conclusion over the years that the fix is always to remove the timeout: the existence of a timeout is, inherently, a bug, not a feature, and if your design fundamentally relies on a timeout to function, then the design is also inherently flawed.

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

#13
I'm a fan of more formal methods in progam analysis, but this particular excercise is very hindsight-is-20/20

> In this case, we can set up an invariant stating that the DNS should never be deleted once a newer plan has been applied

If that invariant had been expressed in the original code — as I'm sure it now is — it wouldn't have broken in the first place. The invariant is obvious in hindsight, but it's hardly axiomatic.

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

#14
post #2

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

It’s more than one person at AWS now

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

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

#15
post #13

I'm a fan of more formal methods in progam analysis, but this particular excercise is very hindsight-is-20/20 > In this case, we can set up an invariant stating that the DNS should never be deleted once a newer plan has been applied If that invariant had been expressed in the original code — as I'm sure it now is — it wouldn't have broken in the first place. The invariant is obvious in hindsight, but it's hardly axio…

not deleting the active plan seems like a basic fail-safe design choice, and this isn't AWS people's first rodeo. likely there was some rationale for not going with a built-in fallback.

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

#17

Earlier quoted context omitted.

It’s more than one person at AWS now

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

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

#19
post #15
post #13

I'm a fan of more formal methods in progam analysis, but this particular excercise is very hindsight-is-20/20 > In this case, we can set up an invariant stating that the DNS should never be deleted once a newer plan has been applied If that invariant had been expressed in the original code — as I'm sure it now is — it wouldn't have broken in the first place. The invariant is obvious in hindsight, but it's hardly axio…

not deleting the active plan seems like a basic fail-safe design choice, and this isn't AWS people's first rodeo. likely there was some rationale for not going with a built-in fallback.

[deleted]

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

#20
post #13

I'm a fan of more formal methods in progam analysis, but this particular excercise is very hindsight-is-20/20 > In this case, we can set up an invariant stating that the DNS should never be deleted once a newer plan has been applied If that invariant had been expressed in the original code — as I'm sure it now is — it wouldn't have broken in the first place. The invariant is obvious in hindsight, but it's hardly axio…

Every such analysis will have some hindsight bias. Still, it’s a great post that shows how to model such behavior. And I agree with the another reply that not deleting an active plan seems like a basic fail safe choice which the post also covered
Post reply on HN