tla/storage: initial implementation [doubled buckets problem investigation]

.gitignore

@@ -21,3 +21,7 @@ build
 .rocks
 build.luarocks
 .DS_Store
+
+# TLA+ files
+states/
+*_TTrace_*

proofs/tla/src/utils.tla

@@ -0,0 +1,10 @@
+------------------------------- MODULE utils -----------------------------------
+
+EXTENDS Naturals, FiniteSets
+
+RECURSIVE SetSum(_)
+SetSum(set) == IF set = {} THEN 0 ELSE
+  LET x == CHOOSE x \in set: TRUE
+    IN x + SetSum(set \ {x})
+
+================================================================================

proofs/tla/test/storage/DoubledBigTest.cfg

@@ -0,0 +1,27 @@
+INIT Init
+NEXT Next
+
+CONSTANTS
+    Storages <- StoragesC
+    ReplicaSets <- ReplicaSetsC
+    BucketIds <- BucketIdsC
+    StorageAssignments <- StorageAssignmentsC
+    BucketAssignments <- BucketAssignmentsC
+    MasterAssignments <- MasterAssignmentsC
+    b1 = b1
+    b2 = b2
+    b3 = b3
+    b4 = b4
+
+SYMMETRY Symmetry
+
+INVARIANTS
+    NetworkTypeInv
+    StorageTypeInv
+    StorageToReplicasetTypeInv
+    NoActiveSimultaneousInv
+
+CONSTRAINT
+    SendLimitConstraint
+    NetworkBoundConstraint
+    RefConstraint

proofs/tla/test/storage/DoubledBigTest.tla

@@ -0,0 +1,70 @@
+--------------------------- MODULE DoubledBigTest ------------------------------
+EXTENDS storage, utils
+
+CONSTANTS b1, b2, b3, b4
+
+StoragesC == {"s1", "s2", "s3", "s4"}
+ReplicaSetsC == {"rs1", "rs2", "rs3"}
+BucketIdsC == {b1, b2, b3, b4}
+StorageAssignmentsC == [rs1 |-> {"s1", "s2"},
+                       rs2 |-> {"s3"},
+                       rs3 |-> {"s4"}]
+BucketAssignmentsC == [rs1 |-> {b1},
+                       rs2 |-> {b2},
+                       rs3 |-> {b3, b4}]
+MasterAssignmentsC == [rs1 |-> {"s1"},
+                       rs2 |-> {"s3"},
+                       rs3 |-> {"s4"}]
+
+(***************************************************************************)
+(*                           CONSTRAINTS                                   *)
+(***************************************************************************)
+
+MAX_TOTAL_SENDS == 3
+
+\* 1. Limit total bucket sends - prevent endless transfers.
+SendLimitConstraint ==
+    LET totalSends ==
+        SetSum({ storages[i].errinj.bucketSendCount : i \in StoragesC })
+    IN totalSends =< MAX_TOTAL_SENDS
+
+\* 2. Keep network bounded - avoid message explosion.
+NetworkBoundConstraint ==
+    /\ \A s1, s2 \in StoragesC :
+            Len(network[s1][s2]) =< 3
+    /\ \A s \in StoragesC :
+        /\ storages[s].errinj.networkReorderCount <= 2
+        /\ storages[s].errinj.networkDropCount <= 2
+
+RefConstraint ==
+    \A s1 \in StoragesC :
+        /\ storages[s1].errinj.bucketRWRefCount <= 2
+        /\ storages[s1].errinj.bucketRORefCount <= 2
+        /\ storages[s1].errinj.bucketRWUnRefCount <= 2
+        /\ storages[s1].errinj.bucketROUnRefCount <= 2
+
+(***************************************************************************)
+(*                            SYMMETRY                                     *)
+(***************************************************************************)
+
+Symmetry ==
+    Permutations(BucketIdsC)
+
+(***************************************************************************)
+(*                           STATE INVARIANTS                              *)
+(***************************************************************************)
+
+NoActiveSimultaneousInv ==
+    \* No bucket can be ACTIVE in storages belonging to different ReplicaSets
+    \A b \in BucketIds :
+        \A rs1, rs2 \in ReplicaSets :
+            rs1 # rs2 =>
+                ~(\E s1, s2 \in Storages :
+                     storageToReplicaset[s1] = rs1 /\
+                     storageToReplicaset[s2] = rs2 /\
+                     storages[s1].status = "master" /\
+                     storages[s2].status = "master" /\
+                     storages[s1].buckets[b].status = "ACTIVE" /\
+                     storages[s2].buckets[b].status = "ACTIVE")
+
+================================================================================

