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 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.
They'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).
If you don't show me the syntax above the fold on first page view, I'm something like 50% more likely to disregard. I know this has false positives associated, but I don't entirely feel in the wrong for this either.
Indeed, they hid source code samples a bit too deep.
Easiest I could find is to go to tutorials in the menu, for instance, [1]. Such pages have links to actual source files which live on GitHub, like [2].
I love ideas like this. It's "top-down" programming: start with a high-level, formal description of the system. ("There are 4 communicating state machines."). Then you gradually add detail to the model and go "downwards" until you reach the level where you can actually generate code.
Yep agree. It’s a great way to write solid software. You can do something similar even when not using formal methods:
Start by writing the skeleton of the complete application. By “skeleton” I mean all interfaces implemented with placeholder all-in-memory code. And then step-by-step refine the whole application until it is done.
I was surprised, because from a performance perspective, I'd expect that if you can generate code for USB drivers, you can also do so for cloud services? You have generally have better and more control over hardware in the latter case?
The state machines seem pretty low level, so I don't see in principle why efficient code couldn't be generated from them.
Is it an issue of wanting the implementations to use many cores perhaps?
I wonder if the P-generated code is still used for USB drivers today, or if they moved away from that approach and just use the modeling process?
Thanks for any clarification
FWIW I'm using 3 or 4 C/C++ code generators for https://www.oilshell.org, and I've the layer of indirection useful in many ways (although it also can make it harder for people to understand)
Yes, P has been updated a lot in the last 6 years. Much better documentation and compiler. There is going to be a new release in a couple of months with a verifier as well as a way to check P specifications on implementation.
Readit News
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 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.
See https://github.com/awslabs/shuttle and a whitepaper at https://www.amazon.science/publications/using-lightweight-fo...
Disclaimer: used to work at AWS and had some involvement in this stuff
* Describe a distributed system as a bunch of FSMs.
* Verifies its correctness to some degree (but not proves yet).
* Geneerates C or C# code; compact enough to suit even device drivers.
* Allows to describe test suites and monitoring tools for the code.
* MIT license.
(still looking for syntax sample btw)
Easiest I could find is to go to tutorials in the menu, for instance, [1]. Such pages have links to actual source files which live on GitHub, like [2].
[1]: https://p-org.github.io/P/tutorial/clientserver/ [2]: https://github.com/p-org/P/tree/master/Tutorial/1_ClientServ...
Start by writing the skeleton of the complete application. By “skeleton” I mean all interfaces implemented with placeholder all-in-memory code. And then step-by-step refine the whole application until it is done.
It works great!
Can you expand on this answer at the end about whether the generated code is run in production or not?
https://youtu.be/5YjsSDDWFDY?t=2200
I was surprised, because from a performance perspective, I'd expect that if you can generate code for USB drivers, you can also do so for cloud services? You have generally have better and more control over hardware in the latter case?
The state machines seem pretty low level, so I don't see in principle why efficient code couldn't be generated from them. Is it an issue of wanting the implementations to use many cores perhaps?
I wonder if the P-generated code is still used for USB drivers today, or if they moved away from that approach and just use the modeling process?
Thanks for any clarification
FWIW I'm using 3 or 4 C/C++ code generators for https://www.oilshell.org, and I've the layer of indirection useful in many ways (although it also can make it harder for people to understand)
I'd missed it, glad it came up again!
P: A programming language for asynchrony, fault-tolerance and uncertainty - https://news.ycombinator.com/item?id=14377941 - May 2017 (40 comments)
The P programming language - https://news.ycombinator.com/item?id=12673739 - Oct 2016 (87 comments)
But that invites the question: where to execute this?
StepFunctions, whether you love you some AWS or not, provides all the storage, compute, &c resources you need, and then some.
[1] https://docs.aws.amazon.com/step-functions/
[0] https://en.wikipedia.org/wiki/P-code_machine
[0] https://en.wikipedia.org/wiki/BCPL