These are chat archives for atomix/atomix

10th
Oct 2018
Alex Robin
@alexrobin
Oct 10 2018 07:04
@kuujo nice, SWIM is a great addition to Atomix! You're still keeping the simpler heartbeat protocol, right?
Johno Crawford
@johnou
Oct 10 2018 07:50
@kuujo interesting work with bitswapping, might be worth adding a few unit tests though?
Jordan Halterman
@kuujo
Oct 10 2018 07:52
Yeah still keeping the regular heartbeat protocol… it will be the default for now. But you can configure the cluster to use whichever you want:
Atomix atomix = Atomix.builder()
.withMembershipProtocol(SwimProtocol.builder()
.withProbeInterval(Duration.ofSeconds(1))
.withGossipInterval(Duration.ofMillis(200))
.withGossipFanout(2)
.build())
.build();
I actually really like the SWIM implementation. Seems pretty solid after writing the spec and implementing it from that
The tests show it tolerates network partitions pretty well as long as there’s a route between nodes, but that can be a good or a bad thing depending on how you’re using it
Johno Crawford
@johnou
Oct 10 2018 07:54
what do you run the tlaplus spec with?
Jordan Halterman
@kuujo
Oct 10 2018 07:55
TLA+ toolbox, which has the TLC model checker
Johno Crawford
@johnou
Oct 10 2018 07:55
and how do you determine if it tolerates network partitions well etc.
is that built into the spec, or is there generic network partition tests in the toolkit
Jordan Halterman
@kuujo
Oct 10 2018 08:00

Well the model checker basically searches the entire state space to verify that some invariant holds in all possible states. The invariant I defined for the SWIM model is just that nodes always transition from Alive to Suspect to Dead and that any node can only be in each of those states once per term.

https://github.com/atomix/atomix-tlaplus/blob/master/SWIM/SWIM.tla#L348-L352

There’s not really a way to validate that it does well in a network partition because the protocol doesn’t purport to tolerate network partitions completely. It just does well because it probes through peers rather than assuming if a node can’t contact another node that the node is dead. I just wanted to verify that the gossip protocol always results in an eventually consistent state through the use of epochs managed by each member (an extension to the original SWIM protocol)

you can also use temporal logic statements to verify that it will eventually reach some state, but they’re pretty complicated
That spec defines what seems to be a pretty solid extension to the SWIM paper to make the protocol actually scalable. I might write a blog post about it or something
Johno Crawford
@johnou
Oct 10 2018 08:09
looks like eclipse
Jordan Halterman
@kuujo
Oct 10 2018 08:09
it is
Johno Crawford
@johnou
Oct 10 2018 08:09
anyway, I imported it, but nothing happens when I click run
Jordan Halterman
@kuujo
Oct 10 2018 08:10
it’s complicated… you have to create a model, define the values, define the initial and next state predicates, define the invariant, and add a state constraint before running it
Johno Crawford
@johnou
Oct 10 2018 08:11
aaah ok so you need to put in those each time?
Jordan Halterman
@kuujo
Oct 10 2018 08:11
you just create and save the model
then add a state constraint:
\A source \in DOMAIN history :
\A dest \in DOMAIN history[source] :
Cardinality(DOMAIN history[source][dest]) <= 3
Johno Crawford
@johnou
Oct 10 2018 08:12
wouldn't it be a good idea to publish the models to the same repo?
Jordan Halterman
@kuujo
Oct 10 2018 08:12
that basically limits the state space so it doesn’t search forever
that constraint basically allows for three terms for each member, but currently the model will still search a much larger state space than my laptop will handle
Johno Crawford
@johnou
Oct 10 2018 08:14
yeah now it's running
Jordan Halterman
@kuujo
Oct 10 2018 08:14
it supports clustering, but I have no interest in doing that. I mostly use it as a tool for specifying distributed systems algorithms and roughly verifying the invariants
Johno Crawford
@johnou
Oct 10 2018 08:14
I see
Jordan Halterman
@kuujo
Oct 10 2018 08:14
I really like it just for writing a spec
it’s a different way of thinking
you’re not writing a program but defining the possible states, so it forces you to think about edge cases and the model checker will usually find them
Johno Crawford
@johnou
Oct 10 2018 08:15
well the syntax is different, that's for sure
that's cool
Jordan Halterman
@kuujo
Oct 10 2018 08:16
well it’s a mathematical language for defining states and state transitions
Johno Crawford
@johnou
Oct 10 2018 08:16
i assume you've found a bunch of bugs with it
can you give me an example of what you've found?
Jordan Halterman
@kuujo
Oct 10 2018 08:17
the syntax is sort of like LaTeX… actually it is LaTeX and generates a PDF:
https://github.com/atomix/atomix-tlaplus/blob/master/SWIM/SWIM.pdf
Johno Crawford
@johnou
Oct 10 2018 08:18
wondering if I can incorporate this into something i'm working on
wow still going and it's using 3 gig of data
Johno Crawford
@johnou
Oct 10 2018 08:26
so you're essentially testing your understanding of the spec
what about going from spec to code
Jordan Halterman
@kuujo
Oct 10 2018 08:31
yeah it’s probably going to go until it consumes all the memory
I don’t think that state constraint is right
it’s probably just creating and droping messages like crazy, which makes it an infinite state space
need to limit the number of messages or something
I think I found a sequencing bug in the Raft client sequencer, but I don’t remember what it was now:
https://github.com/atomix/atomix-tlaplus/blob/master/ClientSequencer/ClientSequencer.pdf
Jordan Halterman
@kuujo
Oct 10 2018 08:37
I started out implementing the SWIM protocol in code but was having trouble figuring out how to manage the gossip protocol. Once I wrote it in TLA+ it became easier to figure out the logical clock for some reason 🤷‍♂️
gotta go prep a talk for the morning
Jordan Halterman
@kuujo
Oct 10 2018 08:59
Welp... that was quick
Anyways, I’ll probably write a spec for the primary-backup protocol as well just to work out all the bugs.