Live data from Hacker News

Systems Correctness Practices at Amazon Web Services

cacm.acm.org

101–110 of 143 posts

Re: Systems Correctness Practices at Amazon Web Services

#101

Earlier quoted context omitted.

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.

We should have formal verification of the formal verification specification. Standing on a turtle.

I've heard that called "validation". In other words, you verify that your solution meets the problem specification, but you validate that your specification is actually what you need.

Re: Systems Correctness Practices at Amazon Web Services

#102
post #99
post #77

Earlier quoted context omitted.

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 introdu…

Also a huge proponent of Antithesis and their current work, but there definitely were some notable precedents at or around that time e.g. MODIST from 2009 ( https://www.usenix.org/legacy/event/nsdi09/tech/full_papers/... ), which similarly tried to build a "model checker for distributed systems". As another interesting historical side note, I have wondered about the similarities between Antithesis and "Corensic", a s…

Corensic was impressive tech. I actually debriefed with one of their founders years ago. IIRC, their product was focused on finding single-process concurrency bugs.

Deterministic hypervisors are by no means new. Somebody once told me that VMWare used to support a deterministic emulation mode (mostly used for internal debugging). Apparently they lost the capability some time ago.

Re: Systems Correctness Practices at Amazon Web Services

#103

Earlier quoted context omitted.

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.

We should have formal verification of the formal verification specification. Standing on a turtle.

You're looking for foundational, proof-carrying code with verified logins. I can't find the verified logic right now, though. Examples:

https://www.cs.princeton.edu/~appel/papers/fpcc.pdf

https://hol-light.github.io/

I'll also add that mutation testing has found specification errors, too.

https://github.com/EngineeringSoftware/mcoq

Re: Systems Correctness Practices at Amazon Web Services

#104
post #71

Earlier quoted context omitted.

It looks like Coyote[0], which is used in azure, was an evolution of P# which was an evolution of P [0] https://www.microsoft.com/en-us/research/wp-content/uploads/...

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

OK, but then not for generating production code?

I thought I read that somewhere, but now I can't find the claim

Re: Systems Correctness Practices at Amazon Web Services

#105

>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…

It ought to be the norm, and it is (slowly) getting there. For example, the .NET 8 standard library now has a TimeProvider type to allow test frameworks to provide substitute implementations of the system clock.

Re: Systems Correctness Practices at Amazon Web Services

#106
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.

I experienced this. The Go/Rust/Haskell way of avoiding exceptions in the language is better than the C#/Java/JavaScript way.

To the point I've seen it cause real bugs in production.

The problem in Node is you can either throw to make a 4xx or you can return a 4xx so downstream there are 2 things to check.

Re: Systems Correctness Practices at Amazon Web Services

#107
post #14

This sounds interesting but as someone who hasn't worked at AWS, and isn't already familiar with TLA+ or P, I would have liked to see even a hello world example of either of them. Without that, it sounds like a lot of extra pain for things that a good design and testing process should catch anyway. Seeing a basic example in the article itself that would give me a better insight into what these actually do.

I experimented with TLA, and the graphical toolbox didn't seem to work or match the tutorial. Kinda disappointing: I wanted to use TLA, and I'm otherwise a big fan of Lamport's work, from the utilitarian Latex to the intellectually satisfying paper on time, clocks, and distributed systems.

Re: Systems Correctness Practices at Amazon Web Services

#108
post #47

S3 remains one of the most amazing pieces of software I've ever seen. That thing a few years ago where they just added strong read-after-write consistency to the whole system? Incredible software engineering. https://aws.amazon.com/blogs/aws/amazon-s3-update-strong-rea...

I had the distinct pleasure of working on S3 (Lifecycle) during the timeframe that the index team was working on the rearchitecture that enabled the read-after-write consistency.

I can confidently say that as impressive as S3 is from the outside, it's at least that impressive internally, both in implementation, and organizational structure.

Re: Systems Correctness Practices at Amazon Web Services

#109

> 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 i…

I suspect you can relatively easily obtain a completely deterministic machine by running QEMU in 100% emulation mode in one thread. But what you are after is controlled deterministic execution, and it's far harder. That is, making your multiple processes to follow a specific dance that triggers an interesting condition must be very involved, when seen from the level as low as CPU and OS scheduler. Hence a language-agnostic setup is hard to achieve and especially hard to make it do your bidding. It may drown you in irrelevant details.

I once built a much, much simpler thing that allowed to run multiple JVM threads in a particular kind of lockstep, by stubbing and controlling I/O operations and the advance of the system time. With that, I could run several asynchronously connected components in particular interaction patterns, including not just different thread activation order but also I/O failures, retries, etc. It was manageable, and it helped uncover a couple of nasty bugs before the code ever ran in prod.

But that was only possible because I went with drastic simplifications, controlling not the whole system but only particular synchronization points. It won't detect a generic data race where explicit synchronization would be just forgotten.

Re: Systems Correctness Practices at Amazon Web Services

#110

Earlier quoted context omitted.

I really do respect the engineering efforts. But object stores are embarrassingly parallel, so if such a migration should be possible somewhere without down time, then it is definitely object stores.

Where would you make make the cut that takes advantage of object store parallelism? That is, at what layer of the stack do you start migrating some stuff to the new strongly consistent system on the live service? You can't really do it on a per-bucket basis, since existing buckets already have data in the old system. You can't do it at the key-prefix level for the same reason. Can't do both systems in parallel and tr…

Obviously depends on how they delivered read after write.

Likely they don't have to physically move data of objects, but the layer that writes and reads coordinates based on some version control guarantees e.g in database land MVCC is a prominent paradigm. They'd need a distributed transactional kv store that tells every reader what the latest version of the object is and where to read from.

An object write only acknowledges finished if the data is written and kv store is updated with new version.

They could do this bucket by bucket in parallel since buckets are isolated from each other.

Post reply on HN