Skip to content

Commit e82391f

Browse files
SerpentianSerpentian
committed
tla/storage: initial implementation
Run the tests with: ```sh JAVA_OPTS="-DTLA-Library=../../src" tlc DoubledBucketsSmallTest.tla -config DoubledBucketsSmallTest.cfg -workers 6 -continue -checkpoint 10 ``` DoubledBucketsSmallTest reliably reproduces the doubled bucket problem, which is related to master change. DoubledBucketsTest requires constraints to become useful. NO_DOC=tla NO_TEST=tla
1 parent 3f48a8f commit e82391f

19 files changed

+1529
-0
lines changed

‎.gitignore‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,3 +21,7 @@ build
2121
.rocks
2222
build.luarocks
2323
.DS_Store
24+
25+
# TLA+ files
26+
states/
27+
*_TTrace_*

‎proofs/tla/src/storage.tla‎

Lines changed: 645 additions & 0 deletions
Large diffs are not rendered by default.

‎proofs/tla/src/utils.tla‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
------------------------------- MODULE utils -----------------------------------
2+
3+
EXTENDS Naturals, FiniteSets
4+
5+
RECURSIVE SetSum(_)
6+
SetSum(set) == IF set = {} THEN 0 ELSE
7+
LET x == CHOOSE x \in set: TRUE
8+
IN x + SetSum(set \ {x})
9+
10+
================================================================================

‎proofs/tla/test/storage/DoubledBucketsSmallTest.cfg‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
INIT Init
2+
NEXT Next
3+
4+
CONSTANTS
5+
Storages <- StoragesC
6+
ReplicaSets <- ReplicaSetsC
7+
BucketIds <- BucketIdsC
8+
StorageAssignments <- StorageAssignmentsC
9+
BucketAssignments <- BucketAssignmentsC
10+
MasterAssignments <- MasterAssignmentsC
11+
b1 = b1
12+
b2 = b2
13+
14+
SYMMETRY Symmetry
15+
16+
INVARIANTS
17+
NetworkTypeInv
18+
StorageTypeInv
19+
StorageToReplicasetTypeInv
20+
NoActiveSimultaneousInv
21+
22+
CONSTRAINTS
23+
SendLimitConstraint
24+
NetworkBoundConstraint
25+
TwoMastersConstraint

‎proofs/tla/test/storage/DoubledBucketsSmallTest.tla‎

Lines changed: 61 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
-------------------------MODULE DoubledBucketsSmallTest ------------------------
2+
EXTENDS storage, utils
3+
4+
CONSTANTS b1, b2
5+
6+
StoragesC == {"s1", "s2", "s3", "s4"}
7+
ReplicaSetsC == {"rs1", "rs2"}
8+
BucketIdsC == {b1, b2}
9+
StorageAssignmentsC == [rs1 |-> {"s1", "s2"},
10+
rs2 |-> {"s3", "s4"}]
11+
BucketAssignmentsC == [rs1 |-> {b1},
12+
rs2 |-> {b2}]
13+
MasterAssignmentsC == [rs1 |-> {"s1"},
14+
rs2 |-> {"s3"}]
15+
16+
(***************************************************************************)
17+
(* CONSTRAINTS *)
18+
(***************************************************************************)
19+
20+
MAX_TOTAL_SENDS == 1
21+
22+
\* 1. Limit total bucket sends - prevent endless transfers.
23+
SendLimitConstraint ==
24+
LET totalSends ==
25+
SetSum({ storages[i].errinj.bucketSendCount : i \in Storages })
26+
IN totalSends =< MAX_TOTAL_SENDS
27+
28+
\* 2. Allow only a small number of concurrent masters.
29+
TwoMastersConstraint ==
30+
Cardinality({s \in Storages : storages[s].status = "master"}) =< 2
31+
32+
\* 3. Keep network bounded - avoid message explosion.
33+
NetworkBoundConstraint ==
34+
\A s1, s2 \in StoragesC :
35+
Len(network[s1][s2]) =< 2
36+
37+
(***************************************************************************)
38+
(* SYMMETRY *)
39+
(***************************************************************************)
40+
41+
Symmetry ==
42+
Permutations(BucketIdsC)
43+
44+
(***************************************************************************)
45+
(* STATE INVARIANTS *)
46+
(***************************************************************************)
47+
48+
NoActiveSimultaneousInv ==
49+
\* No bucket can be ACTIVE in storages belonging to different ReplicaSets
50+
\A b \in BucketIds :
51+
\A rs1, rs2 \in ReplicaSets :
52+
rs1 # rs2 =>
53+
~(\E s1, s2 \in Storages :
54+
storageToReplicaset[s1] = rs1 /\
55+
storageToReplicaset[s2] = rs2 /\
56+
storages[s1].status = "master" /\
57+
storages[s2].status = "master" /\
58+
storages[s1].buckets[b].status = "ACTIVE" /\
59+
storages[s2].buckets[b].status = "ACTIVE")
60+
61+
================================================================================

