Live data from Hacker News

Systems Correctness Practices at Amazon Web Services

cacm.acm.org

21–30 of 143 posts

Re: Systems Correctness Practices at Amazon Web Services

#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 in a distributed protocol. The nondeterminism in the system is controlled by the test framework, allowing developers to specify orderings they believe are interesting (such as ones that have caused bugs in the past). The scheduler in the testing framework can also be extended for fuzzing of orderings or exploring all possible orderings to be tested.

Any good open source libraries that do this that are language agnostic? Seems doable - spin up a container with some tools within it. Said tools require some middleware to know when a test is going to be run, when test is run, tools basically make certain things, networking, storage, etc "determinstic" in the context of the test run.

This is more-or-less what antithesis does, but haven't seen anything open source yet.

You of course, could write your tests well, such that you can stub out I/O, but that's work and not everyone will write their tests well anyway (you should do this anyway, but it's nicer imo if this determinism is on a layer higher than the application).

as a slight sidebar - I'm not really bullish on AI, but I think testing is one of the things where AI will hopefully shine, because the feedback loop during prompting can be driven by your actual application requirements, such that the test implementation (driven by AI), requirements (driven by you as the prompt) and "world" (driven by the actual code being tested) can hopefully help drive all three to some theoretical ideal. if AI gives us anything, I'm hoping it can make software a more rigorous discipline by making formal verification more doable.

Re: Systems Correctness Practices at Amazon Web Services

#22

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

Guessing an ordering that will trigger a bug and exploring all orderings should both be basically impossible for non-trivial scenarios, no?

Re: Systems Correctness Practices at Amazon Web Services

#23

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

Guessing an ordering that will trigger a bug and exploring all orderings should both be basically impossible for non-trivial scenarios, no?

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.

Re: Systems Correctness Practices at Amazon Web Services

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

The TLA Plus examples repository is very good: https://github.com/tlaplus/Examples . I would recommend starting with something simple like the DieHard problem.

Re: Systems Correctness Practices at Amazon Web Services

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

Tests do specific instances of a class of problem and proves that your implementation is correct for these instances. Formal verification proves the whole class.

You can have a function that returns the anagram and testing will proves it correct for some pairs of words. But to prove it for all words require formal verification. And that’s when you catch some tricky errors due to undefined behavior or library bugs because you can’t prove their semantics.

Re: Systems Correctness Practices at Amazon Web Services

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

>> a good design

good is doing a lot of heavy lifting here. The point of TLA+/Pluscal is to have a proof of the soundness of the design.

Re: Systems Correctness Practices at Amazon Web Services

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

How much effort should be put into "failing well"? I rather see the program crash than output a liability. Fail well is too broad to be useful, in my industry.

Re: Systems Correctness Practices at Amazon Web Services

#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 could also be used in a cloud, which is less resource-constrained

Re: Systems Correctness Practices at Amazon Web Services

#29
Amazing article! Using state machines is a must if you are building infrastructure control-planes. Was P a must, though? I am not sure. We have been building infrastructure control-planes for over 13 years now and every iteration we have built with Ruby. It worked wonders for us https://www.ubicloud.com/blog/building-infrastructure-contro...

Re: Systems Correctness Practices at Amazon Web Services

#30

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

similar to the integration testing component in keploy.io, which includes time freezing.

basically certain system clocks are rolled back and incremented in a deterministic manner to emulate real issues recorded from production bugs. Had lot of fun working with building this and the effect of messing with different system clocks by intercepting system calls.

https://keploy.io/docs/keploy-cloud/time-freezing/

Post reply on HN