3 ms·
My team at AWS has been using P heavily for modelling and reasoning about distributed storage and database protocols and designs. I'm a big fan. The sweet spot
by mjb 4y ago
My team at AWS has been using P heavily for modelling and reasoning about distributed storage and database protocols and designs. I'm a big fan. The sweet spot for P in my mind comes from the fact that it's a much more approachable language, and mental model, than TLA+ (or Pluscal) for most programmers. That means that folks can pick up formal verification more easily, and then expand into tools like TLA+ or Dafny as their needs change.
I find myself reaching for P when, in the past, I would have reached for Pluscal. TLA+ is still my go-to for more "conceptual" problems, but I find the state machine model in P perfect for cloud systems work.
Ankush Desai did a great talk at HPTS'22 about P, and finding critical distributed systems bugs early: http://hpts.ws/papers/2022/HPTS2022.pdf http://hpts.ws/papers/2022/HPTS2022.pdf He's also been working on some very interesting new directions for the verifier, and for closing the gap between specification and implementation for systems that are specified using P.
- Taikonerd 4y agoI'm really excited to hear that this is being used in industry. I think I heard that AWS also used TLA+ to find some very subtle bug in S3, too.
- gamegoblin 4y agoThey've also developed a library that plugs into their actual Rust code to verify it (rather than writing a secondary model in TLA+ or P, it's easier to verify the actual system source code). See https://github.com/awslabs/shuttle https://github.com/awslabs/shuttle and a whitepaper at https://www.amazon.science/publications/using-lightweight-formal-methods-to-validate-a-key-value-storage-node-in-amazon-s3 https://www.amazon.science/publications/using-lightweight-fo... Disclaimer: used to work at AWS and had some involvement in this stuff
- mjb 4y agoYes, indeed. We talk about it here https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/abstract https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-... (or here https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon.... if you can't access that).