Raft

[shayanh]

Raft basic protocol implementation.

This PR contains:

• Raft model checked spec.
• Raft Go tests.
• Locally shared archetype resourced implemented. This resource can be safely shared between concurrent running archetypes.
• Fix a bug in mpcalctx.go. Moved panic recovery before ctx.preRun() to catch preRun() panics. The previous version panic recovered by a monitor and caused infinite blocking on a subsequent ctx.Stop() call.
• TLA bug fix: According to TLC semantics, in SubSeq function if from is greater than to, just return an empty sequence.
• TLA bug fix: When making a TLA function, if domain of the function is not a tuple, then the output shouldn't be a tuple too.

[shayanh]

I agree that the persistence is required (according to Raft paper, in addition to log, we should also persist currentTerm and votedFor). This PR is so large and I suggest working on persistence in another PR. And yes, your help is much appreciated. I should work on 538B presentation and the writing.

[shayanh]

Also we can run etcd using tmpfs, so it uses memory as file system and there will no disk overhead. We can use this hack in case of need.

[fhackett]

Re: tmpfs; I thought about it, but am not seriously considering it (yet). In case of need, yes.

I forgot one last comment: we should make sure the two TLA+ bugs are fixed in the interpreter as well, otherwise the fuzz tests will "find" the changes here eventually.

Otherwise, looks good.