Erlang leader election - code available?

[Thomas Arts]

The leader election module gen_leader contains a bug.

I just returned from a chat at Chalmers with a PhD student
that is looking into verification of the gen_leader. He made
clear to me that the algorithm we used was valid for systems
in which nodes go down, but is not correct for a situation in
which nodes restart (not even if the restart is reasonably slow
compared to the recovery).
He found the bug, I see it as my responsibility to find a solution
for the error (a deadlock and sometimes a partitioning in which
two leaders are elected). 

Has anyone observed that in practise? The likelyhood that it
appears is probably not very large, but this is a ticking bomb,
of course.

I am looking into the matter. If someone already fixed it, let me
know.

Cheers
Thomas

---
Dr Thomas Arts 
     Program Manager 
     Software Engineering and Management 
IT-university in Gothenburg 
Box 8718, 402 75 Gothenburg, Sweden 
http://www.ituniv.se/

Tel +46 31 772 6031 
Fax +46 31 772 4899