P Language: a state machine-based programming language (2021) | Hacker News Reader

P Language: a state machine-based programming language (2021)

p-org.github.io

75 pointsnine_k26 comments

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.

I'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.

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

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

Yes, indeed. We talk about it here https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-... (or here https://lamport.azurewebsites.net/tla/formal-methods-amazon.... if you can't access that).

A language to describe distributes systems as state machines.

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

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.

(still looking for syntax sample btw)

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

[1]: https://p-org.github.io/P/tutorial/clientserver/ [2]: https://github.com/p-org/P/tree/master/Tutorial/1_ClientServ...

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.

It works great!

There was a talk on P at StrangeLoop as well: https://www.youtube.com/watch?v=5YjsSDDWFDY

I watched this a few weeks ago -- great talk and exciting tool!

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)

Previously: https://news.ycombinator.com/item?id=12673739 Oct 2016, 86 comments

I'd missed it, glad it came up again!

Thanks! Macroexpanded:

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)

I don't remember seeing it back then. I hope that it has somehow improved during the 6 years that passed.

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.

These seems a fascinating, full tool, compared to partial, arguably ugly JSON DSL like StepFunctions[1].

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/

AFAICT it compiles to C or C# sources which you can then link into your larger app.

Is the name a reference to Pascal's P-code machine?

[0] https://en.wikipedia.org/wiki/P-code_machine

My guess is that it's the next entry in the BCPL "lineage".

[0] https://en.wikipedia.org/wiki/BCPL

Apparently no relation.

Can someone provide a simple hello world example of a program in P? I searched the website. It provides definitions and ideas for many concepts. But not a single example.

Not quite a hello world, but the Tutorials section in the left-side menu is actually a set of examples, each one an annotated program.

See for example the first one, a client/server application implementing bank withdrawals with safety and liveness properties: https://p-org.github.io/P/tutorial/clientserver/

https://p-org.github.io/P/tutsoutline/

Simple Client Server example: https://p-org.github.io/P/tutorial/clientserver/

This title doesn't really tell the reader what the P language is for.

dang, would it be possible to change the title to something like, "P Language: a state machine-based programming language" ? (That's from the first diagram on the page.)

Ok, done. Thanks!

That's a nice example of what I mean by looking for alternate titles or representative language (https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...)

> [Step 2] Install Java Runtime

Nooooooope. No thank you.

https://p-org.github.io/P/getstarted/install

Reply on news.ycombinator.com