From 6307a6109732565867cde2d4e603b83911e22b7b Mon Sep 17 00:00:00 2001 From: ekexium Date: Wed, 28 Oct 2020 10:20:02 +0800 Subject: [PATCH] DistributedTransaction: rewrite monotonicity formulas to check SnapshotIsolation (#33) * DistributedTransaction: rewrite monotonicity formulas Signed-off-by: ekexium * DistributedTransaction: check SnapshotIsolation Signed-off-by: ekexium * delete proof Signed-off-by: ekexium --- .../DistributedTransaction.tla | 10 ++-- .../DistributedTransaction___Test1.launch | 31 +++++++++--- .../DistributedTransactionProofs.tla | 47 ------------------- DistributedTransaction/README.md | 8 +--- 4 files changed, 29 insertions(+), 67 deletions(-) delete mode 100644 DistributedTransaction/DistributedTransactionProofs.tla diff --git a/DistributedTransaction/DistributedTransaction.tla b/DistributedTransaction/DistributedTransaction.tla index d008e4c..317eadd 100644 --- a/DistributedTransaction/DistributedTransaction.tla +++ b/DistributedTransaction/DistributedTransaction.tla @@ -547,16 +547,12 @@ UniqueWrite == \* Snapshot Isolation \* Asserts that next_ts is monotonically increasing. -NextTsMonotonicity == - \A ts \in Ts : - (ts <= next_ts) => [](ts <= next_ts) +NextTsMonotonicity == [][next_ts' >= next_ts]_vars \* Asserts that no msg would be deleted once sent. MsgMonotonicity == - /\ \A req \in ReqMessages : - req \in req_msgs => [](req \in req_msgs) - /\ \A resp \in RespMessages : - resp \in resp_msgs => [](resp \in resp_msgs) + /\ [][\A req \in req_msgs : req \in req_msgs']_vars + /\ [][\A resp \in resp_msgs : resp \in resp_msgs']_vars \* Asserts that all messages sent should have ts less than next_ts. MsgTsConsistency == diff --git a/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test1.launch b/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test1.launch index acb55a8..aec9d79 100644 --- a/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test1.launch +++ b/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test1.launch @@ -1,12 +1,22 @@ + + + + + - + - - + + + + + + + @@ -24,8 +34,11 @@ - - + + + + + @@ -35,7 +48,13 @@ + + + + - + + + diff --git a/DistributedTransaction/DistributedTransactionProofs.tla b/DistributedTransaction/DistributedTransactionProofs.tla deleted file mode 100644 index 0a1b1af..0000000 --- a/DistributedTransaction/DistributedTransactionProofs.tla +++ /dev/null @@ -1,47 +0,0 @@ ---------------------- MODULE DistributedTransactionProofs ------------------- -EXTENDS DistributedTransaction, TLAPS - -THEOREM SpecTypeOK == Spec => TypeOK - PROOF OMITTED - -LEMMA NextInv == - Next => - /\ next_ts' = next_ts + 1 \/ UNCHANGED next_ts - /\ \E reqs : SendReqs(reqs) \/ UNCHANGED req_msgs - /\ \E resp : SendResp(resp) \/ UNCHANGED resp_msgs - BY DEF Next, vars, msg_vars, - ClientPrewriteOptimisistic, ClientPrewrited, ClientCommit, ClientLockKey, - ClientLockedKey, ClientRetryLockKey, ClientPrewritePessimistic, - ClientPrewrited, ClientCommit, ServerLockKey, ServerPrewritePessimistic, - ServerPrewriteOptimistic, ServerCommit, ServerCleanupStaleLock, - ServerCleanup, ServerResolveCommitted, ServerResolveRollbacked - -LEMMA SpecNextTsMonotonicity == Spec => NextTsMonotonicity - <1> SUFFICES ASSUME NEW ts \in Ts, TypeOK - PROVE (ts <= next_ts) /\ [][Next]_vars => [](ts <= next_ts) - BY SpecTypeOK DEF NextTsMonotonicity, Spec - <1>2. (ts <= next_ts) /\ [Next]_vars => (ts <= next_ts)' - BY NextInv DEF TypeOK, Ts, vars - <1>3. QED - BY <1>2, PTL - -LEMMA SpecMsgMonotonicity == Spec => MsgMonotonicity - <1>1. ASSUME NEW req \in ReqMessages - PROVE req \in req_msgs /\ [][Next]_vars => [](req \in req_msgs) - <2>1. req \in req_msgs /\ (\E reqs : SendReqs(reqs)) => (req \in req_msgs)' - BY DEF SendReqs - <2>2. req \in req_msgs /\ [Next]_vars => (req \in req_msgs)' - BY <2>1, NextInv DEF vars, msg_vars - <2>3. QED - BY <2>2, PTL - <1>2. ASSUME NEW resp \in RespMessages - PROVE resp \in resp_msgs /\ [][Next]_vars => [](resp \in resp_msgs) - <3>1. resp \in resp_msgs /\ (\E resp2 : SendResp(resp2)) => (resp \in resp_msgs)' - BY DEF SendResp - <3>2. resp \in resp_msgs /\ [Next]_vars => (resp \in resp_msgs)' - BY <3>1, NextInv DEF vars, msg_vars - <3>3. QED - BY <3>2, PTL - <1>3. QED - BY <1>1, <1>2, SpecTypeOK DEF MsgMonotonicity, Spec -============================================================================= diff --git a/DistributedTransaction/README.md b/DistributedTransaction/README.md index 1d4a4b4..5becb85 100644 --- a/DistributedTransaction/README.md +++ b/DistributedTransaction/README.md @@ -1,9 +1,3 @@ # TLA+ for Distributed Transaction -The module contains a abstract specification of the transaction system implemented in TiKV. The implementation can be found in [TiKV Transaction Module](https://github.com/tikv/tikv/blob/master/src/storage/mvcc/txn.rs). - -The module contains two TLA+ files: `DistributedTransaction.tla` and `DistributedTransactionProofs.tla`. - -In most cases you will likely have an interest in only `DistributedTransaction.tla`, where the specification and safety invariants are defined. Besides that, in `DistributedTransactionProofs.tla`, there are some formal proofs, which are supposed to be build up gradually (so it's not completed yet), to the safety invariants. - -To run the formal proofs in `DistributedTransactionProofs.tla`, you'd like to install the [TLAPS](https://tla.msr-inria.inria.fr/tlaps/content/Download/Binaries.html) (TLA+ Proof System) first. It's not distributed altogether with the TLA toolbox. +The module contains a abstract specification of the transaction system implemented in TiKV. The server-side implementation can be found in [TiKV Transaction Module](https://github.com/tikv/tikv/tree/master/src/storage/txn).