‎proofs/tla/test/storage/DoubledBucketsTest.cfg‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
INIT Init
2+
NEXT Next
3+
4+
CONSTANTS
5+
Storages <- StoragesC
6+
ReplicaSets <- ReplicaSetsC
7+
BucketIds <- BucketIdsC
8+
StorageAssignments <- StorageAssignmentsC
9+
BucketAssignments <- BucketAssignmentsC
10+
MasterAssignments <- MasterAssignmentsC
11+
b1 = b1
12+
b2 = b2
13+
b3 = b3
14+
15+
SYMMETRY Symmetry
16+
17+
INVARIANTS
18+
NetworkTypeInv
19+
StorageTypeInv
20+
StorageToReplicasetTypeInv
21+
NoActiveSimultaneousInv
22+
23+
CONSTRAINT
24+
SendLimitConstraint
25+
NetworkBoundConstraint
26+
RefConstraint

‎proofs/tla/test/storage/DoubledBucketsTest.tla‎

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
------------------------- MODULE DoubledBucketsTest ----------------------------
2+
EXTENDS storage, utils
3+
4+
CONSTANTS b1, b2, b3
5+
6+
StoragesC == {"s1", "s2", "s3"}
7+
ReplicaSetsC == {"rs1", "rs2", "rs3"}
8+
BucketIdsC == {b1, b2, b3}
9+
StorageAssignmentsC == [rs1 |-> {"s1"},
10+
rs2 |-> {"s2"},
11+
rs3 |-> {"s3"}]
12+
BucketAssignmentsC == [rs1 |-> {b1},
13+
rs2 |-> {b2},
14+
rs3 |-> {b3}]
15+
MasterAssignmentsC == [rs1 |-> {"s1"},
16+
rs2 |-> {"s2"},
17+
rs3 |-> {"s3"}]
18+
19+
(***************************************************************************)
20+
(* CONSTRAINTS *)
21+
(***************************************************************************)
22+
23+
MAX_TOTAL_SENDS == 2
24+
25+
\* 1. Limit total bucket sends - prevent endless transfers.
26+
SendLimitConstraint ==
27+
LET totalSends ==
28+
SetSum({ storages[i].errinj.bucketSendCount : i \in StoragesC })
29+
IN totalSends =< MAX_TOTAL_SENDS
30+
31+
\* 2. Keep network bounded - avoid message explosion.
32+
NetworkBoundConstraint ==
33+
/\ \A s1, s2 \in StoragesC :
34+
Len(network[s1][s2]) =< 3
35+
/\ \A s \in StoragesC :
36+
/\ storages[s].errinj.networkReorderCount <= 1
37+
/\ storages[s].errinj.networkDropCount <= 1
38+
39+
RefConstraint ==
40+
\A s1 \in StoragesC :
41+
/\ storages[s1].errinj.bucketRWRefCount <= 0
42+
/\ storages[s1].errinj.bucketRORefCount <= 0
43+
/\ storages[s1].errinj.bucketRWUnRefCount <= 0
44+
/\ storages[s1].errinj.bucketROUnRefCount <= 0
45+
46+
(***************************************************************************)
47+
(* SYMMETRY *)
48+
(***************************************************************************)
49+
50+
Symmetry ==
51+
Permutations(BucketIdsC)
52+
53+
(***************************************************************************)
54+
(* STATE INVARIANTS *)
55+
(***************************************************************************)
56+
57+
NoActiveSimultaneousInv ==
58+
\* No bucket can be ACTIVE in storages belonging to different ReplicaSets
59+
\A b \in BucketIds :
60+
\A rs1, rs2 \in ReplicaSets :
61+
rs1 # rs2 =>
62+
~(\E s1, s2 \in Storages :
63+
storageToReplicaset[s1] = rs1 /\
64+
storageToReplicaset[s2] = rs2 /\
65+
storages[s1].status = "master" /\
66+
storages[s2].status = "master" /\
67+
storages[s1].buckets[b].status = "ACTIVE" /\
68+
storages[s2].buckets[b].status = "ACTIVE")
69+
70+
(***************************************************************************)
71+
(* MODEL CHECKING PROPERTIES *)
72+
(***************************************************************************)
73+
74+
================================================================================

‎proofs/tla/test/storage/MasterDoubledTest.cfg‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
INIT TestInit
2+
NEXT TestNext
3+
4+
CONSTANTS
5+
Storages <- StoragesC
6+
ReplicaSets <- ReplicaSetsC
7+
BucketIds <- BucketIdsC
8+
StorageAssignments <- StorageAssignmentsC
9+
BucketAssignments <- BucketAssignmentsC
10+
MasterAssignments <- MasterAssignmentsC
11+
b1 = b1
12+
b2 = b2
13+
b3 = b3
14+
b4 = b4
15+
16+
INVARIANTS
17+
NetworkTypeInv
18+
StorageTypeInv
19+
StorageToReplicasetTypeInv
20+
NoActiveSimultaneousInv

