pingcap/tla-plus issues and pull requests

#45 - Add DM safe mode replication

Pull Request - State: open - Opened by lance6716 about 1 month ago - 1 comment

#44 - added WriteAndVerify committing

Pull Request - State: open - Opened by YuJuncen about 1 month ago - 2 comments

#43 - Specialized tla+ for RaftRs

Pull Request - State: open - Opened by wego1236 8 months ago - 12 comments

#42 - Quint spec for large transaction

Pull Request - State: open - Opened by ekexium 11 months ago

#41 - add RaftEngineHedge tla module

Pull Request - State: open - Opened by tonyxuqqi about 1 year ago

#40 - TLC throw an error while verifying Raft TLA+ spec

Issue - State: open - Opened by kikimo almost 2 years ago

#39 - [Question] Does TiKV has/follow a TLA+ Spec for Raft membership change?

Issue - State: open - Opened by kikimo almost 2 years ago

#38 - Add async commit check

Pull Request - State: open - Opened by zhuo1angT about 3 years ago

#37 - add check txn status, read key, read SI check

Pull Request - State: closed - Opened by zhuo1angT over 3 years ago - 3 comments

#36 - Add CheckTxnStatus

Pull Request - State: closed - Opened by zhuo1angT over 3 years ago - 3 comments

#35 - Add ResolvePessimisticLock

Pull Request - State: closed - Opened by zhuo1angT over 3 years ago - 1 comment

#34 - fix typo: transaction tla

Pull Request - State: closed - Opened by zhuo1angT over 3 years ago - 1 comment

#33 - DistributedTransaction: rewrite monotonicity formulas to check SnapshotIsolation

Pull Request - State: closed - Opened by ekexium about 4 years ago - 3 comments

#32 - Only write rollback record on primary keys

Pull Request - State: closed - Opened by andylokandy over 4 years ago

#31 - `Raft.pla` doesn't seem to cover all exceptions?

Issue - State: open - Opened by Yriuns over 4 years ago

#30 - Add a refined spec for distributed transaction

Pull Request - State: closed - Opened by andylokandy over 4 years ago

#29 - spec for optimistic/pessimistic mixed transaction

Pull Request - State: closed - Opened by sticnarf about 5 years ago - 3 comments

#28 - Transaction specs may be not as solid as expected

Issue - State: open - Opened by sticnarf about 5 years ago - 2 comments

#27 - Add ResolvedTS spec

Pull Request - State: closed - Opened by overvenus about 5 years ago

#26 - spec for joint consensus

Pull Request - State: open - Opened by nolouch about 6 years ago - 1 comment

#25 - Cluster membership changes

Pull Request - State: closed - Opened by nolouch about 6 years ago - 1 comment

#24 - collapserollback: move collapserollback optimization to a separate directory

Pull Request - State: closed - Opened by cwen0 about 6 years ago - 2 comments

#23 - ConcurrentPercolator: remove the pre rollback

Pull Request - State: closed - Opened by cwen0 over 6 years ago - 6 comments

#22 - Update the format

Pull Request - State: closed - Opened by QueenyJin over 6 years ago - 1 comment

#21 - Add readme file to the repo

Pull Request - State: closed - Opened by QueenyJin over 6 years ago - 1 comment

#20 - optimized commit ts: remove the cost of getting commitTS

Pull Request - State: closed - Opened by alivxxx over 6 years ago - 9 comments

#19 - OptimizedCommitTS: fork from concurrent percolator

Pull Request - State: closed - Opened by alivxxx over 6 years ago - 3 comments

#18 - concurrent_percolator: remove the cost of getting commitTS

Pull Request - State: closed - Opened by alivxxx over 6 years ago - 1 comment

#17 - concurrent percolator: fix a copy-then-paste error.

Pull Request - State: closed - Opened by foreverbell over 6 years ago

#16 - percolator: allow clients having different primary keys.

Pull Request - State: closed - Opened by foreverbell over 6 years ago - 1 comment

#15 - concurrent percolator: implementation.

Pull Request - State: closed - Opened by foreverbell over 6 years ago - 6 comments

#14 - concurrent percolator: fork from percolator.

Pull Request - State: closed - Opened by foreverbell over 6 years ago - 1 comment

#13 - percolator: refactor variables key_* to emphasize the timestamp dimension.

Pull Request - State: closed - Opened by foreverbell over 6 years ago - 5 comments

#12 - Percolator: remove TLAPS proof

Pull Request - State: closed - Opened by foreverbell over 6 years ago - 2 comments

#11 - RaftMerge: rollback and TLC models.

Pull Request - State: closed - Opened by foreverbell over 6 years ago - 2 comments

#10 - RaftMerge: body part of multi-raft region merge protocol except rollback.

Pull Request - State: closed - Opened by foreverbell over 6 years ago - 5 comments

#9 - RaftMerge: implement a simplified raft model.

Pull Request - State: closed - Opened by foreverbell over 6 years ago - 1 comment

#8 - percolator: Added README and TLC models.

Pull Request - State: closed - Opened by foreverbell almost 7 years ago - 4 comments

#7 - percolator: all writes of one key cannot overlap

Pull Request - State: closed - Opened by foreverbell almost 7 years ago - 2 comments

#6 - percolator: verify snapshot isolation property.

Pull Request - State: closed - Opened by foreverbell almost 7 years ago - 4 comments

#5 - percolator: Remove canGoCommit and canGoPrewrite.

Pull Request - State: closed - Opened by foreverbell almost 7 years ago - 4 comments

#4 - Remove canGoCommit and canGoPrewrite.

Pull Request - State: closed - Opened by foreverbell almost 7 years ago - 1 comment

#3 - raft: Port raft from ongardie/raft.tla as-is.

Pull Request - State: closed - Opened by foreverbell almost 7 years ago - 3 comments

#2 - TLA+ formalization of Percolator.

Pull Request - State: closed - Opened by foreverbell almost 7 years ago - 6 comments

#1 - TLAPS and Coq proof of TwoPC protocol.

Pull Request - State: closed - Opened by foreverbell almost 7 years ago - 1 comment

GitHub / pingcap/tla-plus issues and pull requests