[HN Gopher] Reproducing the AWS Outage Race Condition with a Mod...
       ___________________________________________________________________
        
       Reproducing the AWS Outage Race Condition with a Model Checker
        
       Author : simplegeek
       Score  : 61 points
       Date   : 2025-11-02 18:37 UTC (4 hours ago)
        
 (HTM) web link (wyounas.github.io)
 (TXT) w3m dump (wyounas.github.io)
        
       | jldugger wrote:
       | Presumably that one guy at AWS who promotes TLA+ is furiously
       | modeling all this himself in more detail for internal analysis.
        
         | symbogra wrote:
         | Hah, I went to a few of his talks
        
         | cowsandmilk wrote:
         | It's more than one person at AWS now
        
       | tonetegeatinst wrote:
       | Wish 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.
        
         | throwaway81523 wrote:
         | I haven't used Alloy (alloytools.org) but it looks interesting
         | and there are good docs. Did you mean "now" instead of "not"?
        
       | grogers wrote:
       | 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 and the
       | tombstones are kept for 1 day. It would take something ridiculous
       | to make the thing that usually takes 1 minute take longer than a
       | day - not worth even considering. But sometimes there are a
       | confluence of events that make such a thing possible... For
       | example, maybe the top of rack switch died. The server stays
       | running, it just can't succeed any upstream calls. Maybe it is
       | continuously retrying while the network is down (or just slowly
       | timing out on individual requests and skipping to the next one to
       | try it). When the network comes back up, those calls start
       | succeeding but now it's so much staler than you ever even thought
       | was possible or planned for. That's just one scenario, probably
       | not exactly what happened to AWS.
        
         | withinboredom wrote:
         | 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 point is. You can't trust anything "will resolve in
         | time period X" or "if it takes longer than X, timeout". There
         | are so many cases where this is simply not true and should be
         | added to a "myths programmers believe" article if it isn't
         | already there.
        
       | philipwhiuk wrote:
       | I don't really understand the purpose of this. It's not like they
       | have anything other than the RCA (e.g. the code)
        
         | __float wrote:
         | A lot of people view model checking and similar tools as too
         | theoretical, academic Stuff that can't be so easily applied to
         | the real world.
         | 
         | Here we see the basic steps of modeling a complex system, and
         | how that can be useful for understanding behavior even without
         | knowing the details of every component.
        
       ___________________________________________________________________
       (page generated 2025-11-02 23:00 UTC)