github-repos/tla-plus
1
0
Fork 0
mirror of https://github.com/pingcap/tla-plus.git synced 2025-03-14 02:20:09 +08:00
Code Issues Packages Projects Releases Wiki Activity
43 Commits 2 Branches 0 Tags 1.4 MiB
TLA 89.1%
Coq 10.7%
Makefile 0.2%
00f95e6457
Go to file
Yilin Chen 00f95e6457
protect primary key of pessimistic txn 
Signed-off-by: Yilin Chen <sticnarf@gmail.com>
2019-10-30 13:40:11 +08:00
CollapseRollbacks move collapserollback optimization to a new separate directory (#24) 2018-08-22 11:33:57 -07:00
ConcurrentPercolator move collapserollback optimization to a new separate directory (#24) 2018-08-22 11:33:57 -07:00
OptimizedCommitTS optimized commit ts: remove the cost of getting commitTS (#20) 2018-05-14 17:55:33 +08:00
Percolator percolator: allow clients having different primary keys. (#16) 2018-04-02 14:04:53 +08:00
PessimisticTransaction protect primary key of pessimistic txn 2019-10-30 13:40:11 +08:00
Raft Port raft from ongardie/raft.tla as-is. (#3) 2018-02-01 15:20:23 +08:00
RaftMerge RaftMerge: rollback and TLC models. (#11) 2018-03-22 14:56:07 +08:00
TwoPC Fix silly error in Coq proof. 2018-01-21 20:45:05 +08:00
.gitignore percolator: allow clients having different primary keys. (#16) 2018-04-02 14:04:53 +08:00
LICENSE Initial commit 2017-12-19 19:12:25 +08:00
README.md Update README.md 2018-05-08 22:52:09 -07:00

README.md

TLA+ in TiDB

About TLA+

TLA+ is a formal specification and verification language to help engineers design, specify, reason about, and verify complex software and hardware systems. It is widely used to verify the algorithms in distributed systems.

Using TLA+ in TiDB

In TiDB, we use TLA+ for the following purposes:

  • To verify the distributed consensus algorithm - Raft.
  • To verify the implementation of distributed transaction.

For further information about TLA+, see tla-plus-resources.