Dealing with Deadlocks using reasoning engines

[bblfish]

I don't know much about this, but I know who does.

In 2019 there was a very interesting talk on an typesafe actor system developed by @alcestes who tied a reasoning engine into dotty to allow it to reason about deadlocks.

See the thread here: https://twitter.com/bblfish/status/1358462175174664192

Perhaps that can be adapted to Libretto's Linear Types for Scala?

[TomasMikula]

Neat! I have seen lchannels by @alcestes (here's my single paragraph comparison to Libretto).

Using a reasoning engine to verify a property about a Libretto program is definitely something that could be done, since a Libretto program is just data (~ a free monoidal category).

My preferred way of excluding bad programs though is to make them unrepresentable. I.e. not to have a verification procedure that returns true or false. But rather have the verification procedure transform the program to a representation that prevents bad programs. I have no doubt a representation preventing deadlocks exists, though I haven't spent much time trying to find one.

[alcestes]

Yes, Effpi types alone (without the compiler plugin) ensure "linearity" --- but I need to explain the quotes :-)

An Effpi type can say e.g.: a program uses a communication channel x to send an integer exactly once; or it uses channel y to receive a value z that is then forwarded unchanged over channel w. What is tracked is the usage of communication channels, and that capability captures the way in which session types ensure linear usage of communication channels.

However, Effpi types do not have a general notion of linearity. So, an Effpi type can ensure e.g. that Bob uses a channel x to receive two coins c1 and c2 from Alice, and then sends them back unchanged over a channel y; however, Effpi cannot prevent Bob from copying c1 and c2 into an internal collection and use those copies later.

The Effpi compiler plugin only inspects the communication behaviour described by the AST of Effpi types; it does not inspect the AST of Effpi DSL programs --- because the DSL is designed to strictly enforce the types.

[TomasMikula]

I see, thanks for clarification.

I am wondering one more thing: Can an Effpi program communicate over two channels concurrently? For example, Alice waiting for a message from either Bob or Carol, and whichever comes first, Alice will respond to that one first. Or are the protocols in Effpi fundamentally sequential?

[alcestes]

The protocols in Effpi include parallel composition, so they are not "sequential".

In the current implementation, an Effpi process can receive messages from only one channel at a time. So, Alice can have a channel b carrying messages from Bob, and another channel c carrying messages from Carol --- but Alice cannot listen from b and c at the same time: she should receive from b and then from c, or vice versa.

A pattern similar to the one you describe can be achieved by having Bob and Carol send their messages on a same channel a towards Alice, while Alice uses a to receive whichever message comes first. There can also be other processes listening on a. This creates a race between produces and consumers --- but this can be OK, and the compiler plug-in can analyse whether the resulting configuration would cause e.g. a deadlock.

[TomasMikula]

👍 Thanks. Sorry for questioning, but I find working out examples a good way to learn about a system. Continuing the example, would you be able to express that over the shared channel a, there comes exactly one message of type B (from Bob) and exactly one message of type C (from Carol)?

[alcestes]

Yes, that is possible - but probably not in the way hinted in your question (if I understood correctly).

If the shared channel a has type Chan[B|C], then:

• the type of Bob's process can force him to use a to send B exactly once
• the type of Carol's process can force her to use a to send C exactly once
• the type of Alice's process can force her to use a exactly twice, and do something different depending on what she receives (e.g. after Alice receives B, she must input again, and if she receives C, she must terminate). However, Alice's type would also include some behaviour in case she receives B or C twice (which would not occur in this scenario, but it might if someone else is using channel a besides Bob and Carol).

In other words, the property that "over the shared channel a, there comes exactly one message of type B (from Bob) and exactly one message of type C (from Carol)" would emerge from the overall composition of types - but it cannot be observed by only looking at Alice's type..

[bblfish]

@TomasMikula @alcestes on the Category Theory Zulip I asked about CT models of Actor Systems. (current invite link).
There were some interesting replies, a couple of which i linked to from the tweet thread.
https://twitter.com/bblfish/status/1567062264926150656

I have not had time to study those articles yet. I am trying to understand Actors as best as possible for the work I am doing on decentralised social networks. It seems from the discussion above that linear types come in here too.

My experience is that actors are a very good way to represent resources on the web, which is what I am interested in. It is also how I build my Reactive Solid server. Problem is that Akka has now moved to a closed license. Now is the time to come up with a radically new framework.

[TomasMikula]

I generally find myself aligned with some high-level description of actors (interaction instead of shared state, autonomy of each actor, program large systems the same way we program small systems), but find concrete implementations (Akka, Erlang) too untyped and hard to reason about locally.

I was actually working with Akka Typed at the time when I conceived of Libretto. A type like Stream[Msg] => Unit just says too little about the behavior of the actor. For example, it looks like it is OK to send any Msg at any time, but that's often not the case and you end up writing code to detect and handle illegal state. Or, if a message has a replyTo: ActorRef[Resp], there is no guarantee this actor will ever reply.

I didn't know right away that I would end up representing programs as arrows of a category. I just had this problem that concurrency with futures/actors/fibers is too cumbersome and dangerous, and stream libraries (often advertised as "declarative concurrency") too limited in expressivity.

Do you have some requirements for what "resources on the web" should be capable of?
Session types are going to be useful (only) if there's a more complex interaction than a single request-response.