Skip to content

Commit 5e90e0e

Browse files
lorinahelwer
lorin
authored and
ahelwer
committed
Added a B-tree TLA⁺ specification
Blog post: https://surfingcomplexity.blog/2024/07/04/modeling-b-trees-in-tla/ Signed-off-by: Lorin Hochstein <lorinh@gmail.com> Co-authored-by: Lorin Hochstein <lorinh@gmail.com>
1 parent 18c5810 commit 5e90e0e

5 files changed

Lines changed: 512 additions & 0 deletions

File tree

‎specifications/btree/README.md‎

Whitespace-only changes.

‎specifications/btree/btree.cfg‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
SPECIFICATION Spec
2+
3+
CONSTANTS
4+
READY = ready
5+
GET_VALUE = get_value
6+
FIND_LEAF_TO_ADD = find_leaf_to_add
7+
WHICH_TO_SPLIT = which_to_split
8+
9+
ADD_TO_LEAF = add_to_leaf
10+
SPLIT_ROOT_LEAF = split_root_leaf
11+
SPLIT_ROOT_INNER = split_root_inner
12+
SPLIT_INNER = split_inner
13+
SPLIT_LEAF = split_leaf
14+
UPDATE_LEAF = update_leaf
15+
16+
17+
NIL = nil
18+
MISSING = missing
19+
20+
Vals = {x,y,z}
21+
22+
MaxOccupancy = 2
23+
MaxNode = 8
24+
MaxKey = 4
25+
26+
\* PROPERTY
27+
\* Refinement
28+
29+
INVARIANT
30+
TypeOk
31+
InnersMustHaveLast
32+
LeavesCantHaveLast
33+
KeyOrderPreserved
34+
KeysInLeavesAreUnique
35+
FreeNodesRemain

‎specifications/btree/btree.tla‎

