[erlang-questions] Looking for tricky protocol examples for verification research

[Ulf Wiger]

On 29 Oct 2014, at 18:36, Jonathan Schuster <schuster@REDACTED> wrote:

> This morning I happened to find the "Erlang and Akka" thread from a couple of months ago, and it caught my eye because several people discussed exactly the sort of thing I'm researching right now: verifying that actor-based programs conform to some given protocol. In particular, I'm trying to figure out how we can do better for real-world programs instead of the simple examples used in things like session types.


I have used UBF, and like the idea of having a state- and type-based protocol checking. I thought a problem with UBF was that it really only dealt with synchronous protocols. I know Joe had some excellent ideas on how to move further, but I’m not sure they were ever implemented.

While type errors are certainly important, I believe unexpected message ordering is more so. I talked about that in my “Death by Accidental Complexity” [1] and got permission to publish the code used in the presentation [2].

Of course, any verification here would have to take into account that Erlang can implicitly ignore (buffer) messages in states where the focus is on only a few specific messages. Keeping track of message types, one could perhaps note if patterns are too general, so as to accept messages that are not expected to (or even must not) be handled in the current state. The POTS code mentioned above actually contains examples of that, where valid messages are discarded in states that do not recognize them, yet still consume them. This is in a way worse than crashing on a bad message, since this at least gives a fairly clear indication of what has gone wrong; instead the code ends up waiting indefinitely for a message that has already been received and discarded.

BR,
Ulf W

[1] http://www.infoq.com/presentations/Death-by-Accidental-Complexity
[2] https://github.com/uwiger/pots

Ulf Wiger, Co-founder & Developer Advocate, Feuerlabs Inc.
http://feuerlabs.com



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20141030/da8f833e/attachment.htm>