What’s been disappointing to me is how easily formal methods are dismissed in industry.
TLA takes some time to learn to wield effectively but it pays off on spades.
Systems Correctness Practices at Amazon Web Services
61–70 of 143 posts
Re: Systems Correctness Practices at Amazon Web Services
#62> 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.
[deleted]
Re: Systems Correctness Practices at Amazon Web Services
#63What’s been disappointing to me is how easily formal methods are dismissed in industry. TLA takes some time to learn to wield effectively but it pays off on spades.
[deleted]
Re: Systems Correctness Practices at Amazon Web Services
#64> 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…
There have historically been two giant adoption challenges for DST.
(1) Previously, you had to build your entire system around one of the simulation frameworks (and then not take any dependencies).
(2) It’s way too easy to fool yourself with weak search/input generation, which makes all your tests look green when actually you aren’t testing anything nontrivial.
As you say, Antithesis is trying to solve both of these problems, but they are very challenging.
I don’t know of anybody else who has a reliable way of retrofitting determinism onto arbitrary software. Facebook’s Hermit project tried to do this with a deterministic Linux userspace, but is abandoned. (We actually tried the same thing before we wrote our hypervisor, but found it didn’t work well).
A deterministic computer is a generically useful technology primitive beyond just testing. I’m sure somebody else will create one someday, or we will open-source ours.
Re: Systems Correctness Practices at Amazon Web Services
#65>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?
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)
Re: Systems Correctness Practices at Amazon Web Services
#66The 92 % stat looks really interesting! It’s rarely the spectacular crash that knocks a cluster over. Instead, the “harmless” retry leaks state until everything breaks at 2 a.m on one fateful Friday. Evidently, we should budget more engineering hours for mediocre, silent failures than for outright disasters. That’s where the bodies are buried.
Or survivorship bias: the major issues, that have been addressed, do not cause problems cause they were addressed. Some of the minor issues that are not addressed randomly do cause major issues.
Re: Systems Correctness Practices at Amazon Web Services
#67This 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 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.
Re: Systems Correctness Practices at Amazon Web Services
#68S3 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.
Re: Systems Correctness Practices at Amazon Web Services
#69> to more lightweight semi-formal approaches (such as property-based testing, fuzzing, and runtime monitoring)
Ok, I get how property-based testing and fuzzing have a relationship to formal methods (the thing being checked looks like part of a formal specification, and in some sense these are a subset of the checks that a model-checking confirms), but calling runtime monitoring a "semi-formal approach" seems like a real stretch.
Re: Systems Correctness Practices at Amazon Web Services
#70> to more lightweight semi-formal approaches (such as property-based testing, fuzzing, and runtime monitoring) Ok, I get how property-based testing and fuzzing have a relationship to formal methods (the thing being checked looks like part of a formal specification, and in some sense these are a subset of the checks that a model-checking confirms), but calling runtime monitoring a "semi-formal approach" seems like a r…
Runtime monitoring with something like PObserve is a semi-formal approach. Not just regular alarming and metrics.