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

[Jonathan Schuster]

On Thu, Oct 30, 2014 at 4:07 AM, Scott Lystig Fritchie <
fritchie@REDACTED> wrote:

> Hrm, well, there is the Multi-Paxos framework that's the foundation for
> riak_ensemble.
>
>     https://github.com/basho/riak_ensemble
>
> There are four different Raft protocol implementations mentioned at:
>
>     http://raftconsensus.github.io/
>
> Is this the sort of thing you're looking for?
>
> Elsewhere, verifying the good/bad health of the gen_leader protocol.
> Its implementations have splintered, so I'm not quite sure which one is
> the highest quality today, perhaps this one?  Ulf Wiger and/or Andrew
> Thompson might also have some opinions ... I haven't seen any postings
> to this list by Augusto Becciu.
>
>     https://github.com/abecciu/gen_leader_revival
>
>
I've only had a chance to glance at these so far, but both these and the
POTS example Ulf mentioned look possibly relevant.

More generally, I'm looking for the kinds of scenarios that one might use
contracts to specify in a non-concurrent world: instances in which you
expect some component you're interacting with to have a certain behavior,
so you specify that behavior in some way that the computer understands. My
hunch is that something similar could be useful for communication-focused
programs, but it's unclear what. It would be especially useful if anyone
points out in these examples "at line X of file Y, I want to state
invariant Z but have no way of doing so".

>From what I've seen, session types come closest to solving this problem,
but they tend to be overly restrictive, and it's not obvious how to apply
session types to actor-based programs, because session types assume that
channels are created separately from the processes that receive messages on
them.

I'm especially interested in examples that expect a particular behavior
from PIDs sent as messages, since this adds an extra layer of complexity
not normally addressed in the classic communicating finite state machine
literature. Session types deal with this with what they call "carried
types", and I'm curious what other mechanisms I might be able to devise for
those situations.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20141030/72c72327/attachment.htm>