Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Systems Correctness Practices at Amazon Web Services

cacm.acm.org

Post reply on HN
Print view View original

111–120 of 143 posts

Re: Systems Correctness Practices at Amazon Web Services

#111

Post by amw-zero »

belter wrote: post #7
EGreg wrote: post #2

Wow. I used to correspond with Leslie Lamport years ago (about his Buridan's Principle papers, etc.) Today I went to his website and discovered a lot about TLA+ and PlusCal. He still maintains it: https://lamport.azurewebsites.net/tla/peterson.html?back-lin... I must say ... it would make total sense for a guy like that, who brought mathematics to programming and was an OG of concurrent systems, to create a systems d…

>> Proving correctness is crucial in large systems. You can't do that... The model checker says the specification satisfies the properties you wrote within the finite state space you explored...

You can write proofs in TLA+ and many other formalisms. You don’t need to ever use a model checker. The proofs hold for an infinite number of infinite-length executions. We are definitely not limited to finite behaviors.

Re: Systems Correctness Practices at Amazon Web Services

#112

Post by mdaniel »

jiggawatts wrote: post #105
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…

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.

related: https://docs.oracle.com/en/java/javase/21/docs/api/java.base...

Re: Systems Correctness Practices at Amazon Web Services

#113

Post by koito17 »

ninetyninenine wrote: post #91
SteveNuts wrote: post #81

Earlier quoted context omitted.

It's funny that things that are pinnacles of human engineering exist like this where the general public has no idea it even exists, though they (most likely) use it every single day.

I find red dead redemption 2 more impressive. I don’t know why. It sounds stupid but S3 on the surface has the simplest api and it’s just not impressive to me when compared to something like that. I’m curious which one is actually more impressive in general.

> S3 on the surface has the simplest api and it’s just not impressive [...]

Reminded of the following comment from not too long ago.

https://news.ycombinator.com/item?id=43363055

Re: Systems Correctness Practices at Amazon Web Services

#114

Post by UltraSane »

ninetyninenine wrote: post #91
SteveNuts wrote: post #81

Earlier quoted context omitted.

It's funny that things that are pinnacles of human engineering exist like this where the general public has no idea it even exists, though they (most likely) use it every single day.

I find red dead redemption 2 more impressive. I don’t know why. It sounds stupid but S3 on the surface has the simplest api and it’s just not impressive to me when compared to something like that. I’m curious which one is actually more impressive in general.

AWS has said that the largest S3 buckets are spread over 1 million hard drives. That is quite impressive.

Re: Systems Correctness Practices at Amazon Web Services

#115

Post by UltraSane »

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.

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?

Re: Systems Correctness Practices at Amazon Web Services

#116

Post by rossjudson »

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.

GCS's metadata layer was originally implemented with Megastore (the precursor to Spanner). That was seamlessly migrated to Spanner (in roughly small-to-large "region" order), as Spanner's scaling ability improved over the years. GCS was responsible for finding (and helping to knock out) quite a few scaling plateaus in Spanner.

Re: Systems Correctness Practices at Amazon Web Services

#117

Post by purpleidea »

It's very interesting (I applaud this) that one of the main goals seems to be to make it more approachable as compared to TLA+, but then they go in write it in C# which I consider to be an incredibly unapproachable community and language.

I'm not trying to draw the ire of the Microsoft fan boys, and there are certainly smart people working on that, but it's just not going to happen for most people.

Had this been in golang, or maybe java, I'm sure many more hands would be digging in! Having said that, I hope this helps bring correctness and validation more into the mainstream. I've been casually following the project for a while now.

My long-term goal is to integrate model validation into https://github.com/purpleidea/mgmt/ so if this is an area of interest to you, please let me know!

Re: Systems Correctness Practices at Amazon Web Services

#118

Post by ninetyninenine »

UltraSane wrote: post #114
ninetyninenine wrote: post #91

Earlier quoted context omitted.

I find red dead redemption 2 more impressive. I don’t know why. It sounds stupid but S3 on the surface has the simplest api and it’s just not impressive to me when compared to something like that. I’m curious which one is actually more impressive in general.

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.

Re: Systems Correctness Practices at Amazon Web Services

#119

Post by rtpg »

UltraSane wrote: post #115
nickpsecurity wrote: post #67

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.

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?

In most domains you're always going to have the possibility of a gap.

The real thing though, is that if you have a verified formal model and a buggy implementation, then _you know_ your problem is at that model implementation level.

Could be the implementation is wrong. Could be that the "bug" is in fact not a bug according to your model. But your model isn't "wrong". If your model says that A happens in condition B, then that is what should happen!

You can avoid second guessing a lot of design patterns with models, and focus on this transitional layer.

If someone came up to you and said "I built a calculator and with this calculator 1/0 becomes 0" you don't say "oh... maybe my model of division is wrong". You think the calculator is wrong in one way or another.

Maybe the calculator's universe is consistent in some way but in that case its model is likely not the same model of division you're thinking of. This eliminates entire classes of doubt.

Re: Systems Correctness Practices at Amazon Web Services

#120

Post by SteveNuts »

ninetyninenine wrote: post #118
UltraSane wrote: post #114

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

There's likely over a trillion active SQLite databases in use right now.
Post reply on HN