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.
Systems Correctness Practices at Amazon Web Services
131–140 of 143 posts
Re: Systems Correctness Practices at Amazon Web Services
#132Earlier 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.
Can't you use the formal model to write/generate a lot of unit tests to verify the actual code behaves like the model does?
There are two DIFFERENT gaps here. You're talking about the gap where what you have verified is a model, and the actual code and the model may diverge. But there is another, subtler gap: how good are you at coming up with properties? Because your verification is only as good as the properties you come up with, and the average programmer is not great at coming up with properties. (Before people attack me, I should make clear I've been working in formal methods for 3 decades now.)
Re: Systems Correctness Practices at Amazon Web Services
#133S3 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...
S3 is not a piece of software per se, it is a service. Also S3 is not better than gcs or azure blob.
Services are built on software.
S3 is likely an order of magnitude larger then those others - it's had a lot longer to grow.
Re: Systems Correctness Practices at Amazon Web Services
#134Earlier quoted context omitted.
AWS has said that the largest S3 buckets are spread over 1 million hard drives. That is quite impressive.
Red dead redemption 2 is likely on over 74 million hard drives.
I think you misunderstood. They're not saying S3 uses a million hard drives, they're saying that there exist some large single buckets that use a million hard drives just for that one bucket/customer!
Re: Systems Correctness Practices at Amazon Web Services
#135Earlier quoted context omitted.
Complexity and sheer intelligence and capability required to build either.
And what is the basis for your claim? You are not impressed by AWS's complexity and intelligence and capability to build and manage 1-2 zettabytes of storage near flawlessly?
Im more impressed by red dead redemption 2 or baldurs gate 3.
There is no “basis” other my gut feeling. Unless you can get quantified metrics to compare that’s all we got. For example if you had lines of code for both, or average IQ. Both would lead towards the “basis” which neither you or I have.
Re: Systems Correctness Practices at Amazon Web Services
#136It is interesting how the industry ended up with things like TDD when it doesn't work for something as simple as a function that adds two numbers together. While not completely useless in some edge cases, its complete lack of any kind of formal underpinnings should have given us a clue. So many bad / unexamined ideas in the Uncle Bob era. Far closer to a religion than anything else (complete with process "rituals" even).
Re: Systems Correctness Practices at Amazon Web Services
#137Earlier 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.
Can't you use the formal model to write/generate a lot of unit tests to verify the actual code behaves like the model does?
That's called specification-, model-, or property-based test generation. Google those terms. If older security or verification papers, always try adding "citeseerx" and "pdf" to the search to find research publications.
The papers will describe the strengths and weaknesses of those tools.
Re: Systems Correctness Practices at Amazon Web Services
#138> 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…
[deleted]
Re: Systems Correctness Practices at Amazon Web Services
#139Earlier quoted context omitted.
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)
That's not enough for proof purposes. It allows you to build a test that deterministically tests one path, but it does not give you control over all possible tests. In fact I seem to be a bit iconoclastic on this matter but I'm not even a fan for testing purposes. Even non-proof-based testing needs the ability to test that goroutines may execute out of order. Nothing prevents a goroutine scheduled for 2ms from now to…
There may be more there than meets the eye at first glance.
I'm not saying this easy to do at the moment, but the possibility is there.
If you can take control of all timers/sleep in your Go program, then you have, in effect, complete control of Goroutine scheduling.
If you assign a distinct time point to each goroutine, say based on its ID, and then have the goroutine sleep until that point, then you have also assigned the order in which those goroutines will run. Each will "wake up" alone, only at the next point at which the clock is forced to advance--which is when the previous goroutine blocked.
Re: Systems Correctness Practices at Amazon Web Services
#140Earlier quoted context omitted.
This paper from 11 years ago had the exact same finding!!(Finding 10). https://www.usenix.org/system/files/conference/osdi14/osdi14...
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.
Oh, thank you for pointing that out. Appreciate it.