This summer, I participated in the GSoC program of CNCF graduated project TiKV[^1]. 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 upd