<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Oct 30, 2014 at 4:07 AM, Scott Lystig Fritchie <span dir="ltr"><<a href="mailto:fritchie@snookles.com" target="_blank">fritchie@snookles.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hrm, well, there is the Multi-Paxos framework that's the foundation for<br>
riak_ensemble.<br>
<br>
    <a href="https://github.com/basho/riak_ensemble" target="_blank">https://github.com/basho/riak_ensemble</a><br>
<br>
There are four different Raft protocol implementations mentioned at:<br>
<br>
    <a href="http://raftconsensus.github.io/" target="_blank">http://raftconsensus.github.io/</a><br>
<br>
Is this the sort of thing you're looking for?<br>
<br>
Elsewhere, verifying the good/bad health of the gen_leader protocol.<br>
Its implementations have splintered, so I'm not quite sure which one is<br>
the highest quality today, perhaps this one?  Ulf Wiger and/or Andrew<br>
Thompson might also have some opinions ... I haven't seen any postings<br>
to this list by Augusto Becciu.<br>
<br>
    <a href="https://github.com/abecciu/gen_leader_revival" target="_blank">https://github.com/abecciu/gen_leader_revival</a><br>
<span><font color="#888888"><br></font></span></blockquote><div><br></div>I've only had a chance to glance at these so far, but both these and the POTS example Ulf mentioned look possibly relevant. <br><br>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".<br><br>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.<br><br></div><div class="gmail_quote">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.<br></div></div></div>