github-repos/tla-plus
1
0
Fork 0
mirror of https://github.com/pingcap/tla-plus.git synced 2025-01-13 21:30:08 +08:00
Code Issues Packages Projects Releases Wiki Activity

percolator: Added README and TLC models. (#8)

Browse Source
This commit is contained in:
foreverbell 2018-02-06 17:51:28 +08:00 committed by Ian
parent 92b423e1ce
commit 29d92af688
5 changed files with 89 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Percolator/.gitignore vendored
View File

@ -1 +1,2 @@
Percolator.toolbox
Percolator.tlaps/
states/

10
Percolator/Percolator.cfg
View File

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

6
Percolator/Percolator.tla
View File

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

53
Percolator/Percolator.toolbox/Percolator___PercolatorModel.launch Normal file
View File

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

21
Percolator/README.md Normal file
View File

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