Initial implementation for Raft

[twitu]

This a first draft of Raft on DPC. I raised this PR to get some initial feedback on this implementation.

TODOs

There's still some subtlety to be added. Mostly related to election term value and how it affects node's ActorState when sending Replication/Commit messages and also having a better ActorState to track log entries as well. There also appears to be a bug which is preventing the Leader from moving to commit state after getting a majority on the replication request.

Challenges/Workarounds

I also faced some challenges in the implementation, most prominently because there is no concept of local state changes without sending messages. So implementing these two parts of the Raft algorithm required hacky workarounds.

• Timeout - There is no way to update a local timer without sending messages through protlets. So I used OneOf protlet to act as a decision between regular leader follower replication communication and a reelection scenario.
• Local state change - Again there is no way to change local state without sending messages through protlets. So the transition of a Follower to a Candidate which is only a local state change cannot be modeled well. That is there is not way to have a Candidate state. In this implementation, the reElection protlet directly converts a Follower to a Leader if the majority vote is met otherwise the node remains a Follower.

[kandersen]

Thank you for your interest in the project!

I will be sure to return the favour as soon as possible, and will be happy to take a look at your work :) For now, a quick thought for each of your workarounds.

Re timeouts, I think that is precisely the right approach - the notion of time is lacking from the specification language. I wonder if there might be a relatively smooth way of extending some notion of relative time by adding a sequence number to messages, but the specification language (and the specification language for logics in the tradition from which DPC arises) is very upfront about not having a notion of time.

The implementation can of course take all the time it wants (hah) to fulfil a protocol like OneOf, as you have done it.

Re the local state, the point that there's no local state change is by design - the specification layer talks only of externally visible state. I do however wonder if you could model the internal state change by sending a mock message to some other node that represents some internal, decision making "subcomponent". Does that make sense? 1 participant in raft is represented by 2 nodes in DPC.

[twitu]

Re the local state, the point that there's no local state change is by design - the specification layer talks only of externally visible state. I do however wonder if you could model the internal state change by sending a mock message to some other node that represents some internal, decision making "subcomponent". Does that make sense? 1 participant in raft is represented by 2 nodes in DPC.

For this I part I was thinking one way to implement it could be by sending a message to self and then changing state based on that. I'll try out this approach and add a Candidate state.