proofs/tla/test/storage/DoubledBucketsSmallTest.cfg

@@ -0,0 +1,25 @@
+INIT Init
+NEXT Next
+
+CONSTANTS
+    Storages <- StoragesC
+    ReplicaSets <- ReplicaSetsC
+    BucketIds <- BucketIdsC
+    StorageAssignments <- StorageAssignmentsC
+    BucketAssignments <- BucketAssignmentsC
+    MasterAssignments <- MasterAssignmentsC
+    b1 = b1
+    b2 = b2
+
+SYMMETRY Symmetry
+
+INVARIANTS
+    NetworkTypeInv
+    StorageTypeInv
+    StorageToReplicasetTypeInv
+    NoActiveSimultaneousInv
+
+CONSTRAINTS
+    SendLimitConstraint
+    NetworkBoundConstraint
+    TwoMastersConstraint

proofs/tla/test/storage/DoubledBucketsSmallTest.tla

@@ -0,0 +1,61 @@
+-------------------------MODULE DoubledBucketsSmallTest ------------------------
+EXTENDS storage, utils
+
+CONSTANTS b1, b2
+
+StoragesC == {"s1", "s2", "s3", "s4"}
+ReplicaSetsC == {"rs1", "rs2"}
+BucketIdsC == {b1, b2}
+StorageAssignmentsC == [rs1 |-> {"s1", "s2"},
+                       rs2 |-> {"s3", "s4"}]
+BucketAssignmentsC == [rs1 |-> {b1},
+                       rs2 |-> {b2}]
+MasterAssignmentsC == [rs1 |-> {"s1"},
+                       rs2 |-> {"s3"}]
+
+(***************************************************************************)
+(*                           CONSTRAINTS                                   *)
+(***************************************************************************)
+
+MAX_TOTAL_SENDS == 1
+
+\* 1. Limit total bucket sends - prevent endless transfers.
+SendLimitConstraint ==
+    LET totalSends ==
+        SetSum({ storages[i].errinj.bucketSendCount : i \in Storages })
+    IN totalSends =< MAX_TOTAL_SENDS
+
+\* 2. Allow only a small number of concurrent masters.
+TwoMastersConstraint ==
+    Cardinality({s \in Storages : storages[s].status = "master"}) =< 2
+
+\* 3. Keep network bounded - avoid message explosion.
+NetworkBoundConstraint ==
+    \A s1, s2 \in StoragesC :
+        Len(network[s1][s2]) =< 2
+
+(***************************************************************************)
+(*                            SYMMETRY                                     *)
+(***************************************************************************)
+
+Symmetry ==
+    Permutations(BucketIdsC)
+
+(***************************************************************************)
+(*                           STATE INVARIANTS                              *)
+(***************************************************************************)
+
+NoActiveSimultaneousInv ==
+    \* No bucket can be ACTIVE in storages belonging to different ReplicaSets
+    \A b \in BucketIds :
+        \A rs1, rs2 \in ReplicaSets :
+            rs1 # rs2 =>
+                ~(\E s1, s2 \in Storages :
+                     storageToReplicaset[s1] = rs1 /\
+                     storageToReplicaset[s2] = rs2 /\
+                     storages[s1].status = "master" /\
+                     storages[s2].status = "master" /\
+                     storages[s1].buckets[b].status = "ACTIVE" /\
+                     storages[s2].buckets[b].status = "ACTIVE")
+
+================================================================================

proofs/tla/test/storage/DoubledBucketsTest.cfg

@@ -0,0 +1,26 @@
+INIT Init
+NEXT Next
+
+CONSTANTS
+    Storages <- StoragesC
+    ReplicaSets <- ReplicaSetsC
+    BucketIds <- BucketIdsC
+    StorageAssignments <- StorageAssignmentsC
+    BucketAssignments <- BucketAssignmentsC
+    MasterAssignments <- MasterAssignmentsC
+    b1 = b1
+    b2 = b2
+    b3 = b3
+
+SYMMETRY Symmetry
+
+INVARIANTS
+    NetworkTypeInv
+    StorageTypeInv
+    StorageToReplicasetTypeInv
+    NoActiveSimultaneousInv
+
+CONSTRAINT
+    SendLimitConstraint
+    NetworkBoundConstraint
+    RefConstraint

