Systems Correctness Practices at Amazon Web Services

Post by inaseer » Fri, May 30, 2025, 5:37 PM UTC

algorithmsRcool wrote: post #49

chubot wrote: post #28

One thing I wondered about the P language: It seems like in the early days, it was used at Microsoft to generate C code that’s actually used at runtime in the Windows USB stack? But now it is no longer used to generate production code? I asked that question here, which I think was the same question as in a talk: https://news.ycombinator.com/item?id=34284557 It seems like if the generated code is used in a kernel, it…

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

Post by bit_razor » Fri, May 30, 2025, 5:45 PM UTC

amazingamazing wrote: post #21

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

Post by SteveNuts » Fri, May 30, 2025, 5:53 PM UTC

positisop wrote: post #68

simonw wrote: 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...

Google Cloud Storage had it for eons before S3. GCS comes across as a much better thought-out and built product.

Post by mjb » Fri, May 30, 2025, 5:57 PM UTC

wwilson wrote: post #51

sebstefan wrote: post #5

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

Post by hamburglar » Fri, May 30, 2025, 6:05 PM UTC

nickpsecurity wrote: post #67

dmd wrote: post #16

Earlier quoted context omitted.

The entire point of using formal methods is that testing will never, ever catch everything.

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.