[leif]

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

[2]: http://aphyr.com/posts/284-call-me-maybe-mongodb

[lumpypua]

Ark is just about making replication as a whole trustworthy.

Then you need a formal model.