Skip to content

Guard B-tree splits against node exhaustion #238

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Qian-Cheng-nju wants to merge 1 commit into
base: master
Choose a base branch
from
+57 −2
Open

Guard B-tree splits against node exhaustion #238

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 40 additions & 0 deletions specifications/btree/MCbtreeExhaustion.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
\* A root split needs two free nodes; this pool has only one left.
SPECIFICATION Spec

CONSTANTS
READY = ready
GET_VALUE = get_value
FIND_LEAF_TO_ADD = find_leaf_to_add
WHICH_TO_SPLIT = which_to_split

ADD_TO_LEAF = add_to_leaf
SPLIT_ROOT_LEAF = split_root_leaf
SPLIT_ROOT_INNER = split_root_inner
SPLIT_INNER = split_inner
SPLIT_LEAF = split_leaf
UPDATE_LEAF = update_leaf


NIL = nil
MISSING = missing

Vals = {x}

MaxOccupancy = 2

CONSTANTS
MaxNode = 2
MaxKey = 3

CONSTANTS
Keys <- MCKeys
Nodes <- MCNodes

CHECK_DEADLOCK FALSE

INVARIANT
TypeOk
InnersMustHaveLast
LeavesCantHaveLast
KeyOrderPreserved
KeysInLeavesAreUnique
6 changes: 6 additions & 0 deletions specifications/btree/btree.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,6 +98,9 @@ IsFree(node) == isLeaf[node] /\ keysOf[node] = {}

ChooseFreeNode == CHOOSE n \in Nodes : IsFree(n)

HasFreeNode == \E n \in Nodes : IsFree(n)
HasTwoFreeNodes == \E n1, n2 \in Nodes : n1 # n2 /\ IsFree(n1) /\ IsFree(n2)


Init == /\ isLeaf = [n \in Nodes |-> TRUE]
/\ keysOf = [n \in Nodes |-> {}]
Expand Down Expand Up @@ -217,6 +220,7 @@ SplitRootLeaf ==
n2Keys == {x \in keys: x>=pivot}
keyToInsert == args[1] IN
/\ state = SPLIT_ROOT_LEAF
/\ HasTwoFreeNodes
/\ root' = newRoot
/\ isLeaf' = [isLeaf EXCEPT ![newRoot]=FALSE, ![n2]=TRUE]
/\ keysOf' = [keysOf EXCEPT ![newRoot]={pivot}, ![n1]=n1Keys, ![n2]=n2Keys]
Expand Down Expand Up @@ -248,6 +252,7 @@ SplitRootInner ==
n1Keys == {x \in keys: x<pivot}
n2Keys == {x \in keys: x>pivot} IN
/\ state = SPLIT_ROOT_INNER
/\ HasTwoFreeNodes
/\ root' = newRoot
/\ isLeaf' = [isLeaf EXCEPT ![newRoot]=FALSE, ![n2]=FALSE]
/\ keysOf' = [keysOf EXCEPT ![newRoot]={pivot}, ![n1]=n1Keys, ![n2]=n2Keys]
Expand All @@ -273,6 +278,7 @@ SplitLeaf ==
keyToInsert == args[1]
IN
/\ state = SPLIT_LEAF
/\ HasFreeNode
/\ isLeaf' = [isLeaf EXCEPT ![n2]=TRUE]
/\ keysOf' = [keysOf EXCEPT ![parent]=@ \union {pivot}, ![n1]=n1Keys, ![n2]=n2Keys]
\* In the parent, point the pivot key to n1, and point the parent key to n2.
Expand Down
13 changes: 11 additions & 2 deletions specifications/btree/manifest.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,17 @@
"mode": "exhaustive search",
"result": "success",
"distinctStates": 374727,
"totalStates": 2820091,
"totalStates": 2892343,
"stateDepth": 38
},
{
"path": "specifications/btree/MCbtreeExhaustion.cfg",
"runtime": "00:00:01",
"mode": "exhaustive search",
"result": "success",
"distinctStates": 202,
"totalStates": 778,
"stateDepth": 11
}
]
},
Expand All @@ -44,4 +53,4 @@
]
}
]
}
}
Loading