Update TLA+ Spec for async commit

[andylokandy]

The TiKV has recently been launching a new feature in the transaction model named Async commit. It's an optimization that reduces the commit latency from 2PC to 1PC. However, this feature has not been reflected in the TLA+ Specs.

This issue tracks updating the spec and also running TLC model checker on the new model to gain more confidence on the async commit design.

[zhuo1angT]

Hi @andylokandy, I'm interested in this project, and I'd like to take part in the GSoC 2021. What I can do to start?

[WT-Liu]

Hi @andylokandy, I'm interested in this project, and I'd like to take part in the GSoC 2021. What I can do to start?

Hi @zhuo1angT Thanks for your interest! The students application of GSoC 2021 will be open on Mar 30. Stay tuned please!

[andylokandy]

This issue is now tracked by tikv/tikv#10319