DistributedTransaction: rewrite monotonicity formulas to check SnapshotIsolation (#33)

* DistributedTransaction: rewrite monotonicity formulas

Signed-off-by: ekexium <ekexium@gmail.com>

* DistributedTransaction: check SnapshotIsolation

Signed-off-by: ekexium <ekexium@gmail.com>

* delete proof

Signed-off-by: ekexium <ekexium@gmail.com>

DistributedTransaction/DistributedTransaction.tla

@@ -547,16 +547,12 @@ UniqueWrite ==
 \* Snapshot Isolation
 
 \* Asserts that next_ts is monotonically increasing.
-NextTsMonotonicity == 
+NextTsMonotonicity == [][next_ts' >= next_ts]_vars
-  \A ts \in Ts :
-    (ts <= next_ts) => [](ts <= next_ts)
 
 \* Asserts that no msg would be deleted once sent.
 MsgMonotonicity ==
-  /\ \A req \in ReqMessages :
+  /\ [][\A req \in req_msgs : req \in req_msgs']_vars
-      req \in req_msgs => [](req \in req_msgs)
+  /\ [][\A resp \in resp_msgs : resp \in resp_msgs']_vars
-  /\ \A resp \in RespMessages :
-      resp \in resp_msgs => [](resp \in resp_msgs)
 
 \* Asserts that all messages sent should have ts less than next_ts.
 MsgTsConsistency ==

DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test1.launch

@@ -1,12 +1,22 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
+    <stringAttribute key="TLCCmdLineParameters" value=""/>
+    <intAttribute key="collectCoverage" value="1"/>
     <stringAttribute key="configurationName" value="Test1"/>
+    <booleanAttribute key="deferLiveness" value="false"/>
+    <intAttribute key="dfidDepth" value="100"/>
+    <booleanAttribute key="dfidMode" value="false"/>
     <intAttribute key="distributedFPSetCount" value="0"/>
-    <stringAttribute key="distributedNetworkInterface" value="10.0.75.1"/>
+    <stringAttribute key="distributedNetworkInterface" value="192.168.224.64"/>
     <intAttribute key="distributedNodesCount" value="1"/>
     <stringAttribute key="distributedTLC" value="off"/>
-    <intAttribute key="fpIndex" value="8"/>
+    <stringAttribute key="distributedTLCVMArgs" value=""/>
-    <intAttribute key="maxHeapSize" value="25"/>
+    <intAttribute key="fpBits" value="1"/>
+    <intAttribute key="fpIndex" value="41"/>
+    <booleanAttribute key="fpIndexRandom" value="true"/>
+    <intAttribute key="maxHeapSize" value="40"/>
+    <intAttribute key="maxSetSize" value="1000000"/>
+    <booleanAttribute key="mcMode" value="true"/>
     <stringAttribute key="modelBehaviorInit" value=""/>
     <stringAttribute key="modelBehaviorNext" value=""/>
     <stringAttribute key="modelBehaviorSpec" value="Spec"/>
@@ -24,8 +34,11 @@
         <listEntry value="1UniqueWrite"/>
         <listEntry value="1MsgTsConsistency"/>
     </listAttribute>
-    <listAttribute key="modelCorrectnessProperties"/>
+    <listAttribute key="modelCorrectnessProperties">
-    <intAttribute key="modelEditorOpenTabs" value="8"/>
+        <listEntry value="1SnapshotIsolation"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="12"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
     <listAttribute key="modelParameterConstants">
         <listEntry value="KEY;;{k1, k2};1;0"/>
         <listEntry value="CLIENT_KEY;;c1 :&gt; {k1, k2} @@ c2 :&gt; {k1} @@ c3 :&gt; {k1, k2};0;0"/>
@@ -35,7 +48,13 @@
     </listAttribute>
     <intAttribute key="modelVersion" value="20191005"/>
     <intAttribute key="numberOfWorkers" value="6"/>
+    <booleanAttribute key="recover" value="false"/>
     <stringAttribute key="result.mail.address" value=""/>
+    <intAttribute key="simuAril" value="-1"/>
+    <intAttribute key="simuDepth" value="100"/>
+    <intAttribute key="simuSeed" value="-1"/>
     <stringAttribute key="specName" value="DistributedTransaction"/>
-    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="tlcResourcesProfile" value="local nomal"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="false"/>
 </launchConfiguration>

DistributedTransaction/DistributedTransactionProofs.tla

@@ -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
-=============================================================================

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 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).
-
-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.