[erlang-questions] Looking for tricky protocol examples for verification research
Sun Nov 9 15:53:22 CET 2014
On 08 Nov 2014, at 17:49, Benoit Chesneau <> wrote:
> On Thu, Oct 30, 2014 at 10:51 AM, Ulf Wiger <> wrote:
> On 30 Oct 2014, at 09:07, Scott Lystig Fritchie <> wrote:
> > 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 do. It’s probably not the majority opinion, but I’m leaning towards
> ‘locks_leader’  as the best leader-election approach, with the huge
> proviso that it hasn’t seen much - if any - real action*, as far as I know. ;-)
> how would you compare it to raft? Also can we add/remove dynamically nodes which wasn't really possible with gen_leader?
Raft does include leader election, but that’s only part of what it does. I assume the Raft leader election algorithm will work correctly even in an Erlang setting, but some differences between Raft and locks:
1. Raft uses backoff and randomized sleep to resolve election conflicts; locks uses a form of reactive deadlock resolution that converges immediately.
2. Raft makes use of replication history to elect the most suitable leader. This is difficult for locks, since it will fall back on a global ordering of candidates when needed.
For fun, I started trying to implement Raft on top of the locks_leader implementation. I got so far as to add a ‘surrender’ operation in locks_leader, so the newly elected leader can decide to make another process the leader. This is where I stopped, waiting for a time where I could do some more careful analysis of the problem space.
Ulf Wiger, Co-founder & Developer Advocate, Feuerlabs Inc.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the erlang-questions