This summer, I participated in the GSoC program of CNCF graduated project TiKV1. I worked on the distributed transaction model of TiKV. I provided an update to the TLA+ specification regarding the recently implemented feature "Async commit". By running TLC model checker on the new model, we gain more confidence in the async commit design.
Before I applied to the GSoC program, I haven't got any code contributions for open source projects. It's the first time I participate in the FOSS community. Get involved in the community made me really excited, and it was an unforgettable experience for me.
Here, I want to express my sincere thanks to my two mentors: Andy Lok and Ziqian Qin. They are very friendly and gave me a lot of help in the program, leading me into the new field (for me) of distributed transactions and TLA+. Without their help, I couldn't get started in such a short time, and finally made a substantial contribution to TiKV/CNCF.
My task is to update the TLA+ for async commit, it is tracked by this issue. TLA+ is a formal language for modeling programs and systems--especially concurrent and distributed ones. TLA+ and its tools are useful for eliminating fundamental design errors, which are hard to find and expensive to correct in code.
TiKV's transaction model is originally derived from Google Percolator on BigTable, and the TiKV authors made many specific optimizations and enhancements based on it. Therefore, to verify the changes to the transaction model, the TiKV transaction team used TLA+ toolchains to verify the safety of the design.
My task is to update the TLA+ spec. The whole project is roughly divided into two parts:
- Before the "async commit":
- Add the CheckTxnStatus command and deprecate the Cleanup command.
- Add optimistic read, pessimistic read.
- Add invariants for checking snapshot read.
- "Async commit" itself:
- Change states type definitions
- Async version prewrite
- Async version commit check
- Async version CheckTxnStatus (resolve lock)
- 1 phase commit, Not finished yet :(
Before starting the async part, there are a lot of preparatory works to do, because the current version(before GSoC) of TLA+ specification has fallen behind the actual code implementation a lot.
The first is regarding the stale lock resolution. TiKV (code-impl) used a command called CheckTxnStatus to resolve a stale lock, but in the spec, the lock is cleaned by "TiKV server" itself spontaneously. Since the MVCC and lock resolution is the backbones of transaction safety, My first task is to update the lock resolution method. Following the Rust code, I implemented the action pair ClientCheckTxnStatus and ServerCheckTxnStatus along with communication messages. During the process, my understanding of both Google Percolator and the TLA+ language got deeper.
pr: Read key, read snapshot isolation check
After that, my mentors proposed the read snapshot isolation check, since TiKV provides fully ACID-transactions. There are two kinds of read in TiKV: optimistic read (Snapshot Isolation) and pessimistic read (Repeatable Read). I spited CLIENT_KEY to CLIENT_READ_KEY and CLIENT_WRITE_KEY, and added ClientReadOptimistic ServerReadOptimistic, and updated ClientLockKey, ServerLockKey. However, we encountered some difficulties here. The read result message is kept as "states", and the distinct "value timestamp" and "lock_failed" messages are just too much. Such exponential growth makes our model checking impossible to complete in a reasonable time. After a considerable time of discussion with my mentors, we thought of a solution: according to the actual code implementation, we erase some reply messages from the state variables. Here, we made many changes to the message transmission, and it makes us finished the TLC model checking.
Finally, model checking test1 on an ordinary PC takes ~3 hours, and it takes ~15 hours to complete another slightly more complicated test. In practical terms, this is a completely acceptable time, and we have made a good trade-off.
There's also a small change on "amending pessimistic lock".
In the second half of the program, we entered the async commit part. Due to the huge difference between the code and the TLA+ specification, my mentors and I discussed in-depth how to implement the model and the invariant check. I also referred to many technical details in Yilin Chen's article. He explained to me many related issues. I am very grateful for his help. The key point of async commit is the new way of accessing that the transaction can be successfully committed. In order to do that, I added new state type definitions, async versions of Prewrite and CheckTxnStatus, and, most importantly, the commit consistency check, we need to bring forward the invariant check.
In the update mentioned above, the content before the async commit has passed complete model check and can be sure to be complete.
In order to verify the if there's any silly mistake quickly during the development process, I also added two small test cases, whose model checking can be finished within minutes.
It is a pity that because of the read isolation level check, a lot of time was spent here, which led to the fact that I did not complete the entire task in the end. The async commit update still have some bugs for a few corner cases, and had not been fully reviewed (since TLA+ is a tricky language, we need to be really careful to avoid mistakes) and the 1-pc(1 phase commit) task is also postponed. I plan to complete these features after the GSoC program.
Thanks again to my mentor Andy Lok and Ziqian Qin, and TiKV maintainers of SIG-transaction!
Footnotes
-
TiKV is a key-value store, like a hashmap but reliably persistent and scalable to terabytes of data. It runs across multiple nodes for reliability, availability, and scalability - even if you lose some nodes, your data will never be lost and will still be readable and writable; as your data grows, you can simply add more nodes. TiKV supports transactions, like traditional SQL databases, and is ACID-compliant, i.e., transactions are atomic, isolated (with snapshot isolation), and durable. ↩