Live data from Hacker News

Systems Correctness Practices at Amazon Web Services

cacm.acm.org

51–60 of 143 posts

Re: Systems Correctness Practices at Amazon Web Services

#51

>Deterministic simulation. Another lightweight method widely used at AWS is deterministic simulation testing, in which a distributed system is executed on a single-threaded simulator with control over all sources of randomness, such as thread scheduling, timing, and message delivery order. Tests are then written for particular failure or success scenarios, such as the failure of a participant at a particular stage in…

DST was i̶n̶v̶e̶n̶t̶e̶d̶ popularized at FoundationDB a little over a decade ago, and has been quietly gathering steam ever since. If you’re interested in the technique, the FDB paper has some good info in section 4 and section 6.2: https://www.foundationdb.org/files/fdb-paper.pdf

(Disclosure: I am an author.)

I also gave a talk overview of it at Strange Loop back in 2015, but don’t have the youtube link handy.

If you’re interested in trying DST, we have a new company that aims to make it a much easier lift, especially for existing projects that can’t be retrofitted onto one of the many simulation frameworks: https://antithesis.com

Happy to answer any questions about the approach, here or over email.

Re: Systems Correctness Practices at Amazon Web Services

#52
post #51

>Deterministic simulation. Another lightweight method widely used at AWS is deterministic simulation testing, in which a distributed system is executed on a single-threaded simulator with control over all sources of randomness, such as thread scheduling, timing, and message delivery order. Tests are then written for particular failure or success scenarios, such as the failure of a participant at a particular stage in…

DST was i̶n̶v̶e̶n̶t̶e̶d̶ popularized at FoundationDB a little over a decade ago, and has been quietly gathering steam ever since. If you’re interested in the technique, the FDB paper has some good info in section 4 and section 6.2: https://www.foundationdb.org/files/fdb-paper.pdf (Disclosure: I am an author.) I also gave a talk overview of it at Strange Loop back in 2015, but don’t have the youtube link handy. If you…

I think this is the link? https://www.youtube.com/watch?v=4fFDFbi3toc

Re: Systems Correctness Practices at Amazon Web Services

#53
post #6
post #3

Earlier quoted context omitted.

And just a tip for who may be intersted: Claude Opus with Extended Thinking seems to be very good at converting existing code into TLA+ specs. I've found multiple bugs for personal Rust projects like this (A Snake game that allowed a snake to do a 180 degree turn), and have verified some small core C++ components at work with it as well (a queue that has certain properties around locking and liveness). I tried other…

I’ve always envisioned tla and other formal methods as specific to distributed systems and never needed to understand it. How is it used for a snake game? Also how is the TLA+ spec determined from the code? Won’t it implicitly model incorrect bugs as correct behaviour since it’s an existing state in the system? Also when using TLA from the start, can it be applied to implementations? Or is it only for catching bugs d…

I'm not an expert but my current understanding is that code execution is always a state transition to the next state. So what you do is fully specify each state and the relation between them. How the transition actually happens is your code and it's not that important. What's important is that the relations does not conflict to each other. It's a supercharged type system.

> Also how is TLA+ spec determined from the code?

You start from the initial state, which is always known (or is fixed). Then you model the invariants for each lines.

> Won’t it implicitly model incorrect bugs as correct behaviour since it’s an existing state in the system

Invariants will conflicts with each other in this case.

> Also when using TLA from the start, can it be applied to implementations?

Yes, by fully following the specs and handling possible incorrect states that may happens in practice. If your initial state in the TLA+ specs says that it only includes natural numbers between 1 and 5, you add assertions in your implementation (or throw exceptions) that check that as the Int type in many type systems is not a full guarantee for that constraint. Even more work when using a dynamic language.

Re: Systems Correctness Practices at Amazon Web Services

#54

>Deterministic simulation. Another lightweight method widely used at AWS is deterministic simulation testing, in which a distributed system is executed on a single-threaded simulator with control over all sources of randomness, such as thread scheduling, timing, and message delivery order. Tests are then written for particular failure or success scenarios, such as the failure of a participant at a particular stage in…

I want something like this, but I work almost entirely in Go. Am I correct in thinking that this would require a fork of the main Go implementation, in order to make a deterministic (and controllable) goroutine scheduler and network stack? Does one also need to run on a particularly predictable OS?

"Am I correct in thinking that this would require a fork of the main Go implementation, in order to make a deterministic (and controllable) goroutine scheduler and network stack?"

