These are chat archives for atomix/atomix
We are no longer monitoring this channel, please join Slack! https://join.slack.com/t/atomixio/shared_invite/enQtNDgzNjA5MjMyMDUxLTVmMThjZDcxZDE3ZmU4ZGYwZTc2MGJiYjVjMjFkOWMyNmVjYTc5YjExYTZiOWFjODlkYmE2MjNjYzZhNjU2MjY
Atomix atomix = Atomix.builder() .withMembershipProtocol(SwimProtocol.builder() .withProbeInterval(Duration.ofSeconds(1)) .withGossipInterval(Duration.ofMillis(200)) .withGossipFanout(2) .build()) .build();
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
Dead and that any node can only be in each of those states once per term.
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)
\A source \in DOMAIN history : \A dest \in DOMAIN history[source] : Cardinality(DOMAIN history[source][dest]) <= 3