I experimentally implemented Raft in Java but I am not very confident that I did it correctly.
I wish there was a way to implement stateful programs that guarantee "forward progress" and are "steady state systems". I think essentially a state machine that cannot be trapped in a state. Debugging the absence of something of forward moving progress or lack of causation is very difficult.
When there's essentially different actors in the system and they can interact with eachother by communicating, they each have a number of states they can get into. There's no guarantee that the system shall converge on a state that forward progress can be made. Maybe TLA+ is the right answer here.
YMMV but I think (my) reasoning over stateful systems is rather difficult, I think there's lots of hidden states that we cannot easily detect or reason about because they're in our blind spots. Especially related to synchronization. I think it's part of what makes multithreading and distributed systems so hard, because every component can be in a different state and if something is not where it is expected to be, the baton doesn't get passed to the correct state. If you check for something too early, you have a race condition.
If we could see in slow motion what was going on, an interaction between different actors, we could work out why something happens the way it does. But usually the logs are too numerous to get to this detail. I think animation can save us, but what does a Raft animation look like?
How often have you seen an endless spinner? It's as if a completion event was raised but didn't get detected and the system is waiting for something that shall never occur. I want this kind of error to be impossible. This is one form of hidden state that prevents progress.
I wrote an eventually consistent mesh protocol in Python and tested it with Jepsen, it is not linearizable because the consistency level is "eventually consistent".
I don't understand how Raft can scale writes or reads across multiple machines due to the round trip time talking to other nodes.
Microsoft has a library/tool called Coyote* that helps with testing distributed systems; you can write tests/specifications, Coyote will systematically explore nondeterminism in your system and check if your tests still pass. If there's a failure, it'll show the sequence of events that led to the failing test.
I started a project to implement Raft with a KV-store on top, similar to the article, meaning to use Coyote to test it; I didn't get that far before losing interest, though. It's reassuring to read that it took Phil several months to write the code in the post, it's good to know that this is a decidedly nontrivial problem.
Sounds like a job for state machines like you can build out with a library like xstate[0] (though I'm sure there are similar libraries in whatever language you choose. Python has one called automat[1])
These exist to formalize state logic (current state, computing state, transitioning state etc), you can even produce diagrams based on their definitions. Advanced libraries like xstate even have Actors are part of the core of the library
Don’t have anything to comment on the rest, but my understanding with respect to:
> I don't understand how Raft can scale writes or reads across multiple machines due to the round trip time talking to other nodes.
Is that at the point where that becomes a bottleneck you scale to multiple clusters, where the read/write destination cluster is determined by a key and whatever your preferred hashing mechanism is.
I experimentally implemented Raft in Java but I am not very confident that I did it correctly.
I wish there was a way to implement stateful programs that guarantee "forward progress" and are "steady state systems". I think essentially a state machine that cannot be trapped in a state. Debugging the absence of something of forward moving progress or lack of causation is very difficult.
When there's essentially different actors in the system and they can interact with eachother by communicating, they each have a number of states they can get into. There's no guarantee that the system shall converge on a state that forward progress can be made. Maybe TLA+ is the right answer here.
YMMV but I think (my) reasoning over stateful systems is rather difficult, I think there's lots of hidden states that we cannot easily detect or reason about because they're in our blind spots. Especially related to synchronization. I think it's part of what makes multithreading and distributed systems so hard, because every component can be in a different state and if something is not where it is expected to be, the baton doesn't get passed to the correct state. If you check for something too early, you have a race condition.
If we could see in slow motion what was going on, an interaction between different actors, we could work out why something happens the way it does. But usually the logs are too numerous to get to this detail. I think animation can save us, but what does a Raft animation look like?
How often have you seen an endless spinner? It's as if a completion event was raised but didn't get detected and the system is waiting for something that shall never occur. I want this kind of error to be impossible. This is one form of hidden state that prevents progress.
I wrote an eventually consistent mesh protocol in Python and tested it with Jepsen, it is not linearizable because the consistency level is "eventually consistent".
I don't understand how Raft can scale writes or reads across multiple machines due to the round trip time talking to other nodes.