Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Introducing Ark: A Consensus Algorithm For TokuMX and MongoDB

tokutek.com

Post reply on HN
Print view View original

11–19 of 19 posts

Re: Introducing Ark: A Consensus Algorithm For TokuMX and MongoDB

#11

Post by lumpypua »

leif wrote: post #6
fintler wrote: post #3

Is there a TLA+ or Coq model available for this?

No, none of us know how to use those. :( If you're interested in building one and you have experience with them, get in touch and we can work through it together. I think the biggest challenge would be modeling the semantics of write concern, but I'm not that familiar with proof assistants, maybe that isn't too hard.

It looks like you've read the Call Me Maybe series of posts over at aphyr.com. He tests a number of distributed systems (Mongo, Riak, Cassandra, etc) and their behavior under network partitions and almost all of them fuck up and lose data. A summary of results can be found at [1].

Amazon has used a TLA+ model for their distributed systems and found a bunch of bugs [2].

Seriously, everybody fucks this up. Please please learn a model checker and check your algorithm.

[1] In the "Summary of Jepsen Test Results" section: http://blog.foundationdb.com/call-me-maybe-foundationdb-vs-j...

[2] https://research.microsoft.com/en-us/um/people/lamport/tla/a...

Re: Introducing Ark: A Consensus Algorithm For TokuMX and MongoDB

#12

Post by lumpypua »

leif wrote: post #5
yid wrote: post #2

Interesting -- sounds like once implemented, you could leverage the consensus algorithm to implement atomic multi-document/multi-table transactions too?

Multi-document and multi-collection transactions are already a part of TokuMX[1]. Since commit of the oplog insert is atomic together with the actual operation's changes to documents, atomicity is also guaranteed in replication. Atomicity and MVCC in a sharded system is something we're working on, but it's unrelated to Raft/Ark. Ark is just about making replication as a whole trustworthy. The jepsen post on MongoDB[2…

Ark is just about making replication as a whole trustworthy.

Then you need a formal model.

Re: Introducing Ark: A Consensus Algorithm For TokuMX and MongoDB

#14

Post by [deleted] »

lumpypua wrote: post #11
leif wrote: post #6

Earlier quoted context omitted.

No, none of us know how to use those. :( If you're interested in building one and you have experience with them, get in touch and we can work through it together. I think the biggest challenge would be modeling the semantics of write concern, but I'm not that familiar with proof assistants, maybe that isn't too hard.

It looks like you've read the Call Me Maybe series of posts over at aphyr.com. He tests a number of distributed systems (Mongo, Riak, Cassandra, etc) and their behavior under network partitions and almost all of them fuck up and lose data . A summary of results can be found at [1]. Amazon has used a TLA+ model for their distributed systems and found a bunch of bugs [2]. Seriously, everybody fucks this up. Please plea…

[deleted]

Re: Introducing Ark: A Consensus Algorithm For TokuMX and MongoDB

#15

Post by leif »

lumpypua wrote: post #11
leif wrote: post #6

Earlier quoted context omitted.

No, none of us know how to use those. :( If you're interested in building one and you have experience with them, get in touch and we can work through it together. I think the biggest challenge would be modeling the semantics of write concern, but I'm not that familiar with proof assistants, maybe that isn't too hard.

It looks like you've read the Call Me Maybe series of posts over at aphyr.com. He tests a number of distributed systems (Mongo, Riak, Cassandra, etc) and their behavior under network partitions and almost all of them fuck up and lose data . A summary of results can be found at [1]. Amazon has used a TLA+ model for their distributed systems and found a bunch of bugs [2]. Seriously, everybody fucks this up. Please plea…

We are working on several ways to prove to ourselves and the community that what we have is correct. The most important is obviously testing. We have tests that demonstrate the problems we found, and Ark passes those tests. Publishing this explanation and soliciting feedback is another.

We have run Jepsen and have not been able to get it to show data loss in TokuMX. The problems it found in MongoDB were already fixed in other ways in earlier versions of TokuMX, but we're trying to get Jepsen to demonstrate the other problems we've found.

Model checking may be another way we can prove correctness, but since Ark is so similar to Raft, I think the Raft model in TLA+[1] is probably sufficient. Anyway, we'd also need a proof that the model is equivalent to the implementation, and I don't know of a way to do that, so I think functional tests are more important.

In any case, we'll look in to using a model checker, and any help would be greatly appreciated. If you're interested, feel free to email me.

[1]: https://ramcloud.stanford.edu/~ongaro/raft.tla

Re: Introducing Ark: A Consensus Algorithm For TokuMX and MongoDB

#16

Post by leif »

justin66 wrote: post #13

Does Tokutek intend to patent this consensus algorithm? If there's any possibility at all - I'm asking because of your track record - we're legally better off not reading about it at all, which is sad.

It won't be patented. We hope others find it helpful and consider implementing it in similar systems.

Re: Introducing Ark: A Consensus Algorithm For TokuMX and MongoDB

#17

Post by sseveran »

leif wrote: post #15
lumpypua wrote: post #11

Earlier quoted context omitted.

It looks like you've read the Call Me Maybe series of posts over at aphyr.com. He tests a number of distributed systems (Mongo, Riak, Cassandra, etc) and their behavior under network partitions and almost all of them fuck up and lose data . A summary of results can be found at [1]. Amazon has used a TLA+ model for their distributed systems and found a bunch of bugs [2]. Seriously, everybody fucks this up. Please plea…

We are working on several ways to prove to ourselves and the community that what we have is correct. The most important is obviously testing. We have tests that demonstrate the problems we found, and Ark passes those tests. Publishing this explanation and soliciting feedback is another. We have run Jepsen and have not been able to get it to show data loss in TokuMX. The problems it found in MongoDB were already fixed…

If you don't know how to use a model checker you have no business creating a distributed algorithm. Either implement someone else's or do it right. The world has enough broken distributed algorithms and we really don't need any more. Either you are using Raft and you can depend on its proofs and just do the work to ensure that the model is implemented correctly or you are using something different and you need to write the proofs and models.

The casual attitude that most people show when building these algorithms mind blowing.

Re: Introducing Ark: A Consensus Algorithm For TokuMX and MongoDB

#18

Post by aurelius »

sseveran wrote: post #10
aurelius wrote: post #9

Earlier quoted context omitted.

If you have used a model checker, you probably don't have a proof either. You have a model that might not be accurate, and testing all its inputs may be combinatorially prohibitive.

thats not the real issue. The issue with model checkers is verifying that production code actually exactly implements the model.

Yes, that is another issue with model checkers. Either way, your original comment is still nonsense.

Re: Introducing Ark: A Consensus Algorithm For TokuMX and MongoDB

#19

Post by sseveran »

aurelius wrote: post #18
sseveran wrote: post #10

Earlier quoted context omitted.

thats not the real issue. The issue with model checkers is verifying that production code actually exactly implements the model.

Yes, that is another issue with model checkers. Either way, your original comment is still nonsense.

No. No it is not. See the Amazon paper if you want an overview.
Post reply on HN