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

[Ulf Wiger]

On 30 Oct 2014, at 09:07, Scott Lystig Fritchie <fritchie@REDACTED> 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’ [1] 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. ;-)

> I haven't seen any postings to this list by Augusto Becciu.

I remember him posting back in 2010 [2].

BR,
Ulf W

[1] https://github.com/uwiger/locks/blob/master/doc/locks_leader.md
[2] http://erlang.org/pipermail/erlang-questions/2010-October/054088.html

* If anyone has some feedback about ‘locks’ in the field, please let me know.
You can email me in confidence if you want. Personally, I’ve used locks in the
kvdb database, and successfully negotiated both the kvdb test suite and the
Exosense server test suite (which also does things like passing transaction
contexts between processes). The ‘uw-locks-integration’ branch of kvdb has
not yet been merged into master, though, and while the idea is to eventually
use locks_leader in kvdb (or a Raft version), I’ve not yet gone there.

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