Some feedback after trying P

[gabrielgiussi]

Hi folks 👋
After watching Ankush's presentation I'm really interested on using P to model a distributed system involving datomic peers, datomic transactor and kafka topics to prove some message ordering guarantees.
As a programmer, I think the actor model is much more friendly than having to write TLA+, however I've faced some challenges during this week that didn't allow me to complete my work.
I'm adding a list of them here hoping you find this feedback useful and potentially give me some tips to overcome some of them:

Main issues I've faced

1. I really missed being able to write unit tests for my functions. Coming from FP with a really support for operations on collections I'm making a lot of mistakes having to operate on them using an imperative style and calculating indexes and dealing with mutable state, so it would be nice to be able to test those as functions in isolation (I could make them always receive the state from the machine as a parameter so I can test them without having to have a machine instance). What I did was to write similar functions in scala and testing them there, searching for a collection that will have similar semantics (e.g. ArrayBuffer for the P sequence). It helped me a bit but it is a lot of extra work for something beyond this initial Proof of concept I'm doing.
2. I have no feedback during execution and sometimes my process hang, in one case even ended with a out of memory error, and it is hard to track where the problem is coming from, if it hangs is probably a buggy while loop but I can't say which one. Adding print statements doesn't help because they are only shown after execution ended and only if the execution found a bug.
3. For the out of memory error I had to put an upper bound on the number of checks I was doing over a collection, which of course it goes against any safety property I would like to test. I did it as a way to unblock me and continue with the PoC, but again it is hard to track where that is coming from.
4. To find my away around the lack of feedback in successful executions that I was expecting to be failing, I add to add an assert that fail after a certain amount of executions using a counter, so I could see the print outputs.
5. After recompiling the test seemed to be running with the old code, I'm 100% sure about this because I completely removed an assertion, compiled successfully the code (even double checking that the CSharp code generated didn't include the assertion anymore) and after running it again it continued failing with the same assertion. What I had to do to overcome this is always cleaning up the PCheckerOutput folder.
6. I missed boolean operations like and and or, I can mirror them using functions except in the case I need them to shortcircuit, e.g. and(index < sizeof(aSeq),aSeq(index) > 1)). For this case I had to introduce a boolean var and a break to exit from a while loop.

Things it would be nice to have

1. A function to generate uuids built-in so I can use it to uniquely identify messages.
2. Built-in functions to operate over collections, e.g. slice.
3. Passing state as part of the goto statement, to avoid polluting the machine state with vars for some values that only make sense within a single transition. e.g. I would like to send a message to another process and then do a goto WaitingResponse(request.id) passing the id to the state so I can assert the response corresponds to my request by matching the id. With this I don't have to add another var to the machine and remember to clean it up after receiving the response.

What I did to make sense of my execution was to process the trace.json file and created lamport diagrams from it, let me know if you could be interested in such tooling, I would like to contribute to P if you think it could be useful, maybe as another file to generate on failed executions (or even on successful ones).
The tool requires some conventions about always including the sender of a message, although I saw there is an issue proposing adding that implicitly already, and a way to uniquely identify a message to match send and receive events.

Thanks for the great work on P!
Cheers.

[gabrielgiussi]

I found that P supports foreign functions and foreign types, which could help me to solve of the issues I described like the need for built-in functions to operate over collections and the possibility to unit test those functions.