Earlier quoted context omitted.
Hah, I went to a few of his talks
Who are you guys talking about lol
Likely Marc Brooker, who has given some pretty great talks.
Reproducing the AWS Outage Race Condition with a Model Checker
21–30 of 52 posts
Re: Reproducing the AWS Outage Race Condition with a Model Checker
#22Earlier quoted context omitted.
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 w…
You can have liveness without a timeout. Think about it. Say you set a timeout of 1 minute in your application to transfer 500 mb over a 100mbps link. This normally takes 40s and this is that machines sole job, so it fails fast.
One day, an operator is updating some cabling and changes you over to a 10mbps link for a few hours. During this time, every single one of your transfers is going to fail even though if you were to inspect the socket, the socket is still making progress on the transfer.
This is why we put timeouts on the socket, not the application. The socket knows whether or not it is still alive but your application may not.
Re: Reproducing the AWS Outage Race Condition with a Model Checker
#23Earlier quoted context omitted.
Who are you guys talking about lol
Likely Marc Brooker, who has given some pretty great talks.
It wasn't him although he did give some good talks. It was another guy who headed up the formal verification group. The used it for finding bugs in caches and whatnot
Re: Reproducing the AWS Outage Race Condition with a Model Checker
#24Wish the author had an introduction to model checker article. I have yet to learn about this and will not be throwing some time into researching this topic.
I don't know if this counts as "research" but this research might be helpful https://www.learntla.com/
Re: Reproducing the AWS Outage Race Condition with a Model Checker
#25Earlier quoted context omitted.
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…
My hypothetical pitch deck tile slide: setTimeout() on a vector clock. I can hear Lamport’s scream from here and I live far away
Re: Reproducing the AWS Outage Race Condition with a Model Checker
#26I'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.
If it was, they would have mentioned it in their summary report, the way they justified other deliberate design decisions. I find it more likely they thought of 25 different ways this system could fail, fixed the ones that needed fixing (some of them hinted in the summary report), and then they forgot about that one way it was actually going to fail. Happens all the time.
I agree this article is very hindsight biased though. We do need a way to model the failure modes we can think of, but we also need a method that helps us think of what the failure modes are, in a systematic manner that doesn't suffer from "oops we forgot the one way it was actually going to fail".
Re: Reproducing the AWS Outage Race Condition with a Model Checker
#27Re: Reproducing the AWS Outage Race Condition with a Model Checker
#28Earlier quoted context omitted.
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.
If it was, they would have mentioned it in their summary report, the way they justified other deliberate design decisions. I find it more likely they thought of 25 different ways this system could fail, fixed the ones that needed fixing (some of them hinted in the summary report), and then they forgot about that one way it was actually going to fail. Happens all the time. I agree this article is very hindsight biased…
Yes, any analysis after an incident has the benefit, and bias, of hindsight.
But I see this post less as an incident analysis and more as an experiment in learning from hindsight. The goal, it seems, isn’t to replay what happened, but to show how formal methods let us model a complex system at a conceptual level, without access to every internal detail, and still reason about where races or inconsistencies could emerge.
Re: Reproducing the AWS Outage Race Condition with a Model Checker
#29I'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…
> but it's hardly axiomatic.
Agree, but Time-of-Check to Time-of-Use is a pretty well established failure mode.
Re: Reproducing the AWS Outage Race Condition with a Model Checker
#30Earlier quoted context omitted.
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…
How would you handle the case when some web service is making calls to a 3rd-party and that 3rd-party is failing in unexpected ways (i.e. under high load or IPs are not answering due to routing issues) to avoid a snowball effect on your service without using the timeout concept in any way?