Lines changed: 317 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,317 @@
1+
\* Note: deletes have not been implemented
2+
---- MODULE btree ----
3+
EXTENDS TLC,
4+
Naturals,
5+
FiniteSets,
6+
Sequences
7+
8+
CONSTANTS Vals,
9+
MaxKey,
10+
MaxNode,
11+
MaxOccupancy,
12+
13+
\* states
14+
READY,
15+
GET_VALUE,
16+
FIND_LEAF_TO_ADD,
17+
WHICH_TO_SPLIT,
18+
ADD_TO_LEAF,
19+
SPLIT_LEAF,
20+
SPLIT_INNER,
21+
SPLIT_ROOT_LEAF,
22+
SPLIT_ROOT_INNER,
23+
UPDATE_LEAF
24+
25+
Keys == 1..MaxKey
26+
Nodes == 1..MaxNode
27+
28+
NIL == CHOOSE x : x \notin Nodes
29+
MISSING == CHOOSE v : v \notin Vals
30+
31+
32+
VARIABLES root,
33+
isLeaf, keysOf, childOf, lastOf, valOf,
34+
focus,
35+
toSplit,
36+
op, args, ret,
37+
state
38+
39+
TypeOk == /\ root \in Nodes
40+
/\ isLeaf \in [Nodes -> BOOLEAN]
41+
/\ keysOf \in [Nodes -> SUBSET Keys]
42+
/\ childOf \in [Nodes \X Keys -> Nodes \union {NIL}]
43+
/\ lastOf \in [Nodes -> Nodes \union {NIL}]
44+
/\ valOf \in [Nodes \X Keys -> Vals \union {NIL}]
45+
/\ focus \in Nodes \union {NIL}
46+
/\ toSplit \in Seq(Nodes)
47+
/\ op \in {"get", "insert", "update", NIL}
48+
/\ ret \in Vals \union {"ok", "error", MISSING, NIL}
49+
/\ state \in {READY, GET_VALUE, FIND_LEAF_TO_ADD, WHICH_TO_SPLIT, ADD_TO_LEAF, SPLIT_LEAF, SPLIT_INNER, SPLIT_ROOT_LEAF, SPLIT_ROOT_INNER, UPDATE_LEAF}
50+
51+
\* Max element in a set
52+
Max(xs) == CHOOSE x \in xs : (\A y \in xs \ {x} : x > y)
53+
54+
\* Find the appropriate child node associated with the key
55+
ChildNodeFor(node, key) ==
56+
LET keys == keysOf[node]
57+
maxKey == Max(keys)
58+
closestKey == CHOOSE k \in keys : /\ k>key
59+
/\ ~(\E j \in keys \ {k} : j>key /\ j<k)
60+
IN IF keys = {} \/ key >= maxKey
61+
THEN lastOf[node]
62+
\* smallest k that's bigger than key
63+
ELSE
64+
childOf[node, closestKey]
65+
66+
67+
\* Identify the leaf node based on key
68+
\* Find the leaf node associated with a key
69+
RECURSIVE FindLeafNode(_, _)
70+
FindLeafNode(node, key) ==
71+
IF isLeaf[node] THEN node ELSE FindLeafNode(ChildNodeFor(node, key), key)
72+
73+
AtMaxOccupancy(node) == Cardinality(keysOf[node]) = MaxOccupancy
74+
75+
76+
\* We model a "free" (not yet part of the tree) node as one as a leaf with no keys
77+
IsFree(node) == isLeaf[node] /\ keysOf[node] = {}
78+
79+
ChooseFreeNode == CHOOSE n \in Nodes : IsFree(n)
80+
81+
82+
Init == /\ isLeaf = [n \in Nodes |-> TRUE]
83+
/\ keysOf = [n \in Nodes |-> {}]
84+
/\ childOf = [n \in Nodes, k \in Keys |-> NIL]
85+
/\ lastOf = [n \in Nodes |-> NIL]
86+
/\ valOf = [n \in Nodes, k \in Keys |-> NIL]
87+
/\ root = ChooseFreeNode
88+
/\ focus = NIL
89+
/\ toSplit = <<>>
90+
/\ op = NIL
91+
/\ args = NIL
92+
/\ ret = NIL
93+
/\ state = READY
94+
95+
GetReq(key) ==
96+
/\ state = READY
97+
/\ op' = "get"
98+
/\ args' = <<key>>
99+
/\ ret' = NIL
100+
/\ state' = GET_VALUE
101+
/\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, valOf, focus, toSplit>>
102+
103+
GetValue ==
104+
LET key == args[1]
105+
node == FindLeafNode(root, key) IN
106+
/\ state = GET_VALUE
107+
/\ state' = READY
108+
/\ ret' = IF key \in keysOf[node] THEN valOf[node, key] ELSE MISSING
109+
/\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, valOf, focus, toSplit, args, op>>
110+
111+
112+
InsertReq(key, val) ==
113+
/\ state = READY
114+
/\ op' = "insert"
115+
/\ args' = <<key, val>>
116+
/\ ret' = NIL
117+
/\ state' = FIND_LEAF_TO_ADD
118+
/\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, valOf, focus, toSplit>>
119+
120+
UpdateReq(key, val) ==
121+
LET leaf == FindLeafNode(root, key)
122+
IN /\ state = READY
123+
/\ op' = "update"
124+
/\ args' = <<key, val>>
125+
/\ ret' = NIL
126+
/\ focus' = leaf
127+
/\ state' = UPDATE_LEAF
128+
/\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, valOf, toSplit>>
129+
130+
UpdateLeaf ==
131+
LET key == args[1]
132+
val == args[2]
133+
IN /\ state = UPDATE_LEAF
134+
/\ valOf' = IF key \in keysOf[focus] THEN [valOf EXCEPT ![focus, key]=val] ELSE valOf
135+
/\ ret' = IF key \in keysOf[focus] THEN "ok" ELSE "error"
136+
/\ state' = READY
137+
/\ focus' = NIL
138+
/\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, toSplit, args, op>>
139+
140+
FindLeafToAdd ==
141+
LET key == args[1]
142+
leaf == FindLeafNode(root, key)
143+
IN /\ state = FIND_LEAF_TO_ADD
144+
/\ focus' = leaf
145+
/\ toSplit' = IF AtMaxOccupancy(leaf) THEN <<leaf>> ELSE <<>>
146+
/\ state' = IF AtMaxOccupancy(leaf) THEN WHICH_TO_SPLIT ELSE ADD_TO_LEAF
147+
/\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, valOf, args, op, ret>>
148+
149+
150+
ParentOf(n) == CHOOSE p \in Nodes: \/ \E k \in Keys: n = childOf[p, k]
151+
\/ lastOf[p]=n
152+
153+
WhichToSplit ==
154+
LET node == Head(toSplit)
155+
parent == ParentOf(node)
156+
splitParent == AtMaxOccupancy(parent)
157+
noMoreSplits == ~splitParent \* if the parent doesn't need splitting, we don't need to consider more nodes for splitting
158+
IN /\ state = WHICH_TO_SPLIT
159+
/\ toSplit' =
160+
CASE node = root -> toSplit
161+
[] splitParent -> <<parent>> \o toSplit
162+
[] OTHER -> toSplit
163+
/\ state' =
164+
CASE node # root /\ noMoreSplits /\ isLeaf[node] -> SPLIT_LEAF
165+
[] node # root /\ noMoreSplits /\ ~isLeaf[node] -> SPLIT_INNER
166+
[] node = root /\ isLeaf[node] -> SPLIT_ROOT_LEAF
167+
[] node = root /\ ~isLeaf[node] -> SPLIT_ROOT_INNER
168+
[] OTHER -> WHICH_TO_SPLIT
169+
/\ UNCHANGED <<root, isLeaf, keysOf, childOf, lastOf, valOf, op, args, ret, focus>>
170+
171+
\* Adding the <<key, val>> pair in args to the node indicated by focus
172+
\* If the key is already present, this is an error
173+
AddToLeaf ==
174+
LET key == args[1]
175+
val == args[2] IN
176+
/\ state = ADD_TO_LEAF
177+
/\ ret' = IF key \notin keysOf[focus] THEN "ok" ELSE "error"
178+
/\ keysOf' = IF key \notin keysOf[focus] THEN [keysOf EXCEPT ![focus]=@ \union {key}] ELSE keysOf
179+
/\ valOf' = IF key \notin keysOf[focus] THEN [valOf EXCEPT ![focus,key]=val] ELSE valOf
180+
/\ state' = READY
181+
/\ UNCHANGED <<root, isLeaf, childOf, lastOf, op, args, focus, toSplit>>
182+
183+
\* Return the pivot (midpoint) of a set of keys. If there are an even number of keys, bias towards the smaller one
184+
PivotOf(keys) == CHOOSE k \in keys :
185+
LET smaller == {x \in keys : x < k}
186+
larger == {x \in keys: x > k} IN
187+
\/ Cardinality(smaller) = Cardinality(larger)
188+
\/ Cardinality(smaller) = Cardinality(larger)+1
189+
190+
SplitRootLeaf ==
191+
LET n1 == Head(toSplit)
192+
n2 == ChooseFreeNode
193+
newRoot == CHOOSE n \in Nodes : IsFree(n) /\ (n # n2)
194+
keys == keysOf[n1]
195+
pivot == PivotOf(keys)
196+
n1Keys == {x \in keys: x<pivot}
197+
n2Keys == {x \in keys: x>=pivot}
198+
keyToInsert == args[1] IN
199+
/\ state = SPLIT_ROOT_LEAF
200+
/\ root' = newRoot
201+
/\ isLeaf' = [isLeaf EXCEPT ![newRoot]=FALSE, ![n2]=TRUE]
202+
/\ keysOf' = [keysOf EXCEPT ![newRoot]={pivot}, ![n1]=n1Keys, ![n2]=n2Keys]
203+
/\ childOf' = [childOf EXCEPT ![newRoot, pivot]=n1]
204+
/\ lastOf' = [lastOf EXCEPT ![newRoot]=n2]
205+
/\ valOf' = [n \in Nodes, k \in Keys |->
206+
CASE n=n1 /\ k \in n2Keys -> NIL
207+
[] n=n2 /\ k \in n2Keys -> valOf[n1, k]
208+
[] OTHER -> valOf[n, k]]
209+
\* No more splits necessary, add the focus to the leaf
210+
\* Note that the focus may have changed due to the split
211+
/\ state' = ADD_TO_LEAF
212+
/\ focus' = IF keyToInsert < pivot THEN n1 ELSE n2
213+
/\ UNCHANGED <<op, args, ret, toSplit>>
214+
215+
ParentKeyOf(node) ==
216+
LET p == ParentOf(node) IN
217+
CHOOSE k \in keysOf[p]: childOf[p, k] = node
218+
219+
IsLastOfParent(node) == lastOf[ParentOf(node)] = node
220+
221+
SplitRootInner ==
222+
LET n1 == Head(toSplit)
223+
n2 == ChooseFreeNode
224+
newRoot == CHOOSE n \in Nodes : IsFree(n) /\ (n # n2)
225+
keys == keysOf[n1]
226+
pivot == PivotOf(keys)
227+
(* when splitting an inner node, pivot does not appear in either node, only in parent *)
228+
n1Keys == {x \in keys: x<pivot}
229+
n2Keys == {x \in keys: x>pivot} IN
230+
/\ state = SPLIT_ROOT_INNER
231+
/\ root' = newRoot
232+
/\ isLeaf' = [isLeaf EXCEPT ![newRoot]=FALSE, ![n2]=FALSE]
233+
/\ keysOf' = [keysOf EXCEPT ![newRoot]={pivot}, ![n1]=n1Keys, ![n2]=n2Keys]
234+
/\ childOf' = [n \in Nodes, k \in Keys |->
235+
CASE n=newRoot /\ k=pivot -> n1
236+
[] n=n1 /\ k \in n2Keys -> NIL
237+
[] n=n1 /\ k \in n1Keys -> childOf[n1, k]
238+
[] n=n2 /\ k \in n2Keys -> childOf[n1, k]
239+
[] OTHER -> childOf[n, k]]
240+
/\ lastOf' = [lastOf EXCEPT ![newRoot]=n2, ![n1]=childOf[n1, pivot], ![n2]=lastOf[n1]]
241+
/\ toSplit' = <<>>
242+
/\ state' = ADD_TO_LEAF
243+
/\ UNCHANGED <<op, args, ret, focus, valOf>>
244+
245+
SplitLeaf ==
246+
LET n1 == Head(toSplit)
247+
n2 == ChooseFreeNode
248+
keys == keysOf[n1]
249+
pivot == PivotOf(keys)
250+
parent == ParentOf(n1)
251+
n1Keys == {x \in keys: x<pivot}
252+
n2Keys == {x \in keys: x>=pivot}
253+
keyToInsert == args[1]
254+
IN
255+
/\ state = SPLIT_LEAF
256+
/\ isLeaf' = [isLeaf EXCEPT ![n2]=TRUE]
257+
/\ keysOf' = [keysOf EXCEPT ![parent]=@ \union {pivot}, ![n1]=n1Keys, ![n2]=n2Keys]
258+
\* In the parent, point the pivot key to n1, and point the parent key to n2.
259+
\* TODO: handle the edge case where n1 was the last element
260+
/\ childOf' = IF IsLastOfParent(n1)
261+
THEN [childOf EXCEPT ![parent, pivot]=n1]
262+
ELSE [childOf EXCEPT ![parent, pivot]=n1, ![parent, ParentKeyOf(n1)]=n2]
263+
/\ lastOf' = IF IsLastOfParent(n1) THEN [lastOf EXCEPT ![parent]=n2] ELSE lastOf
264+
/\ valOf' = [n \in Nodes, k \in Keys |->
265+
CASE n=n1 /\ k \in n2Keys -> NIL
266+
[] n=n2 /\ k \in n2Keys -> valOf[n1, k]
267+
[] OTHER -> valOf[n, k]]
268+
/\ state' = ADD_TO_LEAF
269+
/\ focus' = IF keyToInsert < pivot THEN n1 ELSE n2
270+
/\ UNCHANGED <<root, toSplit, op, args, ret>>
271+
272+
273+
Next == \/ \E key \in Keys, val \in Vals :
274+
\/ InsertReq(key, val)
275+
\/ UpdateReq(key, val)
276+
\/ \E key \in Keys: GetReq(key)
277+
\/ GetValue
278+
\/ FindLeafToAdd
279+
\/ WhichToSplit
280+
\/ AddToLeaf
281+
\/ SplitLeaf
282+
\/ SplitRootLeaf
283+
\/ SplitRootInner
284+
\/ UpdateLeaf
285+
286+
vars == <<root, isLeaf, keysOf, childOf, lastOf, valOf, focus, toSplit, op, args, ret, state>>
287+
288+
Spec == Init /\ [][Next]_vars /\ WF_op(\E key \in Keys: GetReq(key))
289+
290+
\*
291+
\* Refinement mapping
292+
\*
293+
294+
Leaves == {n \in Nodes : isLeaf[n]}
295+
296+
Mapping == INSTANCE kvstore
297+
WITH dict <- [key \in Keys |-> IF \E leaf \in Leaves : key \in keysOf[leaf]
298+
THEN LET leaf == CHOOSE leaf \in Leaves : key \in keysOf[leaf]
299+
IN valOf[leaf, key] ELSE MISSING],
300+
state <- IF state = READY THEN "ready" ELSE "working"
301+
302+
303+
Refinement == Mapping!Spec
304+
305+
\*
306+
\* Invariants
307+
\*
308+
Inners == {n \in Nodes: ~isLeaf[n]}
309+
310+
InnersMustHaveLast == \A n \in Inners : lastOf[n] # NIL
311+
KeyOrderPreserved == \A n \in Inners : (\A k \in keysOf[n] : (\A kc \in keysOf[childOf[n, k]]: kc < k))
312+
LeavesCantHaveLast == \A n \in Leaves : lastOf[n] = NIL
313+
KeysInLeavesAreUnique ==
314+
\A n1, n2 \in Leaves : ((keysOf[n1] \intersect keysOf[n2]) # {}) => n1=n2
315+
FreeNodesRemain == \E n \in Nodes : IsFree(n)
316+
317+
====

‎specifications/btree/kvstore.cfg‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
SPECIFICATION Spec
2+
\* Uncomment the previous line and provide the specification name if it's declared
3+
\* in the specification file. Comment INIT / NEXT parameters if you use SPECIFICATION.
4+
5+
CONSTANTS
6+
Keys = {"A", "B", "C"}
7+
Vals = {X, Y, Z}
8+
NIL = NIL
9+
MISSING = "missing"
10+
11+
\* INIT Init
12+
\* NEXT Next
13+
14+
\* PROPERTY
15+
16+
\* Uncomment the previous line and add property names
17+
18+
19+
INVARIANT
20+
TypeOK

0 commit comments

Comments
 (0)