‎proofs/tla/test/storage/MasterDoubledTest.tla‎

Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
1+
-------------------------- MODULE MasterDoubledTest ----------------------------
2+
EXTENDS storage, TLC
3+
4+
(***************************************************************************)
5+
(* Cluster: two replica sets, two storages each. *)
6+
(* We'll force rs1 to send a bucket to rs2, lose replication, and failover.*)
7+
(***************************************************************************)
8+
9+
CONSTANTS
10+
b1, b2, b3, b4
11+
12+
StoragesC == {"s1", "s2", "s3", "s4"}
13+
ReplicaSetsC == {"rs1", "rs2"}
14+
BucketIdsC == {b1, b2, b3, b4}
15+
StorageAssignmentsC ==
16+
[rs1 |-> {"s1", "s2"},
17+
rs2 |-> {"s3", "s4"}]
18+
BucketAssignmentsC ==
19+
[rs1 |-> {b1, b2},
20+
rs2 |-> {b3, b4}]
21+
MasterAssignmentsC ==
22+
[rs1 |-> {"s1"},
23+
rs2 |-> {"s3"}]
24+
25+
(***************************************************************************)
26+
(* Variables and initialization *)
27+
(***************************************************************************)
28+
29+
VARIABLE phase
30+
31+
TestInit ==
32+
/\ Init
33+
/\ phase = 1
34+
35+
(***************************************************************************)
36+
(* Phase-driven Next *)
37+
(***************************************************************************)
38+
39+
TestNext ==
40+
\/ /\ phase = 1
41+
/\ ~(
42+
storages["s1"].buckets[b1].status = "SENT"
43+
/\ storages["s3"].buckets[b1].status = "ACTIVE"
44+
)
45+
/\ \E i \in {"s1"}, j \in {"s3"}, b \in {b1} :
46+
\/ StorageStateApply(i, BucketSendStart(StorageState(i), b, j))
47+
\/ /\ Len(StorageState(j).networkReceive[i]) > 0
48+
/\ \/ StorageStateApply(j, BucketRecvStart(StorageState(j), i))
49+
\/ StorageStateApply(j, BucketRecvFinish(StorageState(j), i))
50+
\/ /\ Len(StorageState(i).networkReceive[j]) > 0
51+
/\ StorageStateApply(i, BucketSendFinish(StorageState(i), j))
52+
/\ UNCHANGED <<storageToReplicaset, phase>>
53+
54+
\/ /\ phase = 1
55+
/\ storages["s1"].buckets[b1].status = "SENT"
56+
/\ storages["s3"].buckets[b1].status = "ACTIVE"
57+
/\ UNCHANGED <<network, storages, storageToReplicaset>>
58+
/\ phase' = 3
59+
60+
\/ /\ phase = 3
61+
/\ \E i \in {"s2"} :
62+
/\ StorageStateApply(i, BecomeMaster(StorageState(i)))
63+
/\ PrintT("Phase 3: failover, s2 becomes master")
64+
/\ phase' = 4
65+
66+
\/ /\ phase = 4
67+
/\ UNCHANGED <<network, storages, storageToReplicaset, phase>>
68+
/\ PrintT("Phase 4: check for double ACTIVE")
69+
70+
(***************************************************************************)
71+
(* Spec *)
72+
(***************************************************************************)
73+
74+
Spec ==
75+
TestInit /\ [][TestNext]_<<network, storages, storageToReplicaset, phase>>
76+
77+
(***************************************************************************)
78+
(* STATE INVARIANTS *)
79+
(***************************************************************************)
80+
81+
NoActiveSimultaneousInv ==
82+
\* No bucket can be ACTIVE in storages belonging to different ReplicaSets
83+
\A b \in BucketIds :
84+
\A rs1, rs2 \in ReplicaSets :
85+
rs1 # rs2 =>
86+
~(\E s1, s2 \in Storages :
87+
storageToReplicaset[s1] = rs1 /\
88+
storageToReplicaset[s2] = rs2 /\
89+
storages[s1].status = "master" /\
90+
storages[s2].status = "master" /\
91+
storages[s1].buckets[b].status = "ACTIVE" /\
92+
storages[s2].buckets[b].status = "ACTIVE")
93+
===============================================================================

‎proofs/tla/test/storage/RecoveryGarbageTest.cfg‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
CONSTANTS
2+
Storages <- StoragesC
3+
ReplicaSets <- ReplicaSetsC
4+
BucketIds <- BucketIdsC
5+
StorageAssignments <- StorageAssignmentsC
6+
BucketAssignments <- BucketAssignmentsC
7+
MasterAssignments <- MasterAssignmentsC
8+
b1 = b1
9+
b2 = b2
10+
b3 = b3
11+
b4 = b4
12+
13+
INVARIANTS
14+
NetworkTypeInv
15+
StorageTypeInv
16+
StorageToReplicasetTypeInv
17+
NoActiveSimultaneousInv
18+
19+
SPECIFICATION Spec
20+
21+
CONSTRAINT SendLimitConstraint
22+
23+
PROPERTY
24+
AllBucketsEventuallyStable

0 commit comments

Comments
 (0)