Yes, because the Go runtime actually explicitly and deliberately leans in the opposite direction. Additional non-determinism is deliberately added to the system, most notably that a "select" call with multiple valid channels will be psuedorandomly chosen, and iteration on a map is somewhat scrambled on each iteration. It's not entirely random and as such not suitable for pretty much any randomness requirement you may have, but enough to generally prevent accidental dependencies on deterministic iteration.

This has the effect of "spreading out" concurrency issues and hopefully reducing the sort of issues you get when you only discover a major issue when something else in the environment changes three years later. It's a nice default but nothing like a proof, of course.

You can also go the "predictable OS" route, since the entire Go runtime sits on top of it. Nothing can non-deterministically run on top of a fully deterministic OS image. But a fully deterministic OS would probably want some integration with the Go runtime to be able to more deeply control it through mechanisms other than varying inputs to the random function, which is a very indirect way to go down a code path.

Re: Systems Correctness Practices at Amazon Web Services

#55
post #8

> 92% of catastrophic failures in tested distributed systems were triggered by incorrect handling of nonfatal errors This. If you take nothing else away from the article (which has a lot) take this: fail well, don’t fail poorly.

It would also be nice to list some "best practices" on how to handle non-fatal errors. I would be definitely interested to know of any sources.

One of the nice things about "errors as values" is that it is generally easier to shim in an error rather than shim in an exception. Not that it's impossible to do the latter, but it's just generally easier because you can have that error serving as a value in your test code.

I have a lot of Go testing shims that look like:

    type UserGetter interface {
        GetUser(userID string) (User, error)
    }

    type TestUsers struct {
        Users map[string]User
        Error error
    }

    func (t TestUsers) GetUser(userID string) (User, error) {
        if t.Error != nil {
            return User{}, t.Error
        }
        user, have := t.Users[userID]
        if !have {
            return User{}, ErrUserNotFound
        }
        return user, nil
    }
This allows easily testing errors upon retrieving users and ensuring the correct thing happens. I'm not a 100% maniacal "get 100% test coverage in everything" kind of guy, but on the flip side, if your test coverage only lights up the "happy path", your testing is not good enough and as you scale up the probability that your system is going to do something very wrong when an error occurs very rapidly approaches 1.

It's more complicated when you have something like a byte stream where you want to simulate a failure at arbitrary points in the stream, but similar techniques can get you as close as you like, depending on how close that is.

From there, in terms of "how do you handle non-fatal errors", there really isn't a snap rule to give. Quite often you just propagate because there isn't anything else to do. Sometimes you retry some bounded number of times, maybe with backoff. Sometimes you log things and move on. Sometimes you have a fallback you may try. It just depends on your needs. I write a lot of network code, and I find that once my systems mature it's actually the case that rather a lot of the errors in the system get some sort of handling beyond "just propagate it up", but it's hard for me to ever guess in advance what they will be. It's a lot easy to mentally design all the happy paths than it is to figure out all the ways the perverse external universe will screw them up and how we can try to mitigate the issues.

Re: Systems Correctness Practices at Amazon Web Services

#56
post #8

> 92% of catastrophic failures in tested distributed systems were triggered by incorrect handling of nonfatal errors This. If you take nothing else away from the article (which has a lot) take this: fail well, don’t fail poorly.

This paper from 11 years ago had the exact same finding!!(Finding 10). https://www.usenix.org/system/files/conference/osdi14/osdi14...

Re: Systems Correctness Practices at Amazon Web Services

#57

>Deterministic simulation. Another lightweight method widely used at AWS is deterministic simulation testing, in which a distributed system is executed on a single-threaded simulator with control over all sources of randomness, such as thread scheduling, timing, and message delivery order. Tests are then written for particular failure or success scenarios, such as the failure of a participant at a particular stage in…

[deleted]

Re: Systems Correctness Practices at Amazon Web Services

#59
post #8

> 92% of catastrophic failures in tested distributed systems were triggered by incorrect handling of nonfatal errors This. If you take nothing else away from the article (which has a lot) take this: fail well, don’t fail poorly.

Yeh I think a lot of security screwups are also in error handling paths. This article gave me two terms I'd not heard before - 'Happy-case castrophic failures' - is a great one, and lower down there is 'goodput'.

Re: Systems Correctness Practices at Amazon Web Services

#60

>Deterministic simulation. Another lightweight method widely used at AWS is deterministic simulation testing, in which a distributed system is executed on a single-threaded simulator with control over all sources of randomness, such as thread scheduling, timing, and message delivery order. Tests are then written for particular failure or success scenarios, such as the failure of a participant at a particular stage in…

[deleted]
Post reply on HN