From 29d92af6889161b0c1b9e02bde973beb7c85ffd2 Mon Sep 17 00:00:00 2001
From: foreverbell <dql.foreverbell@gmail.com>
Date: Tue, 6 Feb 2018 17:51:28 +0800
Subject: [PATCH] percolator: Added README and TLC models. (#8)

---
 Percolator/.gitignore                         |  3 +-
 Percolator/Percolator.cfg                     | 10 +++-
 Percolator/Percolator.tla                     |  6 ++-
 .../Percolator___PercolatorModel.launch       | 53 +++++++++++++++++++
 Percolator/README.md                          | 21 ++++++++
 5 files changed, 89 insertions(+), 4 deletions(-)
 create mode 100644 Percolator/Percolator.toolbox/Percolator___PercolatorModel.launch
 create mode 100644 Percolator/README.md

diff --git a/Percolator/.gitignore b/Percolator/.gitignore
index bac7420..9149158 100644
--- a/Percolator/.gitignore
+++ b/Percolator/.gitignore
@@ -1 +1,2 @@
-Percolator.toolbox
+Percolator.tlaps/
+states/
diff --git a/Percolator/Percolator.cfg b/Percolator/Percolator.cfg
index 0efe917..e13d0a2 100644
--- a/Percolator/Percolator.cfg
+++ b/Percolator/Percolator.cfg
@@ -1,6 +1,12 @@
+\* We use one table with 3 keys and 3 concurrent clients for TLC model checking.
+\* These 3 clients are considered symmetric.
+
 CONSTANT
-  KEY <- 1..3
-  CLIENT <- {"C1", "C2", "C3"}
+  KEY = {1, 2, 3}
+  CLIENT = {c1, c2, c3}
+
+SYMMETRY
+  Symmetry
 
 SPECIFICATION
   PercolatorSpec
diff --git a/Percolator/Percolator.tla b/Percolator/Percolator.tla
index a68ea88..e07553d 100644
--- a/Percolator/Percolator.tla
+++ b/Percolator/Percolator.tla
@@ -1,6 +1,6 @@
 ------------------------------- MODULE Percolator ------------------------------
 
-EXTENDS Integers, FiniteSets, Sequences, TLAPS
+EXTENDS Integers, FiniteSets, Sequences, TLAPS, TLC
 
 \* The set of transaction keys.
 CONSTANTS KEY
@@ -391,6 +391,10 @@ SnapshotIsolation ==
   \A k \in KEY :
     key_si[k] = TRUE
 
+--------------------------------------------------------------------------------
+\* Used for symmetry reduction with TLC.
+Symmetry == Permutations(CLIENT)
+
 --------------------------------------------------------------------------------
 \* TLAPS proof for proving Spec keeps type invariant.
 LEMMA InitStateSatisfiesTypeInvariant ==
diff --git a/Percolator/Percolator.toolbox/Percolator___PercolatorModel.launch b/Percolator/Percolator.toolbox/Percolator___PercolatorModel.launch
new file mode 100644
index 0000000..7c93281
--- /dev/null
+++ b/Percolator/Percolator.toolbox/Percolator___PercolatorModel.launch
@@ -0,0 +1,53 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
+<stringAttribute key="TLCCmdLineParameters" value=""/>
+<stringAttribute key="configurationName" value="PercolatorModel"/>
+<booleanAttribute key="deferLiveness" value="false"/>
+<intAttribute key="dfidDepth" value="100"/>
+<booleanAttribute key="dfidMode" value="false"/>
+<intAttribute key="distributedFPSetCount" value="0"/>
+<stringAttribute key="distributedNetworkInterface" value="172.17.0.1"/>
+<intAttribute key="distributedNodesCount" value="1"/>
+<stringAttribute key="distributedTLC" value="off"/>
+<stringAttribute key="distributedTLCVMArgs" value=""/>
+<intAttribute key="fpBits" value="1"/>
+<intAttribute key="fpIndex" value="1"/>
+<intAttribute key="maxHeapSize" value="25"/>
+<intAttribute key="maxSetSize" value="1000000"/>
+<booleanAttribute key="mcMode" value="true"/>
+<stringAttribute key="modelBehaviorInit" value=""/>
+<stringAttribute key="modelBehaviorNext" value=""/>
+<stringAttribute key="modelBehaviorSpec" value="PercolatorSpec"/>
+<intAttribute key="modelBehaviorSpecType" value="1"/>
+<stringAttribute key="modelBehaviorVars" value="key_data, key_lock, next_ts, client_state, key_last_read_ts, client_key, client_ts, key_si, key_write"/>
+<stringAttribute key="modelComments" value=""/>
+<booleanAttribute key="modelCorrectnessCheckDeadlock" value="false"/>
+<listAttribute key="modelCorrectnessInvariants">
+<listEntry value="1TypeInvariant"/>
+<listEntry value="1WriteConsistency"/>
+<listEntry value="1LockConsistency"/>
+<listEntry value="1CommittedConsistency"/>
+<listEntry value="1AbortedConsistency"/>
+<listEntry value="1SnapshotIsolation"/>
+</listAttribute>
+<listAttribute key="modelCorrectnessProperties"/>
+<stringAttribute key="modelExpressionEval" value=""/>
+<stringAttribute key="modelParameterActionConstraint" value=""/>
+<listAttribute key="modelParameterConstants">
+<listEntry value="KEY;;{1, 2, 3};0;0"/>
+<listEntry value="CLIENT;;{c1, c2, c3};1;1"/>
+</listAttribute>
+<stringAttribute key="modelParameterContraint" value=""/>
+<listAttribute key="modelParameterDefinitions"/>
+<stringAttribute key="modelParameterModelValues" value="{}"/>
+<stringAttribute key="modelParameterNewDefinitions" value=""/>
+<intAttribute key="numberOfWorkers" value="4"/>
+<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="Percolator"/>
+<stringAttribute key="view" value=""/>
+<booleanAttribute key="visualizeStateGraph" value="false"/>
+</launchConfiguration>
diff --git a/Percolator/README.md b/Percolator/README.md
new file mode 100644
index 0000000..5011ae7
--- /dev/null
+++ b/Percolator/README.md
@@ -0,0 +1,21 @@
+# TLA+ for Percolator
+
+This directory contains the TLA+ specification of Percolator, the transaction protocol of [TiKV](https://github.com/pingcap/tikv).
+
+- [TLA+ specification](Percolator.tla)
+- [TLC configuration](Percolator.cfg)
+- [TLA+ toolbox configuration](Percolator.toolbox/Percolator___PercolatorModel.launch) 
+
+## How to run in TLA+ toolbox?
+
+- Install [TLA+ toolbox](https://lamport.azurewebsites.net/tla/toolbox.html#installing).
+- Install [TLAPS](https://tla.msr-inria.inria.fr/tlaps/content/Download/Binaries.html).
+- Import the TLA+ toolbox configuration.
+
+Note TLAPS is optional. You can remove all TLAPS proof, it does not affect the model.
+
+## How to run in command line?
+
+- Download [tla2tools.jar](https://tla.msr-inria.inria.fr/tlatoolbox/dist/tla2tools.jar).
+- Install [TLAPS](https://tla.msr-inria.inria.fr/tlaps/content/Download/Binaries.html).
+- Execute `java -cp ./tla2tools.jar tlc2.TLC -deadlock -workers 4 Percolator`. `-worker 4` sets the number of worker threads, which should equal to the number of cores on machine.