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

11–20 of 143 posts

Re: Systems Correctness Practices at Amazon Web Services

#11

Post by oblio »

skydhash wrote: post #4
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. It could be good in smaller, but critical and widely used utilities like SSH and terminals.

Yeah, basically all the coreutils plus all the common extras (rsync, ssh, etc) could use stuff like this.

Re: Systems Correctness Practices at Amazon Web Services

#12

Post by lopatin »

dosnem wrote: post #6
lopatin wrote: post #3

Earlier quoted context omitted.

And just a tip for who may be intersted: Claude Opus with Extended Thinking seems to be very good at converting existing code into TLA+ specs. I've found multiple bugs for personal Rust projects like this (A Snake game that allowed a snake to do a 180 degree turn), and have verified some small core C++ components at work with it as well (a queue that has certain properties around locking and liveness). I tried other…

I’ve always envisioned tla and other formal methods as specific to distributed systems and never needed to understand it. How is it used for a snake game? Also how is the TLA+ spec determined from the code? Won’t it implicitly model incorrect bugs as correct behaviour since it’s an existing state in the system? Also when using TLA from the start, can it be applied to implementations? Or is it only for catching bugs d…

Here's how it caught my Snake bug: My snake representation is a vector of key points (head, turns, tail). A snake in a straight line, of length 3, facing right can look like this: [(0,0), (2,0)]. When a Snake moves (a single function called "step_forward"), the Snake representation is compressed by my code: If the last 2 points are the same, remove the last one. So if this snake changes direction to "left", then the new snake representation would be [(1, 1), (1, 1)] and compressed to [(1, 1)] before existing out of step_forward.

Here's how the bug was caught: It should be impossible for the Snake representation to be < 2 points. So I told Opus to model the behavior of my snake, and also to write a TLA+ invariant that the snake length should never be under 2. TLA+ then basically simulates it and finds the exact sequence of steps "turns" that cause that invariant to not hold. In this case it was quite trivial, I never thought to prevent a Snake from making turns that are not 90 degrees.

Re: Systems Correctness Practices at Amazon Web Services

#13

Post by agentultra »

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…

The TigerBeetle team does this too and it's an interesting approach. One of their developers did a talk on it at HYTRADBOI this year [0].

[0] https://www.hytradboi.com/2025/c222d11a-6f4d-4211-a243-f5b7f...

Re: Systems Correctness Practices at Amazon Web Services

#14

Post by ctkhn »

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.

Re: Systems Correctness Practices at Amazon Web Services

#16

Post by dmd »

ctkhn wrote: 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 entire point of using formal methods is that testing will never, ever catch everything.

Re: Systems Correctness Practices at Amazon Web Services

#17

Post by senthil_rajasek »

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

It would also be nice to list some "best practices" on how to handle non-fatal errors. I would be definitely interested to know of any sources.

Re: Systems Correctness Practices at Amazon Web Services

#18

Post by supriyo-biswas »

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…

Also somewhat similar to what Antithesis is doing.

Re: Systems Correctness Practices at Amazon Web Services

#20

Post by skydhash »

senthil_rajasek wrote: post #17
mlhpdx wrote: 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.

It would also be nice to list some "best practices" on how to handle non-fatal errors. I would be definitely interested to know of any sources.

The same way you handle fatal errors, by specifying the exceptional circumstances and how to handle them (retry, alternative actions, or signaling to another handler up the call/request tree). Something’s correct output may not be our thing’s correct input.
Post reply on HN