diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..3fc9e3a --- /dev/null +++ b/.gitignore @@ -0,0 +1,6 @@ +states/ + +**/*.toolbox/*/ +**/*.toolbox/*___*_SnapShot_*.launch +**/*.toolbox/.project +**/*.toolbox/.settings/ diff --git a/Percolator/Concurrent/ConcurrentPercolator.tla b/ConcurrentPercolator/ConcurrentPercolator.tla similarity index 98% rename from Percolator/Concurrent/ConcurrentPercolator.tla rename to ConcurrentPercolator/ConcurrentPercolator.tla index 4fc6768..1b78aa9 100644 --- a/Percolator/Concurrent/ConcurrentPercolator.tla +++ b/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 diff --git a/Percolator/Concurrent/ConcurrentPercolator.toolbox/ConcurrentPercolator___ConcurrentPercolatorModel.launch b/ConcurrentPercolator/ConcurrentPercolator.toolbox/ConcurrentPercolator___Test1.launch similarity index 91% rename from Percolator/Concurrent/ConcurrentPercolator.toolbox/ConcurrentPercolator___ConcurrentPercolatorModel.launch rename to ConcurrentPercolator/ConcurrentPercolator.toolbox/ConcurrentPercolator___Test1.launch index 0721fee..66db6e4 100644 --- a/Percolator/Concurrent/ConcurrentPercolator.toolbox/ConcurrentPercolator___ConcurrentPercolatorModel.launch +++ b/ConcurrentPercolator/ConcurrentPercolator.toolbox/ConcurrentPercolator___Test1.launch @@ -1,7 +1,7 @@ - + @@ -15,8 +15,8 @@ - - + + @@ -38,6 +38,7 @@ + diff --git a/ConcurrentPercolator/ConcurrentPercolator.toolbox/ConcurrentPercolator___Test2.launch b/ConcurrentPercolator/ConcurrentPercolator.toolbox/ConcurrentPercolator___Test2.launch new file mode 100644 index 0000000..2124059 --- /dev/null +++ b/ConcurrentPercolator/ConcurrentPercolator.toolbox/ConcurrentPercolator___Test2.launch @@ -0,0 +1,56 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Percolator/Concurrent/ConcurrentPercolator.cfg b/ConcurrentPercolator/Test1.cfg similarity index 57% rename from Percolator/Concurrent/ConcurrentPercolator.cfg rename to ConcurrentPercolator/Test1.cfg index 8fe03ad..9fa8fa1 100644 --- a/Percolator/Concurrent/ConcurrentPercolator.cfg +++ b/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 diff --git a/ConcurrentPercolator/Test1.tla b/ConcurrentPercolator/Test1.tla new file mode 100644 index 0000000..3f8e7ab --- /dev/null +++ b/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) + +================================================================================ diff --git a/ConcurrentPercolator/Test2.cfg b/ConcurrentPercolator/Test2.cfg new file mode 100644 index 0000000..798dc43 --- /dev/null +++ b/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 diff --git a/ConcurrentPercolator/Test2.tla b/ConcurrentPercolator/Test2.tla new file mode 100644 index 0000000..944a649 --- /dev/null +++ b/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 + +================================================================================ diff --git a/Percolator/.gitignore b/Percolator/.gitignore deleted file mode 100644 index 9149158..0000000 --- a/Percolator/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -Percolator.tlaps/ -states/ diff --git a/Percolator/Percolator.tla b/Percolator/Percolator.tla index bdaec07..9e21a75 100644 --- a/Percolator/Percolator.tla +++ b/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 diff --git a/Percolator/Percolator.toolbox/Percolator___PercolatorModel.launch b/Percolator/Percolator.toolbox/Percolator___Test1.launch similarity index 94% rename from Percolator/Percolator.toolbox/Percolator___PercolatorModel.launch rename to Percolator/Percolator.toolbox/Percolator___Test1.launch index 7c93281..a9b1412 100644 --- a/Percolator/Percolator.toolbox/Percolator___PercolatorModel.launch +++ b/Percolator/Percolator.toolbox/Percolator___Test1.launch @@ -1,7 +1,7 @@ - + @@ -36,6 +36,7 @@ + diff --git a/Percolator/Percolator.toolbox/Percolator___Test2.launch b/Percolator/Percolator.toolbox/Percolator___Test2.launch new file mode 100644 index 0000000..2d47633 --- /dev/null +++ b/Percolator/Percolator.toolbox/Percolator___Test2.launch @@ -0,0 +1,54 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/Percolator/Percolator.cfg b/Percolator/Test1.cfg similarity index 53% rename from Percolator/Percolator.cfg rename to Percolator/Test1.cfg index e13d0a2..2e0aabd 100644 --- a/Percolator/Percolator.cfg +++ b/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 diff --git a/Percolator/Test1.tla b/Percolator/Test1.tla new file mode 100644 index 0000000..3f8e7ab --- /dev/null +++ b/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) + +================================================================================ diff --git a/Percolator/Test2.cfg b/Percolator/Test2.cfg new file mode 100644 index 0000000..86be2b1 --- /dev/null +++ b/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 diff --git a/Percolator/Test2.tla b/Percolator/Test2.tla new file mode 100644 index 0000000..944a649 --- /dev/null +++ b/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 + +================================================================================