Systems Correctness Practices at Amazon Web Services

Trust me, I love FDB, but that's not the same thing. The FDB team IIRC had to write their own programming language to do this. It's not a agnostic layer above the application.

The problem with coupled tooling is that no one will use it. That's what is cool about antithesis. If they're able to complete their goal, that's basically what will be achieved.

I'm sure I heard that something like this existed for the JVM ages ago (like 15 years). I don't remember the details so it might not be quite the same, but a colleague was telling me about some tech which would test your concurrency by automatically selecting bad scheduling orders.

+1 for rr. Bonus feature is you can also time-travel debug! It's spoiled me forever...

S3 is probably the largest object store in the world. The fact that they can upgrade a system like that to add a feature as complex as read-after-write with no downtime and working across 200+ exabytes of data is really impressive to me.

Sure, but whose (compatible) API is GCS using again? Also keep in mind that S3 is creeping up on 20 years old, so backing a change in like that is incredible.

GCS's metadata layer was originally implemented with Megastore (the precursor to Spanner). That was seamlessly migrated to Spanner (in roughly small-to-large "region" order), as Spanner's scaling ability improved over the years. GCS was responsible for finding (and helping to knock out) quite a few scaling plateaus in Spanner.

> GCS comes across as a much better thought-out and built product

I've worked with AWS and GCS for a while, and I have the opposite opinion. GCS is what you get if you let engineers dictate to customers how they are allowed to do work, and then give them shit interfaces, poor documentation, and more complexity than adds value.

There's "I engineered the ultimate engineery thing", and then there's "I made something people actually like using".

Maybe. But Google do have a reputation which makes selecting them for infrastructure a risky endeavor

From my POV Amazon designs its services from a "trust nothing, prepare for the worst case" perspective. Eventual consistency included. Sometimes that's useful and most of the time it's a PITA.

Services are built on software.

S3 is likely an order of magnitude larger then those others - it's had a lot longer to grow.

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 during design? Therefore I’m assuming implementations still need to match the design exactly or else you would still get subtle bugs? Sorry for all the questions I’ve never actually learned formal methods but have always been interested.

It seems like the new DeepSeek performs at a similar level as Opus 4. At least to preliminary Aider benchmarks.

Yeah, basically all the coreutils plus all the common extras (rsync, ssh, etc) could use stuff like this.

You can write proofs in TLA+ and many other formalisms. You don’t need to ever use a model checker. The proofs hold for an infinite number of infinite-length executions. We are definitely not limited to finite behaviors.

+1.

We have used Coyote/P# not just for model checking an abstract design (which no doubt is very useful) but testing real implementations of production services at Microsoft.

Whereas, formal verification only catches what properties one correctly specifies in what portions of the program one correctly specifies. In many, there's a gap between these and correctness of the real-world code. Some projects closed that gap but most won't.

Hey Will. I'm a huge fan of the work you all are doing, and of FoundationDB, but I don't believe it's accurate that DST was invented at FoundationDB (or, maybe it was, but was also used in other places around the same time or before).

For example, the first implementations of AWS's internal lock service (Alf) used DST as a key part of the testing strategy, sometime around 2009. Al Vermeulen was influential in introducing it at AWS, and I believe it built on some things he'd worked on before.

Still, Anithesis is super cool, and I really admire how you all are changing the conversation around systems correctness. So this is a minor point.

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

they also made a browser game to showcase their DST, where you can inject faults and see how tigerbeetle recovers

https://sim.tigerbeetle.com/

Keploy is doing the same thing, in same space - https://github.com/keploy/keploy

Which is largely an extended version of what FoundationDB does (from many of the same people).

related: https://docs.oracle.com/en/java/javase/21/docs/api/java.base...

Perhaps, but there is still some value in "capturing the bug with a failing test." If some ordering presents a defect, you can recreate it and prove that you've fixed the bug.

For in-process go scheduling, some progress has been made here; see: https://go.dev/blog/synctest

But `synctest.Wait` won't work for non-durably blocked goroutines (such as in the middle of a TCP syscall) so requires memory-based implementations of e.g. net.Conn (I've plugged in https://pkg.go.dev/google.golang.org/grpc/test/bufconn with good success)

"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.

I worked on adding golang time freezing in keploy by using the approach from the go playground which used a fixed time (2009-11-10 23:00:00 UTC) but also increments the system clock used by goroutines.

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
    }

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.

The same way you handle fatal errors, by specifying the exceptional circumstances and how to handle them (retry, alternative actions, or signaling to another handler up the call/request tree). Something’s correct output may not be our thing’s correct input.

I think the best practice is to handle them with equal attention as the happy path. Error handling is usually afterthought from my experience.

What is the system state when it does error?

What is the best possible recovery from each error state?

What can the user/caller expect for an error?

One I see a lot is not being careful to use the correct error type / status code.

E.g. if you're in python and raise a value error when an API is rate limited, someone down stream from you is going to have a bad time.

And then someone decides to "fix it" by adding a null check and things really go off the rails.

Same paper, they're just referencing it:

> In 2014, Yuan et al. found that 92% of catastrophic failures in tested distributed systems were triggered by incorrect handling of nonfatal errors.

It gets tricky in a distributed system, or I suppose any server process. When the program crashes it just starts up again, and sometimes picks up the same input that caused the crash.

Typical example would be processing an event that you can't handle from a message queue. You don't want to crashloop, so you'd probably have to throw it away on a dead letter queue and continue processing. But then, is your system still correct? What happens if you later receive another event relating to the same entity, which depends on the first event? Or sometimes you can't even tell which entity the malformed or bug-triggering event relates to, and then it's a real problem.

In distributed systems, that means you either wants the whole system to crash (consistency) or that the node that crash is not critical for any operation and can be out until you clean out the state that makes it crash (a partition). The issue is when you fail to be in those two categories. Meaning some aspects are concurrent, but some are sequential.