Systems Correctness Practices at Amazon Web Services
1–10 of 143 posts
Re: Systems Correctness Practices at Amazon Web Services
#2Wow. 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 design language that's used at AWS and other industrial places that need to serve people.
I wish more people who build distributed systems would use what he made. Proving correctness is crucial in large systems.
Re: Systems Correctness Practices at Amazon Web Services
#3Wow. 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…
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 models but kept getting issues with syntax and spec logic with anything else besides Opus.
Re: Systems Correctness Practices at Amazon Web Services
#4Wow. 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.
Re: Systems Correctness Practices at Amazon Web Services
#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 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.
This is fucking amazing
Re: Systems Correctness Practices at Amazon Web Services
#6Wow. 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…
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 during design? Therefore I’m assuming implementations still need to match the design exactly or else you would still get subtle bugs? Sorry for all the questions I’ve never actually learned formal methods but have always been interested.
Re: Systems Correctness Practices at Amazon Web Services
#7Wow. 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...
Re: Systems Correctness Practices at Amazon Web Services
#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.
Re: Systems Correctness Practices at Amazon Web Services
#9>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…
Loom for Rust does this. We also adapted it for some C++ with good success (found actual bugs that slipped tests and reviewes). Sits lower than i.e. TLA+ and is not a proof but super useful as you check the actual implementation.
Re: Systems Correctness Practices at Amazon Web Services
#10>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…
[deleted]