proofs/tla/test/storage/DoubledBucketsTest.tla

@@ -0,0 +1,74 @@
+------------------------- MODULE DoubledBucketsTest ----------------------------
+EXTENDS storage, utils
+
+CONSTANTS b1, b2, b3
+
+StoragesC == {"s1", "s2", "s3"}
+ReplicaSetsC == {"rs1", "rs2", "rs3"}
+BucketIdsC == {b1, b2, b3}
+StorageAssignmentsC == [rs1 |-> {"s1"},
+                       rs2 |-> {"s2"},
+                       rs3 |-> {"s3"}]
+BucketAssignmentsC == [rs1 |-> {b1},
+                       rs2 |-> {b2},
+                       rs3 |-> {b3}]
+MasterAssignmentsC == [rs1 |-> {"s1"},
+                       rs2 |-> {"s2"},
+                       rs3 |-> {"s3"}]
+
+(***************************************************************************)
+(*                           CONSTRAINTS                                   *)
+(***************************************************************************)
+
+MAX_TOTAL_SENDS == 2
+
+\* 1. Limit total bucket sends - prevent endless transfers.
+SendLimitConstraint ==
+    LET totalSends ==
+        SetSum({ storages[i].errinj.bucketSendCount : i \in StoragesC })
+    IN totalSends =< MAX_TOTAL_SENDS
+
+\* 2. Keep network bounded - avoid message explosion.
+NetworkBoundConstraint ==
+    /\ \A s1, s2 \in StoragesC :
+            Len(network[s1][s2]) =< 2
+    /\ \A s \in StoragesC :
+        /\ storages[s].errinj.networkReorderCount <= 2
+        /\ storages[s].errinj.networkDropCount <= 2
+
+RefConstraint ==
+    \A s1 \in StoragesC :
+        /\ storages[s1].errinj.bucketRWRefCount <= 0
+        /\ storages[s1].errinj.bucketRORefCount <= 0
+        /\ storages[s1].errinj.bucketRWUnRefCount <= 0
+        /\ storages[s1].errinj.bucketROUnRefCount <= 0
+
+(***************************************************************************)
+(*                            SYMMETRY                                     *)
+(***************************************************************************)
+
+Symmetry ==
+    Permutations(BucketIdsC)
+
+(***************************************************************************)
+(*                           STATE INVARIANTS                              *)
+(***************************************************************************)
+
+NoActiveSimultaneousInv ==
+    \* No bucket can be ACTIVE in storages belonging to different ReplicaSets
+    \A b \in BucketIds :
+        \A rs1, rs2 \in ReplicaSets :
+            rs1 # rs2 =>
+                ~(\E s1, s2 \in Storages :
+                     storageToReplicaset[s1] = rs1 /\
+                     storageToReplicaset[s2] = rs2 /\
+                     storages[s1].status = "master" /\
+                     storages[s2].status = "master" /\
+                     storages[s1].buckets[b].status = "ACTIVE" /\
+                     storages[s2].buckets[b].status = "ACTIVE")
+
+(***************************************************************************)
+(*                           MODEL CHECKING PROPERTIES                     *)
+(***************************************************************************)
+
+================================================================================

proofs/tla/test/storage/MasterDoubledTest.cfg

@@ -0,0 +1,20 @@
+INIT TestInit
+NEXT TestNext
+
+CONSTANTS
+    Storages <- StoragesC
+    ReplicaSets <- ReplicaSetsC
+    BucketIds <- BucketIdsC
+    StorageAssignments <- StorageAssignmentsC
+    BucketAssignments <- BucketAssignmentsC
+    MasterAssignments <- MasterAssignmentsC
+    b1 = b1
+    b2 = b2
+    b3 = b3
+    b4 = b4
+
+INVARIANTS
+    NetworkTypeInv
+    StorageTypeInv
+    StorageToReplicasetTypeInv
+    NoActiveSimultaneousInv