percolator: allow clients having different primary keys. (#16)

.gitignore

@@ -0,0 +1,6 @@
+states/
+
+**/*.toolbox/*/
+**/*.toolbox/*___*_SnapShot_*.launch
+**/*.toolbox/.project
+**/*.toolbox/.settings/

ConcurrentPercolator/ConcurrentPercolator.tla

@@ -9,6 +9,10 @@ ASSUME KEY # {} \* Keys cannot be empty.
 \* The set of clients to execute a transaction.
 CONSTANTS CLIENT
 
+\* Primary keys of all clients (transactions).
+CONSTANTS CLIENT_PRIMARY_KEY
+ASSUME CLIENT_PRIMARY_KEY \in [CLIENT -> KEY]
+
 \* $next_ts$ is the timestamp for transaction. It is increased monotonically,
 \* so every transaction must have a unique start and commit ts.
 VARIABLES next_ts
@@ -283,9 +287,9 @@ Next == \E c \in CLIENT : ClientOp(c)
 Init ==
   LET
     \* Selects a primary key and use the rest for the secondary keys.
-    chooseKey(ks) ==
+    chooseKey(ks, c) ==
     LET
-      primary == CHOOSE k \in ks : TRUE
+      primary == CLIENT_PRIMARY_KEY[c]
     IN
       [primary |-> primary,
        secondary |-> ks \ {primary},
@@ -294,7 +298,7 @@ Init ==
     /\ next_ts = 0
     /\ client_state = [c \in CLIENT |-> "init"]
     /\ client_ts = [c \in CLIENT |-> [start_ts |-> 0, commit_ts |-> 0]]
-    /\ client_key = [c \in CLIENT |-> chooseKey(KEY)]
+    /\ client_key = [c \in CLIENT |-> chooseKey(KEY, c)]
     /\ key_lock = [k \in KEY |-> {}]
     /\ key_data = [k \in KEY |-> {}]
     /\ key_write = [k \in KEY |-> <<>>]
@@ -439,10 +443,6 @@ SnapshotIsolation ==
   \A k \in KEY :
     key_si[k] = TRUE
 
---------------------------------------------------------------------------------
-\* Used for symmetry reduction in TLC.
-Symmetry == Permutations(CLIENT)
-
 --------------------------------------------------------------------------------
 THEOREM Safety ==
   PercolatorSpec => [](/\ TypeInvariant

ConcurrentPercolator/ConcurrentPercolator.toolbox/ConcurrentPercolator___Test1.launch

@@ -1,7 +1,7 @@
 <?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="ConcurrentPercolatorModel"/>
+<stringAttribute key="configurationName" value="Test1"/>
 <booleanAttribute key="deferLiveness" value="false"/>
 <intAttribute key="dfidDepth" value="100"/>
 <booleanAttribute key="dfidMode" value="false"/>
@@ -15,8 +15,8 @@
 <intAttribute key="maxHeapSize" value="25"/>
 <intAttribute key="maxSetSize" value="1000000"/>
 <booleanAttribute key="mcMode" value="true"/>
-<stringAttribute key="modelBehaviorInit" value="Init"/>
-<stringAttribute key="modelBehaviorNext" value="Next"/>
+<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"/>
@@ -38,6 +38,7 @@
 <listAttribute key="modelParameterConstants">
 <listEntry value="KEY;;{1, 2, 3};0;0"/>
 <listEntry value="CLIENT;;{c1, c2, c3};1;1"/>
+<listEntry value="CLIENT_PRIMARY_KEY;;c1 :&gt; 1 @@ c2 :&gt; 1 @@ c3 :&gt; 1;0;0"/>
 </listAttribute>
 <stringAttribute key="modelParameterContraint" value=""/>
 <listAttribute key="modelParameterDefinitions"/>

ConcurrentPercolator/ConcurrentPercolator.toolbox/ConcurrentPercolator___Test2.launch

@@ -0,0 +1,56 @@
+<?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="Test2"/>
+<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="1RollbackConsistency"/>
+<listEntry value="1UniqueWrite"/>
+<listEntry value="1SnapshotIsolation"/>
+</listAttribute>
+<listAttribute key="modelCorrectnessProperties"/>
+<stringAttribute key="modelExpressionEval" value=""/>
+<stringAttribute key="modelParameterActionConstraint" value=""/>
+<listAttribute key="modelParameterConstants">
+<listEntry value="KEY;;{1, 2};0;0"/>
+<listEntry value="CLIENT;;{c1, c2};1;0"/>
+<listEntry value="CLIENT_PRIMARY_KEY;;c1 :&gt; 1 @@ c2 :&gt; 2;0;0"/>
+</listAttribute>
+<stringAttribute key="modelParameterContraint" value=""/>
+<listAttribute key="modelParameterDefinitions"/>
+<stringAttribute key="modelParameterModelValues" value="{}"/>
+<stringAttribute key="modelParameterNewDefinitions" value=""/>
+<intAttribute key="numberOfWorkers" value="2"/>
+<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="ConcurrentPercolator"/>
+<stringAttribute key="view" value=""/>
+<booleanAttribute key="visualizeStateGraph" value="false"/>
+</launchConfiguration>

ConcurrentPercolator/Test1.cfg

@@ -1,9 +1,12 @@
-\* We use one table with 3 keys and 3 concurrent clients for TLC model checking.
-\* These 3 clients are considered symmetric.
+\* See Test1.tla.
 
 CONSTANT
-  KEY = {1, 2, 3}
-  CLIENT = {c1, c2, c3}
+  c1 = c1
+  c2 = c2
+  c3 = c3
+  KEY <- Key
+  CLIENT <- Client
+  CLIENT_PRIMARY_KEY <- ClientPrimaryKey
 
 SYMMETRY
   Symmetry

ConcurrentPercolator/Test1.tla

@@ -0,0 +1,16 @@
+--------------------------------- MODULE Test1 ---------------------------------
+
+EXTENDS Percolator, TLC
+
+\* We use one table with 3 keys and 3 concurrent clients for TLC model checking.
+\* These 3 clients have the same primary key, so they are considered symmetric.
+
+CONSTANTS c1, c2, c3
+
+Key == {1, 2, 3}
+Client == {c1, c2, c3}
+ClientPrimaryKey == c1 :> 1 @@ c2 :> 1 @@ c3 :> 1
+
+Symmetry == Permutations(Client)
+
+================================================================================

ConcurrentPercolator/Test2.cfg

@@ -0,0 +1,21 @@
+\* See Test2.tla.
+
+CONSTANT
+  c1 = c1
+  c2 = c2
+  KEY <- Key
+  CLIENT <- Client
+  CLIENT_PRIMARY_KEY <- ClientPrimaryKey
+
+SPECIFICATION
+  PercolatorSpec
+
+INVARIANT
+  TypeInvariant
+  WriteConsistency
+  LockConsistency
+  CommittedConsistency
+  AbortedConsistency
+  RollbackConsistency
+  UniqueWrite
+  SnapshotIsolation

ConcurrentPercolator/Test2.tla

@@ -0,0 +1,14 @@
+--------------------------------- MODULE Test2 ---------------------------------
+
+EXTENDS Percolator, TLC
+
+\* We use one table with 2 keys and 2 concurrent clients for TLC model checking.
+\* These 2 clients have primary key 1 and 2 respectively.
+
+CONSTANTS c1, c2
+
+Key == {1, 2}
+Client == {c1, c2}
+ClientPrimaryKey == c1 :> 1 @@ c2 :> 2
+
+================================================================================

Percolator/.gitignore

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

Percolator/Percolator.tla

@@ -9,6 +9,10 @@ ASSUME KEY # {} \* Keys cannot be empty.
 \* The set of clients to execute a transaction.
 CONSTANTS CLIENT
 
+\* Primary keys of all clients (transactions).
+CONSTANTS CLIENT_PRIMARY_KEY
+ASSUME CLIENT_PRIMARY_KEY \in [CLIENT -> KEY]
+
 \* $next_ts$ is the timestamp for transaction. It is increased monotonically,
 \* so every transaction must have a unique start and commit ts.
 VARIABLES next_ts
@@ -271,9 +275,9 @@ Next == \E c \in CLIENT : ClientOp(c)
 Init ==
   LET
     \* Selects a primary key and use the rest for the secondary keys.
-    chooseKey(ks) ==
+    chooseKey(ks, c) ==
     LET
-      primary == CHOOSE k \in ks : TRUE
+      primary == CLIENT_PRIMARY_KEY[c]
     IN
       [primary |-> primary,
        secondary |-> ks \ {primary},
@@ -282,7 +286,7 @@ Init ==
     /\ next_ts = 0
     /\ client_state = [c \in CLIENT |-> "init"]
     /\ client_ts = [c \in CLIENT |-> [start_ts |-> 0, commit_ts |-> 0]]
-    /\ client_key = [c \in CLIENT |-> chooseKey(KEY)]
+    /\ client_key = [c \in CLIENT |-> chooseKey(KEY, c)]
     /\ key_lock = [k \in KEY |-> {}]
     /\ key_data = [k \in KEY |-> {}]
     /\ key_write = [k \in KEY |-> <<>>]
@@ -399,10 +403,6 @@ SnapshotIsolation ==
   \A k \in KEY :
     key_si[k] = TRUE
 
---------------------------------------------------------------------------------
-\* Used for symmetry reduction in TLC.
-Symmetry == Permutations(CLIENT)
-
 --------------------------------------------------------------------------------
 THEOREM Safety ==
   PercolatorSpec => [](/\ TypeInvariant

Percolator/Percolator.toolbox/Percolator___Test1.launch

@@ -1,7 +1,7 @@
 <?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"/>
+<stringAttribute key="configurationName" value="Test1"/>
 <booleanAttribute key="deferLiveness" value="false"/>
 <intAttribute key="dfidDepth" value="100"/>
 <booleanAttribute key="dfidMode" value="false"/>
@@ -36,6 +36,7 @@
 <listAttribute key="modelParameterConstants">
 <listEntry value="KEY;;{1, 2, 3};0;0"/>
 <listEntry value="CLIENT;;{c1, c2, c3};1;1"/>
+<listEntry value="CLIENT_PRIMARY_KEY;;c1 :&gt; 1 @@ c2 :&gt; 1 @@ c3 :&gt; 1;0;0"/>
 </listAttribute>
 <stringAttribute key="modelParameterContraint" value=""/>
 <listAttribute key="modelParameterDefinitions"/>

Percolator/Percolator.toolbox/Percolator___Test2.launch

@@ -0,0 +1,54 @@
+<?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="Test2"/>
+<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};0;0"/>
+<listEntry value="CLIENT;;{c1, c2};1;0"/>
+<listEntry value="CLIENT_PRIMARY_KEY;;c1 :&gt; 1 @@ c2 :&gt; 2;0;0"/>
+</listAttribute>
+<stringAttribute key="modelParameterContraint" value=""/>
+<listAttribute key="modelParameterDefinitions"/>
+<stringAttribute key="modelParameterModelValues" value="{}"/>
+<stringAttribute key="modelParameterNewDefinitions" value=""/>
+<intAttribute key="numberOfWorkers" value="2"/>
+<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>

Percolator/Test1.cfg

@@ -1,9 +1,12 @@
-\* We use one table with 3 keys and 3 concurrent clients for TLC model checking.
-\* These 3 clients are considered symmetric.
+\* See Test1.tla.
 
 CONSTANT
-  KEY = {1, 2, 3}
-  CLIENT = {c1, c2, c3}
+  c1 = c1
+  c2 = c2
+  c3 = c3
+  KEY <- Key
+  CLIENT <- Client
+  CLIENT_PRIMARY_KEY <- ClientPrimaryKey
 
 SYMMETRY
   Symmetry

Percolator/Test1.tla

@@ -0,0 +1,16 @@
+--------------------------------- MODULE Test1 ---------------------------------
+
+EXTENDS Percolator, TLC
+
+\* We use one table with 3 keys and 3 concurrent clients for TLC model checking.
+\* These 3 clients have the same primary key, so they are considered symmetric.
+
+CONSTANTS c1, c2, c3
+
+Key == {1, 2, 3}
+Client == {c1, c2, c3}
+ClientPrimaryKey == c1 :> 1 @@ c2 :> 1 @@ c3 :> 1
+
+Symmetry == Permutations(Client)
+
+================================================================================

Percolator/Test2.cfg

@@ -0,0 +1,19 @@
+\* See Test2.tla.
+
+CONSTANT
+  c1 = c1
+  c2 = c2
+  KEY <- Key
+  CLIENT <- Client
+  CLIENT_PRIMARY_KEY <- ClientPrimaryKey
+
+SPECIFICATION
+  PercolatorSpec
+
+INVARIANT
+  TypeInvariant
+  WriteConsistency
+  LockConsistency
+  CommittedConsistency
+  AbortedConsistency
+  SnapshotIsolation

Percolator/Test2.tla

@@ -0,0 +1,14 @@
+--------------------------------- MODULE Test2 ---------------------------------
+
+EXTENDS Percolator, TLC
+
+\* We use one table with 2 keys and 2 concurrent clients for TLC model checking.
+\* These 2 clients have primary key 1 and 2 respectively.
+
+CONSTANTS c1, c2
+
+Key == {1, 2}
+Client == {c1, c2}
+ClientPrimaryKey == c1 :> 1 @@ c2 :> 2
+
+================================================================================