github-repos/tla-plus
1
0
Fork 0
mirror of https://github.com/pingcap/tla-plus.git synced 2024-12-26 04:20:10 +08:00
Code Issues Packages Projects Releases Wiki Activity
master
tla-plus/DistributedTransaction
History
zhuo1ang b80ac83420
add check txn status, read key, read SI check (#37) 
* Add CheckTxnStatus Msgs

* Add CheckTxnStatus, haven't checked by the TLC

revert a change

DistributedTransaction: fix checkTxnStatus bugs

DistributedTransaction: CheckTxnStatus: refactor

change a var name

Co-authored-by: Andy Lok <andylokandy@hotmail.com>

DistributedTransaction: CheckTxnStatus: format spec

update CheckTxnStatus comment

Co-authored-by: Andy Lok <andylokandy@hotmail.com>

DistributedTransaction: CheckTxnStatus: update comments

* Add SI check

DistributedTransactions: upd min_commit_ts

DistributedTransactions: fix tla parse err

DistributedTransactions: upd tests

upd lock failed

DistributedTransactions: upd read write keys

DistributedTransactions: upd Test2

DistributedTransactions: fix many bugs

* DistributedTransactions: extract unlock_key function

DistributedTransactions: avoid client check txn rollback itself

DistributedTransactions: add ClientCheckTxnStatus to `Next`

DistributedTransactions: amend pessimistic lock

DistributedTransactions: add read SI check

DistributedTransactions: upd pdf version

DistributedTransactions: remove ServerCleanupLock

DistributedTransactions: refactor ClientReadFailed CheckTxnStatus

DistributedTransactions: upd server lock key

DistributedTransactions: fix ClientRetryLockKey bug

DistributedTransactions: fix ReadSI def

* DistributedTransactions: upd max read times

DistributedTransactions: upd max read times

DistributedTransactions: fix bug

DistributedTransactions: upd

DistributedTransactions: refactor, upd some comments

DistributedTransactions: refactor, upd

* DistributedTransaction: Add max client check txn times

DistributedTransaction: upd lock min_commit_ts check

DistributedTransaction: rename wrong name to current_ts

DistributedTransaction: reformat some code

* fix wrong pessimistic lock amend

DistributedTransactions: fix pessimistic lock amend bug

upd

upd

upd

upd

upd

upd

upd

upd

* upd read SI check

upd

refactor ClientRetryLockKey

upd ClientRetryCommit

upd max_lock_key_time

upd

fix bugs

upd pessimistic ReadSI check, same as optimistic one

* upd

remove some resp msgs

upd possible msg lost

* apply code review suggestion

upd

* restucture distributed transaction spec

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* fix comment

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* update comment

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* update assume

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* update comment

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* enable snapshot checks

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* fix pessimistic si check

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* add comment

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* add comment

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* add comment

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* fix typo

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* fix dead end in optimistic prewrite

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

* add test5

Signed-off-by: Andy Lok <andylokandy@hotmail.com>

Co-authored-by: Andy Lok <andylokandy@hotmail.com>
2021-08-22 22:06:49 +08:00
..
DistributedTransaction.toolbox add check txn status, read key, read SI check (#37) 2021-08-22 22:06:49 +08:00
DistributedTransaction.pdf add check txn status, read key, read SI check (#37) 2021-08-22 22:06:49 +08:00
DistributedTransaction.tla add check txn status, read key, read SI check (#37) 2021-08-22 22:06:49 +08:00
README.md DistributedTransaction: rewrite monotonicity formulas to check SnapshotIsolation (#33) 2020-10-28 10:20:02 +08:00
Test1.cfg add check txn status, read key, read SI check (#37) 2021-08-22 22:06:49 +08:00
Test1.tla add check txn status, read key, read SI check (#37) 2021-08-22 22:06:49 +08:00
Test2.cfg add check txn status, read key, read SI check (#37) 2021-08-22 22:06:49 +08:00
Test2.tla add check txn status, read key, read SI check (#37) 2021-08-22 22:06:49 +08:00
Test3.cfg add check txn status, read key, read SI check (#37) 2021-08-22 22:06:49 +08:00
Test3.tla add check txn status, read key, read SI check (#37) 2021-08-22 22:06:49 +08:00
Test4.cfg add check txn status, read key, read SI check (#37) 2021-08-22 22:06:49 +08:00
Test4.tla add check txn status, read key, read SI check (#37) 2021-08-22 22:06:49 +08:00
Test5.cfg add check txn status, read key, read SI check (#37) 2021-08-22 22:06:49 +08:00
Test5.tla add check txn status, read key, read SI check (#37) 2021-08-22 22:06:49 +08:00

README.md

TLA+ for Distributed Transaction

The module contains a abstract specification of the transaction system implemented in TiKV. The server-side implementation can be found in TiKV Transaction Module.