6 ms·

Introducing Ark: A Consensus Algorithm For TokuMX and MongoDB

37 points by zardosht 12y ago

yid 12y ago
Interesting -- sounds like once implemented, you could leverage the consensus algorithm to implement atomic multi-document/multi-table transactions too?
- leif 12y ago
  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] shows MongoDB losing data even with majority write concern, which if used properly, is supposed to make MongoDB a CP system. But because of the design flaws in the election algorithm, you can't rely on it perfectly. The changes we made in Ark fix the election algorithm to make majority write concern actually able to guarantee data safety, so you can treat it as a fully CP system. [1]: http://docs.tokutek.com/tokumx/tokumx-transactions.html http://docs.tokutek.com/tokumx/tokumx-transactions.html [2]: http://aphyr.com/posts/284-call-me-maybe-mongodb http://aphyr.com/posts/284-call-me-maybe-mongodb
  - lumpypua 12y ago
    Ark is just about making replication as a whole trustworthy. Then you need a formal model.
fintler 12y ago
Is there a TLA+ or Coq model available for this?
- leif 12y ago
  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.
  - sseveran 12y ago
    If you have not used a model checker you don't have a proof. Please don't say that you have one. You are just hoping for the best. See this to get yourself started: http://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html http://research.microsoft.com/en-us/um/people/lamport/tla/by...
    - deleted 12y ago
      [deleted]
    - aurelius 12y ago
      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.
      - sseveran 12y ago
        thats not the real issue. The issue with model checkers is verifying that production code actually exactly implements the model.
        aurelius 12y ago
        Yes, that is <i>another</i> issue with model checkers. Either way, your original comment is still nonsense.
        sseveran 12y ago
yourad_io 12y ago
I believe this is officially one name too many matching /ar[ck]/ http://en.wikipedia.org/wiki/Ark#Technology http://en.wikipedia.org/wiki/Ark#Technology http://en.wikipedia.org/wiki/Arc#Computing_and_gaming http://en.wikipedia.org/wiki/Arc#Computing_and_gaming
justin66 12y ago
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.
- leif 12y ago
  It won't be patented. We hope others find it helpful and consider implementing it in similar systems.

37 points by zardosht 12y ago

yid 12y ago

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

leif 12y ago
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] shows MongoDB losing data even with majority write concern, which if used properly, is supposed to make MongoDB a CP system. But because of the design flaws in the election algorithm, you can't rely on it perfectly. The changes we made in Ark fix the election algorithm to make majority write concern actually able to guarantee data safety, so you can treat it as a fully CP system. [1]: http://docs.tokutek.com/tokumx/tokumx-transactions.html http://docs.tokutek.com/tokumx/tokumx-transactions.html [2]: http://aphyr.com/posts/284-call-me-maybe-mongodb http://aphyr.com/posts/284-call-me-maybe-mongodb
- lumpypua 12y ago
  Ark is just about making replication as a whole trustworthy. Then you need a formal model.

fintler 12y ago

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

leif 12y ago
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.
- sseveran 12y ago
  If you have not used a model checker you don't have a proof. Please don't say that you have one. You are just hoping for the best. See this to get yourself started: http://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html http://research.microsoft.com/en-us/um/people/lamport/tla/by...
  - deleted 12y ago
    [deleted]
  - aurelius 12y ago
    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.
    - sseveran 12y ago
      thats not the real issue. The issue with model checkers is verifying that production code actually exactly implements the model.
      - aurelius 12y ago
        Yes, that is <i>another</i> issue with model checkers. Either way, your original comment is still nonsense.
        sseveran 12y ago

yourad_io 12y ago

I believe this is officially one name too many matching /ar[ck]/ http://en.wikipedia.org/wiki/Ark#Technology http://en.wikipedia.org/wiki/Ark#Technology http://en.wikipedia.org/wiki/Arc#Computing_and_gaming http://en.wikipedia.org/wiki/Arc#Computing_and_gaming

justin66 12y ago

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.

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