diff --git a/.gitignore b/.gitignore index fe473517..28f820d2 100644 --- a/.gitignore +++ b/.gitignore @@ -53,3 +53,8 @@ examples/compile_commands.json **/*#* /docs/ +# TLC model checker artifacts +spec/tla/*_TTrace_*.bin +spec/tla/*_TTrace_*.tla +spec/tla/states/ + diff --git a/spec/tla/ARTTreeMaintenance.cfg b/spec/tla/ARTTreeMaintenance.cfg new file mode 100644 index 00000000..d444fe21 --- /dev/null +++ b/spec/tla/ARTTreeMaintenance.cfg @@ -0,0 +1,13 @@ +SPECIFICATION Spec + +CONSTANTS + PrefixCapacity = 2 + +INVARIANTS + TypeOK + NoOrphans + KeyPreservation + WellFormed + +CONSTRAINT + StateConstraint diff --git a/spec/tla/ARTTreeMaintenance.tla b/spec/tla/ARTTreeMaintenance.tla new file mode 100644 index 00000000..d16be71f --- /dev/null +++ b/spec/tla/ARTTreeMaintenance.tla @@ -0,0 +1,552 @@ +--------------------------- MODULE ARTTreeMaintenance --------------------------- +(***************************************************************************) +(* Stage 12: ART Tree Structure Maintenance *) +(* *) +(* Verifies sequential correctness of insert/remove on an ART tree, *) +(* focusing on chain nodes and try_collapse_i4. *) +(* *) +(* Key encoding: path from root spells the key. Each node contributes *) +(* prefix bytes, then 1 dispatch byte selects a child. Terminal node's *) +(* prefix consumes final bytes; is_vis=TRUE marks key presence. *) +(***************************************************************************) +EXTENDS Integers, Sequences, FiniteSets, TLC + +CONSTANTS + PrefixCapacity \* Max prefix bytes per node (2) + +\* Fixed key set exercising all variety dimensions +Keys == {<<1>>, <<1, 2>>, <<1, 2, 1>>, <<2, 1>>, <<1, 2, 1, 2, 1>>} + +VARIABLES + nodes, \* node_id :> [prefix, children, is_vis] + root, \* node_id of root, or 0 if empty + present, \* Set of keys currently stored + nxt \* Next fresh node ID + +vars == <> + +NULL == 0 +Alphabet == {1, 2} +EmptyFcn == [x \in {} |-> x] + +(***************************************************************************) +(* KEY REACHABILITY *) +(***************************************************************************) + +RECURSIVE KeyAt(_, _, _) +KeyAt(nid, key, pos) == + IF nid = NULL \/ nid \notin DOMAIN nodes THEN FALSE + ELSE + LET n == nodes[nid] + plen == Len(n.prefix) + IN + IF plen > Len(key) - pos + 1 THEN FALSE + ELSE IF plen > 0 /\ SubSeq(key, pos, pos + plen - 1) /= n.prefix THEN FALSE + ELSE + LET ap == pos + plen IN + IF ap > Len(key) THEN n.is_vis + ELSE + LET d == key[ap] IN + IF d \notin DOMAIN n.children THEN FALSE + ELSE KeyAt(n.children[d], key, ap + 1) + +(***************************************************************************) +(* REACHABILITY *) +(***************************************************************************) + +RECURSIVE Reachable(_) +Reachable(nid) == + IF nid = NULL \/ nid \notin DOMAIN nodes THEN {} + ELSE LET n == nodes[nid] IN + {nid} \union UNION {Reachable(n.children[b]) : b \in DOMAIN n.children} + +(***************************************************************************) +(* INSERT — Build Chain *) +(***************************************************************************) + +RECURSIVE MkChain(_, _, _) +MkChain(key, pos, base) == + LET remaining == Len(key) - pos + 1 IN + IF remaining <= 0 THEN + <<(base :> [prefix |-> <<>>, children |-> EmptyFcn, is_vis |-> TRUE]), + base, base + 1>> + ELSE IF remaining <= PrefixCapacity THEN + <<(base :> [prefix |-> SubSeq(key, pos, Len(key)), + children |-> EmptyFcn, is_vis |-> TRUE]), + base, base + 1>> + ELSE + LET plen == IF remaining - 1 <= PrefixCapacity + THEN remaining - 1 ELSE PrefixCapacity + pfx == SubSeq(key, pos, pos + plen - 1) + d == key[pos + plen] + sub == MkChain(key, pos + plen + 1, base + 1) + IN <<(base :> [prefix |-> pfx, + children |-> (d :> sub[2]), + is_vis |-> FALSE]) @@ sub[1], + base, sub[3]>> + +(***************************************************************************) +(* INSERT — Recursive Core *) +(***************************************************************************) + +\* Returns <> +RECURSIVE DoInsert(_, _, _, _, _, _) +DoInsert(ns, rt, key, pos, nid, nx) == + LET n == ns[nid] + plen == Len(n.prefix) + key_rem == Len(key) - pos + 1 + match_max == IF plen < key_rem THEN plen ELSE key_rem + RECURSIVE PfxMatch(_) + PfxMatch(i) == + IF i > match_max THEN match_max + ELSE IF key[pos + i - 1] /= n.prefix[i] THEN i - 1 + ELSE PfxMatch(i + 1) + mlen == IF plen = 0 THEN 0 ELSE PfxMatch(1) + IN + IF mlen < plen THEN + \* PREFIX SPLIT + LET sb == n.prefix[mlen + 1] + osuf == IF mlen + 2 > plen THEN <<>> + ELSE SubSeq(n.prefix, mlen + 2, plen) + bpfx == IF mlen = 0 THEN <<>> + ELSE SubSeq(n.prefix, 1, mlen) + kpos == pos + mlen + ns2 == [ns EXCEPT ![nid].prefix = osuf] + \* Check if nid (with new prefix osuf) is collapsible + nid_collapsible == + /\ ~n.is_vis + /\ Cardinality(DOMAIN n.children) = 1 + /\ LET cd == CHOOSE b \in DOMAIN n.children : TRUE + cid == n.children[cd] + IN /\ cid \in DOMAIN ns + /\ Len(osuf) + 1 + Len(ns[cid].prefix) <= PrefixCapacity + IN + IF kpos > Len(key) THEN + LET bid == nx + bn == [prefix |-> bpfx, children |-> (sb :> nid), is_vis |-> TRUE] + raw == <<(bid :> bn) @@ ns2, IF nid = rt THEN bid ELSE rt, nx + 1, bid>> + IN IF nid_collapsible THEN + LET cd == CHOOSE b \in DOMAIN n.children : TRUE + cid == n.children[cd] + new_pfx == osuf \o <> \o ns[cid].prefix + ns_c == [nd \in (DOMAIN raw[1] \ {nid}) |-> + IF nd = cid + THEN [raw[1][cid] EXCEPT !.prefix = new_pfx] + ELSE raw[1][nd]] + ns_d == [ns_c EXCEPT ![bid].children = (sb :> cid)] + IN <> + ELSE raw + ELSE + LET kd == key[kpos] + ch == MkChain(key, kpos + 1, nx + 1) + bid == nx + bc == (sb :> nid) @@ (kd :> ch[2]) + bn == [prefix |-> bpfx, children |-> bc, is_vis |-> FALSE] + raw == <<(bid :> bn) @@ ch[1] @@ ns2, + IF nid = rt THEN bid ELSE rt, ch[3], bid>> + IN IF nid_collapsible THEN + LET cd == CHOOSE b \in DOMAIN n.children : TRUE + cid == n.children[cd] + new_pfx == osuf \o <> \o ns[cid].prefix + ns_c == [nd \in (DOMAIN raw[1] \ {nid}) |-> + IF nd = cid + THEN [raw[1][cid] EXCEPT !.prefix = new_pfx] + ELSE raw[1][nd]] + ns_d == [ns_c EXCEPT ![bid].children[sb] = cid] + IN <> + ELSE raw + ELSE + \* FULL PREFIX MATCH + LET ap == pos + plen IN + IF ap > Len(key) THEN + <<[ns EXCEPT ![nid].is_vis = TRUE], rt, nx, nid>> + ELSE + LET d == key[ap] IN + IF d \in DOMAIN n.children THEN + LET cid == n.children[d] + sub == DoInsert(ns, rt, key, ap + 1, cid, nx) + ns1 == IF sub[4] /= cid + THEN [sub[1] EXCEPT ![nid].children[d] = sub[4]] + ELSE sub[1] + \* Check if nid is now collapsible + n1 == ns1[nid] + single == Cardinality(DOMAIN n1.children) = 1 + /\ ~n1.is_vis /\ nid /= sub[2] + IN + IF single THEN + LET cd2 == CHOOSE b \in DOMAIN n1.children : TRUE + cid2 == n1.children[cd2] + combined == Len(n1.prefix) + 1 + Len(ns1[cid2].prefix) + IN + IF combined <= PrefixCapacity THEN + LET new_pfx == n1.prefix \o <> \o ns1[cid2].prefix + ns2 == [nd \in (DOMAIN ns1 \ {nid}) |-> + IF nd = cid2 + THEN [ns1[cid2] EXCEPT !.prefix = new_pfx] + ELSE ns1[nd]] + IN <> + ELSE <> + ELSE <> + ELSE + LET ch == MkChain(key, ap + 1, nx) + ns2 == [ns EXCEPT ![nid].children = n.children @@ (d :> ch[2])] + IN <> + +(***************************************************************************) +(* INSERT — Top-level Action *) +(***************************************************************************) + +Insert(key) == + /\ key \notin present + /\ IF root = NULL THEN + LET ch == MkChain(key, 1, nxt) + IN /\ nodes' = ch[1] + /\ root' = ch[2] + /\ present' = present \union {key} + /\ nxt' = ch[3] + ELSE + LET r == DoInsert(nodes, root, key, 1, root, nxt) + IN /\ nodes' = r[1] + /\ root' = r[2] + /\ present' = present \union {key} + /\ nxt' = r[3] + +(***************************************************************************) +(* REMOVE — Path Tracing *) +(***************************************************************************) + +\* Returns <<..., <>, ...>>. dispatch=0 means VIS at nid. +RECURSIVE TraceFrom(_, _, _, _) +TraceFrom(ns, nid, key, pos) == + IF nid \notin DOMAIN ns THEN <<>> + ELSE + LET n == ns[nid] + plen == Len(n.prefix) + IN + IF plen > Len(key) - pos + 1 THEN <<>> + ELSE IF plen > 0 /\ SubSeq(key, pos, pos + plen - 1) /= n.prefix THEN <<>> + ELSE + LET ap == pos + plen IN + IF ap > Len(key) THEN + IF n.is_vis THEN <<<>>> ELSE <<>> + ELSE + LET d == key[ap] IN + IF d \notin DOMAIN n.children THEN <<>> + ELSE + LET cid == n.children[d] + rest == TraceFrom(ns, cid, key, ap + 1) + IN + IF rest /= <<>> THEN <<<>>> \o rest + ELSE + \* Check if child is terminal leaf + IF cid \in DOMAIN ns + /\ ns[cid].is_vis + /\ Len(ns[cid].prefix) = 0 + /\ ap + 1 > Len(key) + THEN <<<>>> + ELSE <<>> + +(***************************************************************************) +(* REMOVE — Collapse *) +(***************************************************************************) + +CollapseOp(ns, rt, nid, parent_id, d_to_nid) == + IF nid = NULL \/ nid \notin DOMAIN ns THEN <> + ELSE IF Cardinality(DOMAIN ns[nid].children) /= 1 THEN <> + ELSE IF ns[nid].is_vis THEN <> \* Node has VIS + 1 child = 2 occupants, not single-child + ELSE IF nid = rt THEN <> + ELSE + LET n == ns[nid] + cd == CHOOSE b \in DOMAIN n.children : TRUE + cid == n.children[cd] + IN + IF cid \notin DOMAIN ns THEN <> + ELSE + LET child == ns[cid] + combined == Len(n.prefix) + 1 + Len(child.prefix) + IN + IF combined > PrefixCapacity THEN <> + ELSE + LET new_pfx == n.prefix \o <> \o child.prefix + new_vis == child.is_vis + upd == [child EXCEPT !.prefix = new_pfx] + ns2 == [nd \in (DOMAIN ns \ {nid}) |-> + IF nd = cid THEN upd ELSE ns[nd]] + ns3 == IF parent_id = NULL THEN ns2 + ELSE [ns2 EXCEPT + ![parent_id].children[d_to_nid] = cid] + IN <> + +(***************************************************************************) +(* REMOVE — Cleanup (remove empty non-VIS nodes up the path) *) +(***************************************************************************) + +\* After removing a child, clean up: if node is now childless and non-VIS, +\* remove it from its parent too. Then try collapse on the resulting parent. +\* path = full path, idx = index of node to check, ns = current node map +RECURSIVE CleanUp(_, _, _, _) +CleanUp(ns, rt, path, idx) == + IF idx < 1 THEN <> + ELSE + LET nid == path[idx][1] IN + IF nid \notin DOMAIN ns THEN <> + ELSE + LET n == ns[nid] IN + IF DOMAIN n.children = {} /\ ~n.is_vis THEN + \* Dead node — remove it + IF nid = rt THEN + \* Dead root — tree becomes empty + <<[nd \in (DOMAIN ns \ {nid}) |-> ns[nd]], NULL>> + ELSE IF idx = 1 THEN + \* Root-level entry with no parent in path + <<[nd \in (DOMAIN ns \ {nid}) |-> ns[nd]], NULL>> + ELSE + LET pid == path[idx - 1][1] + pd == path[idx - 1][2] + ns2 == [nd \in (DOMAIN ns \ {nid}) |-> ns[nd]] + ns3 == [ns2 EXCEPT ![pid].children = + [b \in (DOMAIN ns2[pid].children \ {pd}) |-> + ns2[pid].children[b]]] + IN CleanUp(ns3, rt, path, idx - 1) + ELSE + \* Node is alive — try collapse + LET gpid == IF idx >= 2 THEN path[idx - 1][1] ELSE NULL + gpd == IF idx >= 2 THEN path[idx - 1][2] ELSE 0 + IN CollapseOp(ns, rt, nid, gpid, gpd) + +(***************************************************************************) +(* REMOVE — Top-level Action *) +(***************************************************************************) + +Remove(key) == + /\ key \in present + /\ root /= NULL + /\ LET path == TraceFrom(nodes, root, key, 1) IN + /\ path /= <<>> + /\ LET last == path[Len(path)] + last_nid == last[1] + last_d == last[2] + IN + IF last_d = 0 THEN + \* Key is VIS at last_nid + LET n == nodes[last_nid] IN + IF DOMAIN n.children = {} THEN + \* Leaf VIS — remove node + IF last_nid = root THEN + /\ nodes' = EmptyFcn + /\ root' = NULL + /\ present' = present \ {key} + /\ nxt' = nxt + ELSE + LET pe == path[Len(path) - 1] + pid == pe[1] + pd == pe[2] + ns2 == [nd \in (DOMAIN nodes \ {last_nid}) |-> nodes[nd]] + ns3 == [ns2 EXCEPT ![pid].children = + [b \in (DOMAIN ns2[pid].children \ {pd}) |-> + ns2[pid].children[b]]] + cl == CleanUp(ns3, root, path, Len(path) - 1) + IN + /\ nodes' = cl[1] + /\ root' = cl[2] + /\ present' = present \ {key} + /\ nxt' = nxt + ELSE + \* Internal VIS — clear flag, then clean up if needed + LET ns2 == [nodes EXCEPT ![last_nid].is_vis = FALSE] IN + IF Cardinality(DOMAIN n.children) = 1 THEN + \* Became single-child non-VIS — try collapse + LET gpid == IF Len(path) >= 2 + THEN path[Len(path) - 1][1] ELSE NULL + gpd == IF Len(path) >= 2 + THEN path[Len(path) - 1][2] ELSE 0 + cl == CollapseOp(ns2, root, last_nid, gpid, gpd) + IN + /\ nodes' = cl[1] + /\ root' = cl[2] + /\ present' = present \ {key} + /\ nxt' = nxt + ELSE + /\ nodes' = ns2 + /\ root' = root + /\ present' = present \ {key} + /\ nxt' = nxt + ELSE + \* Key ends at leaf child via dispatch last_d + LET leaf_id == nodes[last_nid].children[last_d] + ns2 == [nd \in (DOMAIN nodes \ {leaf_id}) |-> nodes[nd]] + ns3 == [ns2 EXCEPT ![last_nid].children = + [b \in (DOMAIN ns2[last_nid].children \ {last_d}) |-> + ns2[last_nid].children[b]]] + cl == CleanUp(ns3, root, path, Len(path)) + IN + /\ nodes' = cl[1] + /\ root' = cl[2] + /\ present' = present \ {key} + /\ nxt' = nxt + +(***************************************************************************) +(* SPECIFICATION *) +(***************************************************************************) + +Init == + /\ nodes = EmptyFcn + /\ root = NULL + /\ present = {} + /\ nxt = 1 + +Next == + \/ \E key \in Keys : Insert(key) + \/ \E key \in Keys : Remove(key) + +Spec == Init /\ [][Next]_vars + +(***************************************************************************) +(* INVARIANTS *) +(***************************************************************************) + +NoOrphans == + IF root = NULL THEN DOMAIN nodes = {} + ELSE DOMAIN nodes = Reachable(root) + +KeyPreservation == + \A key \in present : root /= NULL /\ KeyAt(root, key, 1) + +WellFormed == + \A nid \in DOMAIN nodes : + (Cardinality(DOMAIN nodes[nid].children) = 1 /\ nid /= root + /\ ~nodes[nid].is_vis) => + LET cd == CHOOSE b \in DOMAIN nodes[nid].children : TRUE + cid == nodes[nid].children[cd] + IN + \/ cid \notin DOMAIN nodes + \/ Len(nodes[nid].prefix) + 1 + Len(nodes[cid].prefix) > PrefixCapacity + +TypeOK == + /\ root \in (DOMAIN nodes) \union {NULL} + /\ present \subseteq Keys + /\ nxt \in Nat \ {0} + /\ \A nid \in DOMAIN nodes : + /\ \A i \in 1..Len(nodes[nid].prefix) : + nodes[nid].prefix[i] \in Alphabet + /\ nodes[nid].is_vis \in BOOLEAN + /\ \A b \in DOMAIN nodes[nid].children : + /\ b \in Alphabet + /\ nodes[nid].children[b] \in DOMAIN nodes + +StateConstraint == nxt <= 7 + +(***************************************************************************) +(* BUGGY INSERT — No ancestor collapse on unwind *) +(* *) +(* Models the real implementation's iterative insert which does NOT check *) +(* whether ancestors became collapsible after a prefix split deeper in *) +(* the tree. *) +(***************************************************************************) + +RECURSIVE BuggyDoInsert(_, _, _, _, _, _) +BuggyDoInsert(ns, rt, key, pos, nid, nx) == + LET n == ns[nid] + plen == Len(n.prefix) + key_rem == Len(key) - pos + 1 + match_max == IF plen < key_rem THEN plen ELSE key_rem + RECURSIVE PfxMatch(_) + PfxMatch(i) == + IF i > match_max THEN match_max + ELSE IF key[pos + i - 1] /= n.prefix[i] THEN i - 1 + ELSE PfxMatch(i + 1) + mlen == IF plen = 0 THEN 0 ELSE PfxMatch(1) + IN + IF mlen < plen THEN + \* PREFIX SPLIT — identical to correct version + LET sb == n.prefix[mlen + 1] + osuf == IF mlen + 2 > plen THEN <<>> + ELSE SubSeq(n.prefix, mlen + 2, plen) + bpfx == IF mlen = 0 THEN <<>> + ELSE SubSeq(n.prefix, 1, mlen) + kpos == pos + mlen + ns2 == [ns EXCEPT ![nid].prefix = osuf] + nid_collapsible == + /\ ~n.is_vis + /\ Cardinality(DOMAIN n.children) = 1 + /\ LET cd == CHOOSE b \in DOMAIN n.children : TRUE + cid == n.children[cd] + IN /\ cid \in DOMAIN ns + /\ Len(osuf) + 1 + Len(ns[cid].prefix) <= PrefixCapacity + IN + IF kpos > Len(key) THEN + LET bid == nx + bn == [prefix |-> bpfx, children |-> (sb :> nid), is_vis |-> TRUE] + raw == <<(bid :> bn) @@ ns2, IF nid = rt THEN bid ELSE rt, nx + 1, bid>> + IN IF nid_collapsible THEN + LET cd == CHOOSE b \in DOMAIN n.children : TRUE + cid == n.children[cd] + new_pfx == osuf \o <> \o ns[cid].prefix + ns_c == [nd \in (DOMAIN raw[1] \ {nid}) |-> + IF nd = cid + THEN [raw[1][cid] EXCEPT !.prefix = new_pfx] + ELSE raw[1][nd]] + ns_d == [ns_c EXCEPT ![bid].children = (sb :> cid)] + IN <> + ELSE raw + ELSE + LET kd == key[kpos] + ch == MkChain(key, kpos + 1, nx + 1) + bid == nx + bc == (sb :> nid) @@ (kd :> ch[2]) + bn == [prefix |-> bpfx, children |-> bc, is_vis |-> FALSE] + raw == <<(bid :> bn) @@ ch[1] @@ ns2, + IF nid = rt THEN bid ELSE rt, ch[3], bid>> + IN IF nid_collapsible THEN + LET cd == CHOOSE b \in DOMAIN n.children : TRUE + cid == n.children[cd] + new_pfx == osuf \o <> \o ns[cid].prefix + ns_c == [nd \in (DOMAIN raw[1] \ {nid}) |-> + IF nd = cid + THEN [raw[1][cid] EXCEPT !.prefix = new_pfx] + ELSE raw[1][nd]] + ns_d == [ns_c EXCEPT ![bid].children[sb] = cid] + IN <> + ELSE raw + ELSE + \* FULL PREFIX MATCH + LET ap == pos + plen IN + IF ap > Len(key) THEN + <<[ns EXCEPT ![nid].is_vis = TRUE], rt, nx, nid>> + ELSE + LET d == key[ap] IN + IF d \in DOMAIN n.children THEN + \* BUG: No ancestor collapse check after recursive return + LET cid == n.children[d] + sub == BuggyDoInsert(ns, rt, key, ap + 1, cid, nx) + ns1 == IF sub[4] /= cid + THEN [sub[1] EXCEPT ![nid].children[d] = sub[4]] + ELSE sub[1] + IN <> + ELSE + LET ch == MkChain(key, ap + 1, nx) + ns2 == [ns EXCEPT ![nid].children = n.children @@ (d :> ch[2])] + IN <> + +BuggyInsert(key) == + /\ key \notin present + /\ IF root = NULL THEN + LET ch == MkChain(key, 1, nxt) + IN /\ nodes' = ch[1] + /\ root' = ch[2] + /\ present' = present \union {key} + /\ nxt' = ch[3] + ELSE + LET r == BuggyDoInsert(nodes, root, key, 1, root, nxt) + IN /\ nodes' = r[1] + /\ root' = r[2] + /\ present' = present \union {key} + /\ nxt' = r[3] + +BuggyNext == + \/ \E key \in Keys : BuggyInsert(key) + \/ \E key \in Keys : Remove(key) + +BuggySpec == Init /\ [][BuggyNext]_vars + +================================================================================ diff --git a/spec/tla/ARTTreeMaintenance_NoAncestorCollapse.cfg b/spec/tla/ARTTreeMaintenance_NoAncestorCollapse.cfg new file mode 100644 index 00000000..f38b7353 --- /dev/null +++ b/spec/tla/ARTTreeMaintenance_NoAncestorCollapse.cfg @@ -0,0 +1,13 @@ +SPECIFICATION BuggySpec + +CONSTANTS + PrefixCapacity = 2 + +INVARIANTS + TypeOK + NoOrphans + KeyPreservation + WellFormed + +CONSTRAINT + StateConstraint diff --git a/spec/tla/Inode256VIS.cfg b/spec/tla/Inode256VIS.cfg new file mode 100644 index 00000000..021fa5ed --- /dev/null +++ b/spec/tla/Inode256VIS.cfg @@ -0,0 +1,14 @@ +SPECIFICATION Spec + +CONSTANTS + N = 4 + Values = {0, 1, 2} + +INVARIANTS + CorrectScanInvariant + BitmaskConsistency + IteratorSafety + +\* This invariant should be VIOLATED — demonstrates the bug with nullptr-only checks. +\* Uncomment to see the counterexample: +\* INVARIANT BuggyScanInvariant diff --git a/spec/tla/Inode256VIS.tla b/spec/tla/Inode256VIS.tla new file mode 100644 index 00000000..39ce4547 --- /dev/null +++ b/spec/tla/Inode256VIS.tla @@ -0,0 +1,112 @@ +--------------------------- MODULE Inode256VIS --------------------------- +\* TLA+ specification for inode256 value-in-slot (VIS) correctness. +\* +\* Models a single inode256 with N slots. Each slot is either: +\* - Empty (no child, no value) +\* - Pointer (holds a child node reference) +\* - Value (holds a packed user value, bitmask bit set) +\* +\* Key invariant: every scan for "occupied" slots must find exactly +\* the union of pointer-slots and value-slots. With bitmask-only +\* encoding, pack(0) = 0 = NULL, so `slot[i] # 0` is INSUFFICIENT. +\* +\* Domain: N=4 slots, values in {0,1,2}, pointers in {-1,-2,-3,-4}. +\* NULL = 0. Pointers are negative (always non-zero). Values are >= 0. + +EXTENDS Integers, FiniteSets + +CONSTANTS + N, \* Number of slots (4 for model checking) + Values \* Set of user values (e.g., {0, 1, 2}) + +VARIABLES + slot, \* slot[i] \in Int (0=NULL, <0=pointer, >=0=packed value) + bitmask, \* bitmask[i] \in BOOLEAN (TRUE = value-in-slot) + hasPtr \* hasPtr[i] \in BOOLEAN (TRUE = slot holds a pointer) + +NULL == 0 +Pointers == {-1, -2, -3, -4} +Pack(v) == v \* Identity encoding. pack(0) = 0 = NULL. +Slots == 1..N +vars == <> + +----------------------------------------------------------------------------- +\* PREDICATES + +\* Ground truth: a slot is occupied if it holds a pointer OR a value. +Occupied(i) == hasPtr[i] \/ bitmask[i] + +OccupiedSet == {i \in Slots : Occupied(i)} + +\* BUGGY: nullptr check only. Misses value=0 slots. +BuggyOccupied(i) == slot[i] # NULL + +BuggyOccupiedSet == {i \in Slots : BuggyOccupied(i)} + +\* CORRECT: nullptr OR bitmask. +CorrectOccupied(i) == slot[i] # NULL \/ bitmask[i] + +CorrectOccupiedSet == {i \in Slots : CorrectOccupied(i)} + +----------------------------------------------------------------------------- +\* INITIAL STATE + +Init == + /\ slot = [i \in Slots |-> NULL] + /\ bitmask = [i \in Slots |-> FALSE] + /\ hasPtr = [i \in Slots |-> FALSE] + +----------------------------------------------------------------------------- +\* OPERATIONS + +InsertValue(i, v) == + /\ ~Occupied(i) + /\ slot' = [slot EXCEPT ![i] = Pack(v)] + /\ bitmask' = [bitmask EXCEPT ![i] = TRUE] + /\ hasPtr' = [hasPtr EXCEPT ![i] = FALSE] + +InsertPointer(i, p) == + /\ ~Occupied(i) + /\ p \in Pointers + /\ slot' = [slot EXCEPT ![i] = p] + /\ bitmask' = [bitmask EXCEPT ![i] = FALSE] + /\ hasPtr' = [hasPtr EXCEPT ![i] = TRUE] + +Remove(i) == + /\ Occupied(i) + /\ slot' = [slot EXCEPT ![i] = NULL] + /\ bitmask' = [bitmask EXCEPT ![i] = FALSE] + /\ hasPtr' = [hasPtr EXCEPT ![i] = FALSE] + +----------------------------------------------------------------------------- +\* NEXT STATE + +Step == + \/ \E i \in Slots, v \in Values : InsertValue(i, v) + \/ \E i \in Slots, p \in Pointers : InsertPointer(i, p) + \/ \E i \in Slots : Remove(i) + +Spec == Init /\ [][Step]_vars + +----------------------------------------------------------------------------- +\* INVARIANTS + +\* The correct check (slot#NULL \/ bitmask) matches ground truth. +CorrectScanInvariant == CorrectOccupiedSet = OccupiedSet + +\* The buggy check (slot#NULL only) should be VIOLATED by TLC. +BuggyScanInvariant == BuggyOccupiedSet = OccupiedSet + +\* Structural consistency of the state. +BitmaskConsistency == + \A i \in Slots : + /\ (bitmask[i] => ~hasPtr[i]) + /\ (hasPtr[i] => ~bitmask[i]) + /\ (hasPtr[i] => slot[i] \in Pointers) + /\ (~Occupied(i) => slot[i] = NULL) + +\* Iterator safety: value slots are never pointers. +IteratorSafety == + \A i \in Slots : (bitmask[i] => ~hasPtr[i]) + +============================================================================= diff --git a/spec/tla/Inode256VIS_BugDemo.cfg b/spec/tla/Inode256VIS_BugDemo.cfg new file mode 100644 index 00000000..e6ebef51 --- /dev/null +++ b/spec/tla/Inode256VIS_BugDemo.cfg @@ -0,0 +1,11 @@ +\* This config demonstrates the VIS bug: BuggyScanInvariant will be VIOLATED. +\* The counterexample shows: insert value 0 into a slot → pack(0) = NULL → +\* buggy nullptr-only scan misses the slot. + +SPECIFICATION Spec + +CONSTANTS + N = 4 + Values = {0, 1, 2} + +INVARIANT BuggyScanInvariant diff --git a/spec/tla/OLCChainCut.cfg b/spec/tla/OLCChainCut.cfg new file mode 100644 index 00000000..1eb5ce94 --- /dev/null +++ b/spec/tla/OLCChainCut.cfg @@ -0,0 +1,17 @@ +\* OLCChainCut model configuration + +SPECIFICATION Spec + +CONSTANTS + MaxVersion = 6 + +CONSTRAINT + StateConstraint + +CHECK_DEADLOCK FALSE + +INVARIANTS + TypeOK + RemoverLockedImpliesChainSingle + ParentNotEmpty + GPConnected diff --git a/spec/tla/OLCChainCut.tla b/spec/tla/OLCChainCut.tla new file mode 100644 index 00000000..087f3882 --- /dev/null +++ b/spec/tla/OLCChainCut.tla @@ -0,0 +1,249 @@ +--------------------------- MODULE OLCChainCut ---------------------------- +(* OLC (Optimistic Lock Coupling) chain-cut protocol. + Models a remover thread cutting a child node from a parent in a B+-tree + with optimistic lock coupling, and a concurrent inserter that can target + the parent or grandparent node. + + Fix M1: RemoverLockedImpliesChainSingle replaces trivially-true ChainLockValid. + Fix M4: Grandparent node added to model Step 4.1 acquisition. *) + +EXTENDS Naturals, TLC + +CONSTANTS MaxVersion + +VARIABLES + (* Remover state *) + rpc, \* remover program counter + r_chain_locked, \* remover holds chain lock on child + r_p_ver_snap, \* remover's snapshot of parent version + r_gp_ver_snap, \* remover's snapshot of grandparent version + + (* Parent node *) + p_ver, \* parent version (odd = locked) + p_count, \* number of children in parent + + (* Child node *) + c_count, \* number of entries in child (chain length proxy) + + (* Grandparent node *) + gp_ver, \* grandparent version (odd = locked) + gp_child, \* grandparent points to parent (TRUE = connected) + + (* Inserter state *) + ipc, \* inserter program counter + i_target \* inserter's target: "parent" | "grandparent" + +vars == <> + +----------------------------------------------------------------------------- +(* Initial state *) + +Init == + /\ rpc = "start" + /\ r_chain_locked = FALSE + /\ r_p_ver_snap = 0 + /\ r_gp_ver_snap = 0 + /\ p_ver = 0 + /\ p_count = 2 + /\ c_count = 1 + /\ gp_ver = 0 + /\ gp_child = TRUE + /\ ipc = "idle" + /\ i_target = "parent" + +----------------------------------------------------------------------------- +(* Remover actions *) + +(* Step 1: Read parent version optimistically *) +ReadParentVer == + /\ rpc = "start" + /\ p_ver % 2 = 0 \* parent not locked + /\ rpc' = "read_parent" + /\ r_p_ver_snap' = p_ver + /\ UNCHANGED <> + +(* Step 2: Lock the chain (child) *) +LockChain == + /\ rpc = "read_parent" + /\ rpc' = "validate_parent" + /\ r_chain_locked' = TRUE + /\ c_count' = 1 \* chain is single node once locked + /\ UNCHANGED <> + +(* Step 3: Validate parent version unchanged *) +ValidateParent == + /\ rpc = "validate_parent" + /\ IF p_ver = r_p_ver_snap /\ p_ver % 2 = 0 + THEN rpc' = "case_a" + ELSE rpc' = "restart" \* validation failed, must restart + /\ UNCHANGED <> + +(* Step 4a: Lock parent (case_a) *) +LockParent == + /\ rpc = "case_a" + /\ p_ver % 2 = 0 \* parent not already locked + /\ p_ver' = p_ver + 1 \* lock parent (make odd) + /\ IF p_count = 2 + THEN rpc' = "acquire_gp" \* parent will shrink, need grandparent + ELSE rpc' = "cut" \* no shrink needed, proceed to cut + /\ UNCHANGED <> + +(* Step 4.1: Acquire grandparent lock (needed when parent will shrink) *) +AcquireGP == + /\ rpc = "acquire_gp" + /\ IF gp_ver % 2 = 0 + THEN /\ gp_ver' = gp_ver + 1 \* lock grandparent + /\ r_gp_ver_snap' = gp_ver + /\ rpc' = "cut" + ELSE /\ rpc' = "gp_failed" \* grandparent busy, must release all + /\ gp_ver' = gp_ver + /\ r_gp_ver_snap' = r_gp_ver_snap + /\ UNCHANGED <> + +(* Grandparent acquisition failed: release all locks and restart *) +GPFailed == + /\ rpc = "gp_failed" + /\ rpc' = "restart" + /\ p_ver' = p_ver + 1 \* unlock parent (make even again) + /\ UNCHANGED <> + +(* Step 5: Perform the cut *) +Cut == + /\ rpc = "cut" + /\ p_count' = p_count - 1 + /\ rpc' = "unlock" + /\ UNCHANGED <> + +(* Step 6: Unlock parent (and grandparent if held) *) +Unlock == + /\ rpc = "unlock" + /\ p_ver' = p_ver + 1 \* unlock parent (make even) + /\ IF r_gp_ver_snap /= 0 + THEN gp_ver' = gp_ver + 1 \* unlock grandparent + ELSE gp_ver' = gp_ver + /\ r_chain_locked' = FALSE + /\ r_gp_ver_snap' = 0 + /\ rpc' = "done" + /\ UNCHANGED <> + +(* Restart: release chain lock and go back to start *) +Restart == + /\ rpc = "restart" + /\ r_chain_locked' = FALSE + /\ rpc' = "start" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Inserter actions — concurrent thread that can insert into parent or gp *) + +InsertChoose == + /\ ipc = "idle" + /\ \E t \in {"parent", "grandparent"} : + /\ i_target' = t + /\ ipc' = "insert" + /\ UNCHANGED <> + +InsertParent == + /\ ipc = "insert" + /\ i_target = "parent" + /\ p_ver % 2 = 0 \* parent not locked + /\ p_ver' = p_ver + 2 \* bump version (lock+unlock) + /\ p_count' = p_count + 1 + /\ ipc' = "insert_done" + /\ UNCHANGED <> + +InsertGrandparent == + /\ ipc = "insert" + /\ i_target = "grandparent" + /\ gp_ver % 2 = 0 \* grandparent not locked + /\ gp_ver' = gp_ver + 2 \* bump version (lock+unlock) + /\ ipc' = "insert_done" + /\ UNCHANGED <> + +(* Inserter cycles back to idle *) +InsertDone == + /\ ipc = "insert_done" + /\ ipc' = "idle" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Next-state relation *) + +RemoverNext == + \/ ReadParentVer + \/ LockChain + \/ ValidateParent + \/ LockParent + \/ AcquireGP + \/ GPFailed + \/ Cut + \/ Unlock + \/ Restart + +InserterNext == + \/ InsertChoose + \/ InsertParent + \/ InsertGrandparent + \/ InsertDone + +Next == RemoverNext \/ InserterNext + +Spec == Init /\ [][Next]_vars + +----------------------------------------------------------------------------- +(* State constraint for bounded model checking *) + +StateConstraint == + /\ p_ver <= MaxVersion + /\ p_count >= 1 + /\ p_count <= 4 + /\ gp_ver <= MaxVersion + +----------------------------------------------------------------------------- +(* Invariants *) + +TypeOK == + /\ rpc \in {"start", "read_parent", "validate_parent", + "case_a", "acquire_gp", "gp_failed", + "cut", "unlock", "restart", "done"} + /\ r_chain_locked \in BOOLEAN + /\ r_p_ver_snap \in Nat + /\ r_gp_ver_snap \in Nat + /\ p_ver \in Nat + /\ p_count \in Nat + /\ c_count \in Nat + /\ gp_ver \in Nat + /\ gp_child \in BOOLEAN + /\ ipc \in {"idle", "insert", "insert_done"} + /\ i_target \in {"parent", "grandparent"} + +(* M1: Stronger invariant — when remover holds chain lock and is in + an active removal state, the chain must be a single node. *) +RemoverLockedImpliesChainSingle == + (r_chain_locked /\ rpc \in {"read_parent", "validate_parent", "case_a", "case_b", "case_c", "cut"}) + => c_count = 1 + +(* Safety: parent count never drops below 1 *) +ParentNotEmpty == + p_count >= 1 + +(* Grandparent always points to parent *) +GPConnected == + gp_child = TRUE + +============================================================================= diff --git a/spec/tla/OLCChainCutFull.cfg b/spec/tla/OLCChainCutFull.cfg new file mode 100644 index 00000000..305ff38d --- /dev/null +++ b/spec/tla/OLCChainCutFull.cfg @@ -0,0 +1,16 @@ +SPECIFICATION Spec + +CONSTANTS + MaxVersion = 4 + OBSOLETE = 99 + +INVARIANTS + CutSafety + WellFormedness + RootEmptyOnlyWhenFullCut + ShrinkCorrectness + +CONSTRAINT + StateConstraint + +CHECK_DEADLOCK FALSE diff --git a/spec/tla/OLCChainCutFull.tla b/spec/tla/OLCChainCutFull.tla new file mode 100644 index 00000000..070c1a02 --- /dev/null +++ b/spec/tla/OLCChainCutFull.tla @@ -0,0 +1,410 @@ +--------------------------- MODULE OLCChainCutFull ------------------------ +\* Stage 10: Full chain cut algorithm covering all critical paths. +\* +\* Topology: root_ptr → gp → parent → chain → (leaf, implicit) +\* - root_ptr: separate lock (not a node), can be CPP if chain extends to gp +\* - gp: can become single-child (Case B extends chain to include parent) +\* - parent: the initial CPP candidate (2+ children) +\* - chain: single-child I4 (the chain being cut) +\* +\* Paths exercised: +\* P1: Normal cut — parent is CPP, no shrink needed +\* P2: Parent needs shrink — acquire gp as grandparent, collapse +\* P3: Case B — parent became single-child, chain extends up +\* P4: Cascading Case B — gp also single-child, cut_level reaches 0 (root) +\* P5: Root as CPP — set root=nullptr (tree emptied) +\* P6: Grandparent acquisition fails — restart +\* P7: Case C — child pointer gone, restart +\* +\* Concurrent inserter can add children to parent or gp (breaking Case B, +\* preventing shrink, etc.) + +EXTENDS Integers + +CONSTANTS MaxVersion, OBSOLETE + +VARIABLES + \* Root pointer (separate lock, not a node) + root_ver, \* root pointer lock version + root_child, \* root points to gp (TRUE/FALSE, FALSE = tree empty) + + \* Grandparent node + gp_count, \* 1..3 + gp_child, \* gp points to parent (TRUE) + gp_ver, + + \* Parent node (initial CPP candidate) + p_count, \* 1..3 + p_child, \* parent points to chain (TRUE) + p_ver, + + \* Chain node + c_ver, + + \* Remover state + rpc, + r_cut_level, \* 0=root is CPP, 1=gp is CPP, 2=parent is CPP, 3=chain-only + r_chain_locked, + r_parent_locked, + r_gp_locked, + r_cpp_locked, \* TRUE when CPP write guard held + r_needs_shrink, \* TRUE if CPP needs shrink after cut + r_cached_ver, \* cached version for current CPP evaluation + + \* Inserter state + ipc, + i_target \* "parent" or "gp" + +vars == <> + +UNCHANGED_inserter == UNCHANGED <> +UNCHANGED_shared == UNCHANGED <> + +----------------------------------------------------------------------------- +Init == + /\ root_ver = 0 /\ root_child = TRUE + /\ gp_count \in {1, 2} /\ gp_child = TRUE /\ gp_ver = 0 + /\ p_count \in {1, 2} /\ p_child = TRUE /\ p_ver = 0 + /\ c_ver = 0 + /\ rpc = "idle" + /\ r_cut_level = 3 /\ r_chain_locked = FALSE + /\ r_parent_locked = FALSE /\ r_gp_locked = FALSE + /\ r_cpp_locked = FALSE /\ r_needs_shrink = FALSE /\ r_cached_ver = 0 + /\ ipc = "idle" /\ i_target = "parent" + +----------------------------------------------------------------------------- +\* REMOVER + +\* Step 2: Lock chain node +RLockChain == + /\ rpc = "idle" + /\ c_ver % 2 = 0 + /\ c_ver # OBSOLETE \* not already obsoleted + /\ p_child = TRUE \* chain still connected (not already cut) + /\ c_ver' = c_ver + 1 + /\ r_chain_locked' = TRUE + /\ r_cut_level' = 3 \* start: only chain locked + /\ rpc' = "eval_parent" + /\ UNCHANGED <> + +\* Step 3: Evaluate parent as CPP candidate +REvalParent == + /\ rpc = "eval_parent" + /\ r_cached_ver' = p_ver + /\ rpc' = "validate_parent" + /\ UNCHANGED <> + +RValidateParent == + /\ rpc = "validate_parent" + /\ IF p_ver = r_cached_ver /\ p_ver % 2 = 0 + THEN IF ~p_child + THEN rpc' = "restart" \* Case C + ELSE IF p_count = 1 + THEN rpc' = "case_b_parent" \* Case B: parent is single-child + ELSE rpc' = "upgrade_parent" \* Case A: parent is CPP + ELSE rpc' = "eval_parent" \* stale, re-read + /\ UNCHANGED <> + +\* Case A: lock parent as CPP +RUpgradeParent == + /\ rpc = "upgrade_parent" + /\ IF p_ver = r_cached_ver /\ p_ver % 2 = 0 + THEN /\ p_ver' = p_ver + 1 + /\ r_cpp_locked' = TRUE + /\ r_cut_level' = 2 \* parent is CPP + /\ rpc' = "check_shrink" + ELSE /\ rpc' = "eval_parent" + /\ UNCHANGED <> + /\ UNCHANGED <> + +\* Case B: parent became single-child → lock it as chain member, eval gp +RCaseBParent == + /\ rpc = "case_b_parent" + /\ IF p_ver = r_cached_ver /\ p_ver % 2 = 0 + THEN /\ p_ver' = p_ver + 1 \* lock parent as chain member + /\ r_parent_locked' = TRUE + /\ rpc' = "eval_gp" + ELSE /\ rpc' = "eval_parent" \* retry + /\ UNCHANGED <> + /\ UNCHANGED <> + +\* Evaluate gp as CPP (after Case B on parent) +REvalGP == + /\ rpc = "eval_gp" + /\ r_cached_ver' = gp_ver + /\ rpc' = "validate_gp" + /\ UNCHANGED <> + +RValidateGP == + /\ rpc = "validate_gp" + /\ IF gp_ver = r_cached_ver /\ gp_ver % 2 = 0 + THEN IF ~gp_child + THEN rpc' = "restart" \* Case C at gp level + ELSE IF gp_count = 1 + THEN rpc' = "case_b_gp" \* Cascading Case B! + ELSE rpc' = "upgrade_gp" \* Case A at gp level + ELSE rpc' = "eval_gp" + /\ UNCHANGED <> + +\* Case A at gp: lock gp as CPP +RUpgradeGP == + /\ rpc = "upgrade_gp" + /\ IF gp_ver = r_cached_ver /\ gp_ver % 2 = 0 + THEN /\ gp_ver' = gp_ver + 1 + /\ r_cpp_locked' = TRUE + /\ r_cut_level' = 1 \* gp is CPP + /\ rpc' = "check_shrink" + ELSE /\ rpc' = "eval_gp" + /\ UNCHANGED <> + /\ UNCHANGED <> + +\* Cascading Case B: gp also single-child → lock gp, go to root +RCaseBGP == + /\ rpc = "case_b_gp" + /\ IF gp_ver = r_cached_ver /\ gp_ver % 2 = 0 + THEN /\ gp_ver' = gp_ver + 1 \* lock gp as chain member + /\ r_gp_locked' = TRUE + /\ rpc' = "acquire_root" \* root is now CPP + ELSE /\ rpc' = "eval_gp" + /\ UNCHANGED <> + /\ UNCHANGED <> + +\* Root as CPP (cut_level = 0) +RAcquireRoot == + /\ rpc = "acquire_root" + /\ IF root_ver % 2 = 0 + THEN /\ root_ver' = root_ver + 1 + /\ r_cpp_locked' = TRUE + /\ r_cut_level' = 0 + /\ rpc' = "cut" \* root CPP → always cut (no shrink check) + ELSE /\ rpc' = "restart" + /\ UNCHANGED <> + /\ UNCHANGED <> + +\* Check if CPP needs shrink (only for non-root CPP) +RCheckShrink == + /\ rpc = "check_shrink" + /\ IF r_cut_level = 2 + THEN r_needs_shrink' = (p_count <= 2) \* I4 with 2 children → collapse after cut + ELSE r_needs_shrink' = (gp_count <= 2) \* gp is CPP + /\ IF r_needs_shrink' + THEN rpc' = "acquire_gp_for_shrink" + ELSE rpc' = "cut" + /\ UNCHANGED <> + +\* Acquire grandparent for shrink (can fail → restart) +\* When CPP is parent (cut_level=2), grandparent is gp node. +\* When CPP is gp (cut_level=1), grandparent is root pointer. +RAcquireGPForShrink_Parent == + /\ rpc = "acquire_gp_for_shrink" + /\ r_cut_level = 2 + /\ IF gp_ver % 2 = 0 /\ gp_ver <= MaxVersion + THEN /\ gp_ver' = gp_ver + 1 + /\ r_gp_locked' = TRUE + /\ rpc' = "cut" + ELSE /\ rpc' = "restart" + /\ UNCHANGED <> + /\ UNCHANGED <> + +RAcquireGPForShrink_GP == + /\ rpc = "acquire_gp_for_shrink" + /\ r_cut_level = 1 + /\ IF root_ver % 2 = 0 + THEN /\ root_ver' = root_ver + 1 + /\ rpc' = "cut" + ELSE /\ rpc' = "restart" + /\ UNCHANGED root_ver + /\ UNCHANGED <> + +\* CUT — point of no return +RCut == + /\ rpc = "cut" + /\ CASE r_cut_level = 0 -> \* Root is CPP: empty tree + /\ root_child' = FALSE + /\ root_ver' = root_ver + 1 \* unlock root + /\ gp_ver' = OBSOLETE \* obsolete gp + /\ p_ver' = OBSOLETE \* obsolete parent + /\ c_ver' = OBSOLETE \* obsolete chain + /\ UNCHANGED <> + [] r_cut_level = 1 -> \* GP is CPP: remove parent from gp + /\ gp_child' = FALSE + /\ gp_count' = gp_count - 1 + /\ gp_ver' = gp_ver + 1 \* unlock gp + /\ p_ver' = OBSOLETE \* obsolete parent + /\ c_ver' = OBSOLETE \* obsolete chain + /\ UNCHANGED <> + [] r_cut_level = 2 -> \* Parent is CPP: remove chain from parent + /\ p_child' = FALSE + /\ p_count' = p_count - 1 + /\ p_ver' = p_ver + 1 \* unlock parent + /\ c_ver' = OBSOLETE \* obsolete chain + /\ UNCHANGED <> + [] r_cut_level = 3 -> \* Chain-only (no additional chain on stack) + /\ c_ver' = OBSOLETE \* obsolete chain + /\ UNCHANGED <> + /\ r_chain_locked' = FALSE /\ r_parent_locked' = FALSE + /\ r_gp_locked' = FALSE /\ r_cpp_locked' = FALSE + /\ rpc' = "done" + /\ UNCHANGED <> + +\* Restart: release all held locks +RRestart == + /\ rpc = "restart" + /\ c_ver' = IF r_chain_locked THEN c_ver + 1 ELSE c_ver + /\ p_ver' = IF r_parent_locked THEN p_ver + 1 ELSE p_ver + /\ gp_ver' = IF r_gp_locked THEN gp_ver + 1 ELSE gp_ver + /\ root_ver' = IF r_cpp_locked /\ r_cut_level = 0 THEN root_ver + 1 ELSE root_ver + /\ r_chain_locked' = FALSE /\ r_parent_locked' = FALSE + /\ r_gp_locked' = FALSE /\ r_cpp_locked' = FALSE + /\ rpc' = "idle" + /\ UNCHANGED <> + +RDone == + /\ rpc = "done" + /\ rpc' = "idle" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +\* INSERTER: can add children to parent or gp (prevents Case B, prevents shrink) + +IChoose == + /\ ipc = "idle" + /\ \E t \in {"parent", "gp"} : + /\ (t = "parent" => p_count < 3) + /\ (t = "gp" => gp_count < 3) + /\ i_target' = t + /\ ipc' = "lock" + /\ UNCHANGED <> + +ILock == + /\ ipc = "lock" + /\ IF i_target = "parent" + THEN /\ p_ver % 2 = 0 /\ p_ver <= MaxVersion + /\ p_ver' = p_ver + 1 + /\ UNCHANGED gp_ver + ELSE /\ gp_ver % 2 = 0 /\ gp_ver <= MaxVersion + /\ gp_ver' = gp_ver + 1 + /\ UNCHANGED p_ver + /\ ipc' = "write" + /\ UNCHANGED <> + +IWrite == + /\ ipc = "write" + /\ IF i_target = "parent" + THEN /\ p_count' = p_count + 1 /\ UNCHANGED gp_count + ELSE /\ gp_count' = gp_count + 1 /\ UNCHANGED p_count + /\ ipc' = "unlock" + /\ UNCHANGED <> + +IUnlock == + /\ ipc = "unlock" + /\ IF i_target = "parent" + THEN /\ p_ver' = p_ver + 1 /\ UNCHANGED gp_ver + ELSE /\ gp_ver' = gp_ver + 1 /\ UNCHANGED p_ver + /\ ipc' = "idle" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +Step == + \/ RLockChain \/ REvalParent \/ RValidateParent \/ RUpgradeParent + \/ RCaseBParent \/ REvalGP \/ RValidateGP \/ RUpgradeGP + \/ RCaseBGP \/ RAcquireRoot + \/ RCheckShrink \/ RAcquireGPForShrink_Parent \/ RAcquireGPForShrink_GP + \/ RCut \/ RRestart \/ RDone + \/ IChoose \/ ILock \/ IWrite \/ IUnlock + +Spec == Init /\ [][Step]_vars + +StateConstraint == + /\ root_ver <= MaxVersion + /\ (gp_ver # OBSOLETE => gp_ver <= MaxVersion) + /\ (p_ver # OBSOLETE => p_ver <= MaxVersion) + /\ (c_ver # OBSOLETE => c_ver <= MaxVersion) + +----------------------------------------------------------------------------- +\* INVARIANTS + +\* Cut only when appropriate locks held and state valid +CutSafety == + rpc = "cut" => + /\ r_chain_locked + /\ (r_cut_level = 0 => r_cpp_locked) \* root locked + /\ (r_cut_level = 1 => r_cpp_locked) \* gp locked as CPP + /\ (r_cut_level = 2 => r_cpp_locked) \* parent locked as CPP + /\ (r_cut_level <= 1 => r_parent_locked) \* parent locked as chain member + /\ (r_cut_level = 0 => r_gp_locked) \* gp locked as chain member + +\* Well-formedness: counts stay valid +WellFormedness == + /\ gp_count >= 1 + /\ p_count >= 1 + +\* Root emptied only when cut_level=0 AND tree still has content +RootEmptyOnlyWhenFullCut == + (rpc = "cut" /\ r_cut_level = 0) => (root_child = TRUE /\ gp_child = TRUE /\ p_child = TRUE) + +\* Shrink only attempted when CPP will be undersized +ShrinkCorrectness == + rpc = "acquire_gp_for_shrink" => + \/ (r_cut_level = 2 /\ p_count <= 2) + \/ (r_cut_level = 1 /\ gp_count <= 2) + +============================================================================= diff --git a/spec/tla/OLCChainMembership.cfg b/spec/tla/OLCChainMembership.cfg new file mode 100644 index 00000000..777507ba --- /dev/null +++ b/spec/tla/OLCChainMembership.cfg @@ -0,0 +1,10 @@ +SPECIFICATION Spec + +CONSTANTS + MaxVersion = 6 + +INVARIANTS + ChainSafety + NotChainCorrect + +CHECK_DEADLOCK FALSE diff --git a/spec/tla/OLCChainMembership.tla b/spec/tla/OLCChainMembership.tla new file mode 100644 index 00000000..b5860063 --- /dev/null +++ b/spec/tla/OLCChainMembership.tla @@ -0,0 +1,140 @@ +--------------------------- MODULE OLCChainMembership --------------------- +\* Stage 4: Chain membership precondition under concurrent insert. +\* +\* One remover evaluates whether an I4 node is a chain member (count==1). +\* One inserter can add a child to that same I4 concurrently. +\* The remover uses OLC revalidation: read count → validate version → act. +\* +\* Verifies: remover never proceeds with cut when count is actually 2. + +EXTENDS Integers + +CONSTANTS + MaxVersion + +VARIABLES + \* Shared I4 node state + count, \* 1 or 2 children + version, \* Even=unlocked, Odd=locked + + \* Remover state (evaluating chain membership) + rpc, \* idle|read_count|validate|upgrade|locked|done|restart + r_count, \* Cached count value + r_ver, \* Cached version + + \* Inserter state + ipc \* idle|lock|insert|unlock|done + +vars == <> + +----------------------------------------------------------------------------- +Init == + /\ count = 1 \* starts as chain member (single child) + /\ version = 0 + /\ rpc = "idle" + /\ r_count = 0 + /\ r_ver = 0 + /\ ipc = "idle" + +----------------------------------------------------------------------------- +\* INSERTER: adds a child (count 1→2) + +InsertLock == + /\ ipc = "idle" + /\ version % 2 = 0 + /\ version <= MaxVersion + /\ count < 2 \* only insert if room + /\ version' = version + 1 + /\ ipc' = "lock" + /\ UNCHANGED <> + +InsertWrite == + /\ ipc = "lock" + /\ count' = count + 1 + /\ ipc' = "unlock" + /\ UNCHANGED <> + +InsertUnlock == + /\ ipc = "unlock" + /\ version' = version + 1 + /\ ipc' = "done" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +\* REMOVER: evaluates chain membership via OLC + +RemoverStart == + /\ rpc = "idle" + /\ rpc' = "read_count" + /\ r_ver' = version \* capture version + /\ UNCHANGED <> + +RemoverReadCount == + /\ rpc = "read_count" + /\ r_count' = count \* read shared count + /\ rpc' = "validate" + /\ UNCHANGED <> + +RemoverValidateOK == + /\ rpc = "validate" + /\ version = r_ver \* unchanged + /\ version % 2 = 0 \* not locked + /\ IF r_count = 1 + THEN rpc' = "upgrade" \* chain member, try to lock + ELSE rpc' = "not_chain" \* not a chain member + /\ UNCHANGED <> + +RemoverValidateFail == + /\ rpc = "validate" + /\ (version # r_ver \/ version % 2 = 1) + /\ rpc' = "restart" + /\ UNCHANGED <> + +RemoverUpgrade == + /\ rpc = "upgrade" + /\ IF version = r_ver /\ version % 2 = 0 + THEN /\ version' = version + 1 + /\ rpc' = "locked" + ELSE /\ rpc' = "restart" + /\ UNCHANGED version + /\ UNCHANGED <> + +RemoverDone == + /\ rpc = "locked" + /\ rpc' = "done" + /\ version' = version + 1 \* unlock + /\ UNCHANGED <> + +RemoverNotChain == + /\ rpc = "not_chain" + /\ rpc' = "done" + /\ UNCHANGED <> + +RemoverRestart == + /\ rpc = "restart" + /\ rpc' = "idle" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +Step == + \/ InsertLock \/ InsertWrite \/ InsertUnlock + \/ RemoverStart \/ RemoverReadCount + \/ RemoverValidateOK \/ RemoverValidateFail + \/ RemoverUpgrade \/ RemoverDone \/ RemoverNotChain \/ RemoverRestart + +Spec == Init /\ [][Step]_vars + +----------------------------------------------------------------------------- +\* INVARIANTS + +\* CRITICAL: Remover never holds lock (proceeds with cut) when count=2. +\* If remover is in "locked" state, the actual count MUST be 1. +ChainSafety == + rpc = "locked" => count = 1 + +\* If remover decided "not_chain", it read count#1 under valid version. +\* (This is a weaker check — mainly for debugging.) +NotChainCorrect == + rpc = "not_chain" => r_count # 1 + +============================================================================= diff --git a/spec/tla/OLCChainMultiLevel.cfg b/spec/tla/OLCChainMultiLevel.cfg new file mode 100644 index 00000000..e454fd33 --- /dev/null +++ b/spec/tla/OLCChainMultiLevel.cfg @@ -0,0 +1,15 @@ +SPECIFICATION Spec + +CONSTANTS + MaxVersion = 6 + +INVARIANTS + CutSafety + ChainLockConsistency + WellFormedness + PartialCutValid + +CONSTRAINT + StateConstraint + +CHECK_DEADLOCK FALSE diff --git a/spec/tla/OLCChainMultiLevel.tla b/spec/tla/OLCChainMultiLevel.tla new file mode 100644 index 00000000..230419fa --- /dev/null +++ b/spec/tla/OLCChainMultiLevel.tla @@ -0,0 +1,277 @@ +--------------------------- MODULE OLCChainMultiLevel --------------------- +\* Stage 9: Multi-level chain cut with concurrent insert. +\* +\* Topology: parent → chain0 → chain1 → (leaf, implicit) +\* Parent has 2+ children (one is chain0). +\* chain0 has 1 child (chain1). chain1 has 1 child (leaf). +\* +\* Remover: locks chain1, then chain0 (bottom-up), then evaluates parent. +\* Inserter: can add a child to chain0 OR chain1, breaking membership. +\* +\* Key scenarios exercised: +\* - cut_level moves DOWN: insert breaks chain0 after chain1 locked +\* - cut_level stays: both chain nodes lock successfully +\* - Case A on parent: normal cut +\* - Case C on parent: child pointer gone (concurrent remove of chain0) +\* +\* Verifies: cut only proceeds with correct locks and valid state. + +EXTENDS Integers + +CONSTANTS MaxVersion + +VARIABLES + \* Parent node + p_count, \* 2 or 3 (chain0 + sibling, optionally + inserted) + p_has_c0, \* parent points to chain0 + p_ver, + + \* Chain node 0 (top of chain, child of parent) + c0_count, \* 1 or 2 + c0_ver, + + \* Chain node 1 (bottom of chain, child of chain0) + c1_count, \* 1 (always — leaf is implicit) + c1_ver, + + \* Remover state + rpc, \* idle|lock_c1|lock_c0|read_parent|validate_parent| + \* upgrade_parent|cut|done|restart + r_cut_level,\* 0=cut from chain0, 1=cut from chain1 only + r_c1_locked,\* holds write lock on chain1 + r_c0_locked,\* holds write lock on chain0 + r_pver, \* cached parent version + r_p_has_c0, \* cached: parent has chain0? + + \* Inserter state + ipc, \* idle|lock|write|unlock|done + i_target, \* "c0" or "c1" + i_ver \* cached version of target for lock + +vars == <> + +----------------------------------------------------------------------------- +Init == + /\ p_count = 2 /\ p_has_c0 = TRUE /\ p_ver = 0 + /\ c0_count = 1 /\ c0_ver = 0 + /\ c1_count = 1 /\ c1_ver = 0 + /\ rpc = "idle" /\ r_cut_level = 0 + /\ r_c1_locked = FALSE /\ r_c0_locked = FALSE + /\ r_pver = 0 /\ r_p_has_c0 = FALSE + /\ ipc = "idle" /\ i_target = "c0" /\ i_ver = 0 + +----------------------------------------------------------------------------- +\* REMOVER: bottom-up chain locking, then CPP evaluation + +\* Step 2a: Lock chain1 (bottom of chain) +RemoverLockC1 == + /\ rpc = "idle" + /\ c1_ver % 2 = 0 /\ c1_count = 1 \* chain membership precondition + /\ c1_ver' = c1_ver + 1 \* lock + /\ r_c1_locked' = TRUE + /\ r_cut_level' = 1 \* initially cut from chain1 + /\ rpc' = "lock_c0" + /\ UNCHANGED <> + +\* Step 2b: Try to lock chain0 (revalidation with precondition) +RemoverLockC0_OK == + /\ rpc = "lock_c0" + /\ c0_ver % 2 = 0 /\ c0_count = 1 \* precondition holds + /\ c0_ver' = c0_ver + 1 \* lock + /\ r_c0_locked' = TRUE + /\ r_cut_level' = 0 \* cut from chain0 (full chain) + /\ rpc' = "read_parent" + /\ UNCHANGED <> + +\* Step 2b: chain0 precondition FAILS (count != 1 or version odd) +\* cut_level stays at 1 — chain0 becomes the cut_point_parent +RemoverLockC0_Fail == + /\ rpc = "lock_c0" + /\ (c0_ver % 2 = 1 \/ c0_count # 1) \* precondition fails + /\ r_cut_level' = 1 \* cut only chain1 + /\ rpc' = "read_c0_as_cpp" \* chain0 is now CPP + /\ UNCHANGED <> + +\* Step 3 (when chain0 is CPP): read chain0 state +RemoverReadC0AsCPP == + /\ rpc = "read_c0_as_cpp" + /\ r_pver' = c0_ver \* reuse r_pver for c0's version + /\ rpc' = "validate_c0_cpp" + /\ UNCHANGED <> + +\* Validate chain0 as CPP and upgrade +RemoverValidateC0CPP == + /\ rpc = "validate_c0_cpp" + /\ IF c0_ver = r_pver /\ c0_ver % 2 = 0 + THEN /\ c0_ver' = c0_ver + 1 \* lock chain0 as CPP + /\ r_c0_locked' = TRUE + /\ rpc' = "cut" + ELSE /\ rpc' = "restart" \* version changed + /\ UNCHANGED <> + /\ UNCHANGED <> + +\* Step 3 (when parent is CPP): read parent state +RemoverReadParent == + /\ rpc = "read_parent" + /\ r_pver' = p_ver + /\ r_p_has_c0' = p_has_c0 + /\ rpc' = "validate_parent" + /\ UNCHANGED <> + +\* Validate parent and upgrade +RemoverValidateParent == + /\ rpc = "validate_parent" + /\ IF p_ver = r_pver /\ p_ver % 2 = 0 + THEN IF ~r_p_has_c0 + THEN rpc' = "restart" \* Case C + ELSE rpc' = "upgrade_parent" \* Case A + ELSE rpc' = "read_parent" \* stale + /\ UNCHANGED <> + +RemoverUpgradeParent == + /\ rpc = "upgrade_parent" + /\ IF p_ver = r_pver /\ p_ver % 2 = 0 + THEN /\ p_ver' = p_ver + 1 + /\ rpc' = "cut" + ELSE /\ rpc' = "read_parent" + /\ UNCHANGED p_ver + /\ UNCHANGED <> + +\* Step 4: Cut (point of no return) +RemoverCut == + /\ rpc = "cut" + /\ IF r_cut_level = 0 + THEN \* Full chain cut: remove chain0 from parent + /\ p_has_c0' = FALSE + /\ p_count' = p_count - 1 + /\ p_ver' = p_ver + 1 \* unlock parent + /\ c0_ver' = c0_ver + 1 \* obsolete chain0 + /\ c1_ver' = c1_ver + 1 \* obsolete chain1 + /\ UNCHANGED <> + ELSE \* Partial cut: remove chain1 from chain0 + /\ c0_count' = c0_count - 1 + /\ c0_ver' = c0_ver + 1 \* unlock chain0 (CPP) + /\ c1_ver' = c1_ver + 1 \* obsolete chain1 + /\ UNCHANGED <> + /\ r_c0_locked' = FALSE + /\ r_c1_locked' = FALSE + /\ rpc' = "done" + /\ UNCHANGED <> + +RemoverRestart == + /\ rpc = "restart" + /\ IF r_c1_locked THEN c1_ver' = c1_ver + 1 ELSE UNCHANGED c1_ver + /\ IF r_c0_locked THEN c0_ver' = c0_ver + 1 ELSE UNCHANGED c0_ver + /\ r_c1_locked' = FALSE /\ r_c0_locked' = FALSE + /\ rpc' = "idle" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +\* INSERTER: adds a child to chain0 or chain1 (breaking chain membership) + +InsertChoose == + /\ ipc = "idle" + /\ \E t \in {"c0", "c1"} : + /\ (t = "c0" => c0_count < 2) + /\ (t = "c1" => c1_count < 2) + /\ i_target' = t + /\ ipc' = "lock" + /\ UNCHANGED <> + +InsertLock == + /\ ipc = "lock" + /\ IF i_target = "c0" + THEN /\ c0_ver % 2 = 0 /\ c0_ver <= MaxVersion + /\ c0_ver' = c0_ver + 1 + /\ UNCHANGED c1_ver + ELSE /\ c1_ver % 2 = 0 /\ c1_ver <= MaxVersion + /\ c1_ver' = c1_ver + 1 + /\ UNCHANGED c0_ver + /\ ipc' = "write" + /\ UNCHANGED <> + +InsertWrite == + /\ ipc = "write" + /\ IF i_target = "c0" + THEN /\ c0_count' = c0_count + 1 + /\ UNCHANGED c1_count + ELSE /\ c1_count' = c1_count + 1 + /\ UNCHANGED c0_count + /\ ipc' = "unlock" + /\ UNCHANGED <> + +InsertUnlock == + /\ ipc = "unlock" + /\ IF i_target = "c0" + THEN /\ c0_ver' = c0_ver + 1 + /\ UNCHANGED c1_ver + ELSE /\ c1_ver' = c1_ver + 1 + /\ UNCHANGED c0_ver + /\ ipc' = "done" + /\ UNCHANGED <> + +InsertDone == + /\ ipc = "done" + /\ ipc' = "idle" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +Step == + \/ RemoverLockC1 \/ RemoverLockC0_OK \/ RemoverLockC0_Fail + \/ RemoverReadC0AsCPP \/ RemoverValidateC0CPP + \/ RemoverReadParent \/ RemoverValidateParent \/ RemoverUpgradeParent + \/ RemoverCut \/ RemoverRestart + \/ InsertChoose \/ InsertLock \/ InsertWrite \/ InsertUnlock \/ InsertDone + +Spec == Init /\ [][Step]_vars +StateConstraint == p_ver <= MaxVersion /\ c0_ver <= MaxVersion /\ c1_ver <= MaxVersion + +----------------------------------------------------------------------------- +\* INVARIANTS + +\* Cut only when holding correct locks and state is valid +CutSafety == + rpc = "cut" => + /\ r_c1_locked \* always hold chain1 lock + /\ (r_cut_level = 0 => r_c0_locked) \* full cut needs chain0 lock + /\ (r_cut_level = 0 => p_has_c0) \* parent still has chain0 + +\* Chain membership: if remover holds chain lock, count must be 1 +ChainLockConsistency == + /\ (r_c1_locked /\ c1_ver % 2 = 1 => c1_count = 1) + /\ (r_c0_locked /\ c0_ver % 2 = 1 /\ r_cut_level = 0 => c0_count = 1) + +\* Well-formedness: counts never go below valid range +WellFormedness == + /\ p_count >= 1 + /\ c0_count >= 0 + /\ c1_count >= 0 + +\* Partial cut correctness: if cut_level=1, chain0 is CPP (locked by remover) +PartialCutValid == + (rpc = "cut" /\ r_cut_level = 1) => r_c0_locked + +============================================================================= diff --git a/spec/tla/OLCDoubleCut.cfg b/spec/tla/OLCDoubleCut.cfg new file mode 100644 index 00000000..69d5ad13 --- /dev/null +++ b/spec/tla/OLCDoubleCut.cfg @@ -0,0 +1,9 @@ +SPECIFICATION Spec + +INVARIANTS + TypeOK + MutualExclusion + AtMostOneCut + NoDoubleObsolete + +CHECK_DEADLOCK FALSE diff --git a/spec/tla/OLCDoubleCut.tla b/spec/tla/OLCDoubleCut.tla new file mode 100644 index 00000000..c9a5d404 --- /dev/null +++ b/spec/tla/OLCDoubleCut.tla @@ -0,0 +1,105 @@ +-------------------------- MODULE OLCDoubleCut ------------------------- +(* Stage 8: Two removes on the same chain — at-most-one-cut. + Models two removers competing to cut a single chain node. Only one + should succeed in marking it obsolete. + + Fix M3: Added RDone actions so removers cycle back to idle, making + AtMostOneCut non-trivial. Replaced NoDoubleFree with NoDoubleObsolete + which verifies: once obsoleted, no one else can lock it. *) + +EXTENDS Naturals + +VARIABLES r1pc, r2pc, c_locked, c_obsolete, cut_count + +vars == <> + +TypeOK == + /\ r1pc \in {"idle", "locked", "cut", "done"} + /\ r2pc \in {"idle", "locked", "cut", "done"} + /\ c_locked \in BOOLEAN + /\ c_obsolete \in BOOLEAN + /\ cut_count \in Nat + +Init == + /\ r1pc = "idle" + /\ r2pc = "idle" + /\ c_locked = FALSE + /\ c_obsolete = FALSE + /\ cut_count = 0 + +(* --- Remover 1 actions --- *) + +R1Lock == + /\ r1pc = "idle" + /\ ~c_locked + /\ ~c_obsolete + /\ c_locked' = TRUE + /\ r1pc' = "locked" + /\ UNCHANGED <> + +R1Cut == + /\ r1pc = "locked" + /\ c_obsolete' = TRUE + /\ cut_count' = cut_count + 1 + /\ r1pc' = "cut" + /\ UNCHANGED <> + +R1Unlock == + /\ r1pc = "cut" + /\ c_locked' = FALSE + /\ r1pc' = "done" + /\ UNCHANGED <> + +R1Done == + /\ r1pc = "done" + /\ r1pc' = "idle" + /\ UNCHANGED <> + +(* --- Remover 2 actions --- *) + +R2Lock == + /\ r2pc = "idle" + /\ ~c_locked + /\ ~c_obsolete + /\ c_locked' = TRUE + /\ r2pc' = "locked" + /\ UNCHANGED <> + +R2Cut == + /\ r2pc = "locked" + /\ c_obsolete' = TRUE + /\ cut_count' = cut_count + 1 + /\ r2pc' = "cut" + /\ UNCHANGED <> + +R2Unlock == + /\ r2pc = "cut" + /\ c_locked' = FALSE + /\ r2pc' = "done" + /\ UNCHANGED <> + +R2Done == + /\ r2pc = "done" + /\ r2pc' = "idle" + /\ UNCHANGED <> + +(* --- Step and Spec --- *) + +Step == + \/ R1Lock \/ R1Cut \/ R1Unlock \/ R1Done + \/ R2Lock \/ R2Cut \/ R2Unlock \/ R2Done + +Spec == Init /\ [][Step]_vars /\ WF_vars(Step) + +(* --- Invariants --- *) + +MutualExclusion == + ~(r1pc \in {"locked", "cut"} /\ r2pc \in {"locked", "cut"}) + +AtMostOneCut == cut_count <= 1 + +NoDoubleObsolete == + /\ (r1pc = "locked" => ~c_obsolete) + /\ (r2pc = "locked" => ~c_obsolete) + +========================================================================= diff --git a/spec/tla/OLCInsert.cfg b/spec/tla/OLCInsert.cfg new file mode 100644 index 00000000..7ab88226 --- /dev/null +++ b/spec/tla/OLCInsert.cfg @@ -0,0 +1,10 @@ +SPECIFICATION Spec + +CONSTANT NumSlots = 2 + +INVARIANTS + TypeOK + MutualExclusion + CountConsistency + +CHECK_DEADLOCK FALSE diff --git a/spec/tla/OLCInsert.tla b/spec/tla/OLCInsert.tla new file mode 100644 index 00000000..4af1fb90 --- /dev/null +++ b/spec/tla/OLCInsert.tla @@ -0,0 +1,113 @@ +--------------------------- MODULE OLCInsert --------------------------- +(* Stage 3: Two writers racing for the same node — mutual exclusion via OLC. + Models the version-based optimistic lock protocol where writers must + acquire exclusive access (odd version) before modifying node state. + + Fix C2: WWrite split into WWriteSlot + WWriteCount to model non-atomic + count maintenance. CountConsistency only checked when version is even + (unlocked state). *) + +EXTENDS Naturals, FiniteSets + +CONSTANTS NumSlots + +Slots == 1..NumSlots + +VARIABLES version, slots, count, + w1pc, w1target, + w2pc, w2target + +vars == <> + +TypeOK == + /\ version \in Nat + /\ slots \in [Slots -> {0, 1}] + /\ count \in 0..NumSlots + /\ w1pc \in {"idle", "locked", "write_slot", "write_count", "unlock"} + /\ w2pc \in {"idle", "locked", "write_slot", "write_count", "unlock"} + /\ w1target \in Slots + /\ w2target \in Slots + +Init == + /\ version = 0 + /\ slots = [i \in Slots |-> 0] + /\ count = 0 + /\ w1pc = "idle" + /\ w2pc = "idle" + /\ w1target = 1 + /\ w2target = 1 + +(* --- Writer 1 actions --- *) + +W1Lock == + /\ w1pc = "idle" + /\ version % 2 = 0 \* not already write-locked + /\ \E t \in Slots : slots[t] = 0 /\ w1target' = t + /\ version' = version + 1 \* odd = locked + /\ w1pc' = "locked" + /\ UNCHANGED <> + +W1WriteSlot == + /\ w1pc = "locked" + /\ slots' = [slots EXCEPT ![w1target] = 1] + /\ w1pc' = "write_slot" + /\ UNCHANGED <> + +W1WriteCount == + /\ w1pc = "write_slot" + /\ count' = count + 1 + /\ w1pc' = "write_count" + /\ UNCHANGED <> + +W1Unlock == + /\ w1pc = "write_count" + /\ version' = version + 1 \* even = unlocked + /\ w1pc' = "idle" + /\ UNCHANGED <> + +(* --- Writer 2 actions --- *) + +W2Lock == + /\ w2pc = "idle" + /\ version % 2 = 0 + /\ \E t \in Slots : slots[t] = 0 /\ w2target' = t + /\ version' = version + 1 + /\ w2pc' = "locked" + /\ UNCHANGED <> + +W2WriteSlot == + /\ w2pc = "locked" + /\ slots' = [slots EXCEPT ![w2target] = 1] + /\ w2pc' = "write_slot" + /\ UNCHANGED <> + +W2WriteCount == + /\ w2pc = "write_slot" + /\ count' = count + 1 + /\ w2pc' = "write_count" + /\ UNCHANGED <> + +W2Unlock == + /\ w2pc = "write_count" + /\ version' = version + 1 + /\ w2pc' = "idle" + /\ UNCHANGED <> + +(* --- Step and Spec --- *) + +Step == + \/ W1Lock \/ W1WriteSlot \/ W1WriteCount \/ W1Unlock + \/ W2Lock \/ W2WriteSlot \/ W2WriteCount \/ W2Unlock + +Spec == Init /\ [][Step]_vars /\ WF_vars(Step) + +(* --- Invariants --- *) + +MutualExclusion == + ~(w1pc \in {"locked", "write_slot", "write_count"} /\ + w2pc \in {"locked", "write_slot", "write_count"}) + +CountConsistency == + version % 2 = 0 => count = Cardinality({i \in Slots : slots[i] = 1}) + +========================================================================= diff --git a/spec/tla/OLCInsertChainVIS.cfg b/spec/tla/OLCInsertChainVIS.cfg new file mode 100644 index 00000000..0a747252 --- /dev/null +++ b/spec/tla/OLCInsertChainVIS.cfg @@ -0,0 +1,13 @@ +SPECIFICATION Spec + +CONSTANTS + MaxVersion = 4 + +INVARIANTS + NoTransientVisible + SnapshotConsistency + +CONSTRAINT + StateConstraint + +CHECK_DEADLOCK FALSE diff --git a/spec/tla/OLCInsertChainVIS.tla b/spec/tla/OLCInsertChainVIS.tla new file mode 100644 index 00000000..a1209e98 --- /dev/null +++ b/spec/tla/OLCInsertChainVIS.tla @@ -0,0 +1,147 @@ +--------------------------- MODULE OLCInsertChainVIS ---------------------- +\* Stage 7: Insert chain protocol with transient VIS bitmask state. +\* +\* When inserting a chain into a non-full node, the writer does: +\* 1. add_to_nonfull(pack_value) → sets value_bit (slot looks like VIS) +\* 2. overwrite slot with chain pointer +\* 3. clear_value_bit (slot is now a pointer) +\* +\* All 3 steps happen under ONE write lock. A concurrent reader that +\* validates successfully must never see the transient state. +\* +\* Verifies: reader never sees (bitmask=TRUE, slot=chain_ptr). + +EXTENDS Integers + +CONSTANTS + MaxVersion + +VARIABLES + \* Shared state + slot, \* 0=empty, 1=packed_value, -1=chain_ptr + bitmask, \* TRUE if slot holds a value + version, \* Even=unlocked, Odd=locked + + \* Writer state (chain insert protocol) + wpc, \* idle|lock|set_bit|write_chain|clear_bit|unlock|done + + \* Reader state + rpc, \* idle|read_slot|read_bitmask|validate|done + rver, \* Cached version + rslot, \* Local slot copy + rbitmask \* Local bitmask copy + +vars == <> + +----------------------------------------------------------------------------- +Init == + /\ slot = 0 + /\ bitmask = FALSE + /\ version = 0 + /\ wpc = "idle" + /\ rpc = "idle" + /\ rver = 0 + /\ rslot = 0 + /\ rbitmask = FALSE + +----------------------------------------------------------------------------- +\* WRITER: chain insert protocol (4 steps under one lock) + +WriterLock == + /\ wpc = "idle" + /\ version % 2 = 0 + /\ version <= MaxVersion + /\ slot = 0 \* slot must be empty + /\ version' = version + 1 + /\ wpc' = "set_bit" + /\ UNCHANGED <> + +WriterSetBit == + /\ wpc = "set_bit" + /\ slot' = 1 \* store packed value temporarily + /\ bitmask' = TRUE \* mark as VIS + /\ wpc' = "write_chain" + /\ UNCHANGED <> + +WriterWriteChain == + /\ wpc = "write_chain" + /\ slot' = -1 \* overwrite with chain pointer + /\ wpc' = "clear_bit" + /\ UNCHANGED <> + +WriterClearBit == + /\ wpc = "clear_bit" + /\ bitmask' = FALSE \* slot is now a pointer, not a value + /\ wpc' = "unlock" + /\ UNCHANGED <> + +WriterUnlock == + /\ wpc = "unlock" + /\ version' = version + 1 + /\ wpc' = "done" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +\* READER: reads slot + bitmask, validates, interprets + +ReaderStart == + /\ rpc = "idle" + /\ rver' = version + /\ rpc' = "read_slot" + /\ UNCHANGED <> + +ReaderReadSlot == + /\ rpc = "read_slot" + /\ rslot' = slot + /\ rpc' = "read_bitmask" + /\ UNCHANGED <> + +ReaderReadBitmask == + /\ rpc = "read_bitmask" + /\ rbitmask' = bitmask + /\ rpc' = "validate" + /\ UNCHANGED <> + +ReaderValidateOK == + /\ rpc = "validate" + /\ version = rver + /\ version % 2 = 0 + /\ rpc' = "done" + /\ UNCHANGED <> + +ReaderValidateFail == + /\ rpc = "validate" + /\ (version # rver \/ version % 2 = 1) + /\ rpc' = "idle" + /\ UNCHANGED <> + +ReaderReset == + /\ rpc = "done" + /\ rpc' = "idle" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +Step == + \/ WriterLock \/ WriterSetBit \/ WriterWriteChain + \/ WriterClearBit \/ WriterUnlock + \/ ReaderStart \/ ReaderReadSlot \/ ReaderReadBitmask + \/ ReaderValidateOK \/ ReaderValidateFail \/ ReaderReset + +Spec == Init /\ [][Step]_vars + +StateConstraint == version <= MaxVersion + +----------------------------------------------------------------------------- +\* INVARIANTS + +\* CRITICAL: Reader never sees transient state (bitmask=TRUE, slot=chain_ptr) +NoTransientVisible == + rpc = "done" => ~(rbitmask = TRUE /\ rslot = -1) + +\* Reader's validated snapshot is consistent +SnapshotConsistency == + rpc = "done" => + /\ (rbitmask = TRUE => rslot >= 0) \* value slots hold values + /\ (rslot = -1 => rbitmask = FALSE) \* chain ptr has no bitmask + +============================================================================= diff --git a/spec/tla/OLCIterRemove.cfg b/spec/tla/OLCIterRemove.cfg new file mode 100644 index 00000000..b306e3cf --- /dev/null +++ b/spec/tla/OLCIterRemove.cfg @@ -0,0 +1,10 @@ +SPECIFICATION Spec + +CONSTANT MaxVersion = 6 +CONSTANT OBSOLETE = 99 + +INVARIANT SnapshotValid + +CONSTRAINT StateConstraint + +CHECK_DEADLOCK FALSE diff --git a/spec/tla/OLCIterRemove.tla b/spec/tla/OLCIterRemove.tla new file mode 100644 index 00000000..11353e65 --- /dev/null +++ b/spec/tla/OLCIterRemove.tla @@ -0,0 +1,297 @@ +--------------------------- MODULE OLCIterRemove --------------------------- +(* OLC (Optimistic Lock Coupling) Iterator vs. Remover specification. + Models a 3-node tree: grandparent → parent → child. + A remover can obsolete either the parent or the child. + An iterator descends the tree using optimistic validation at each level. + + The key safety property (SnapshotValid): if the iterator reaches the "act" + state, it validated against an even (unlocked), non-obsolete version. *) + +EXTENDS Naturals + +CONSTANT MaxVersion +CONSTANT OBSOLETE + +VARIABLES + \* Grandparent node + gp_ver, \* version counter (even = unlocked, odd = write-locked) + gp_child, \* pointer to parent (TRUE = valid, FALSE = removed) + \* Parent node + p_ver, \* version counter + p_child, \* pointer to child (TRUE = valid, FALSE = removed) + \* Child node + c_ver, \* version counter + c_obsolete, \* whether child is obsolete + \* Iterator state + ipc, \* iterator program counter + i_gp_ver, \* snapshot of gp_ver taken during read_gp + i_p_ver, \* snapshot of p_ver taken during read_parent + i_cver, \* snapshot of c_ver taken during read_child + \* Remover state + rpc, \* remover program counter + r_target, \* which node the remover targets: "parent" or "child" + \* Writer state (normal writer — bumps version without obsoleting) + wpc, \* writer program counter: idle | lock | unlock + w_target \* which node writer targets: "parent" or "child" + +vars == <> + +----------------------------------------------------------------------------- +(* Initial state *) + +Init == + /\ gp_ver = 0 + /\ gp_child = TRUE + /\ p_ver = 0 + /\ p_child = TRUE + /\ c_ver = 0 + /\ c_obsolete = FALSE + /\ ipc = "idle" + /\ i_gp_ver = 0 + /\ i_p_ver = 0 + /\ i_cver = 0 + /\ rpc = "idle" + /\ r_target = "child" + /\ wpc = "idle" + /\ w_target = "child" + +----------------------------------------------------------------------------- +(* Iterator actions. + Spinning on a write-locked node is modeled by the action being disabled + (precondition not met). Encountering OBSOLETE triggers a restart. *) + +\* Step 1: Read grandparent — snapshot its version +\* Spins while locked; restarts if obsolete (handled: gp can't be obsoleted) +IterReadGP == + /\ ipc = "idle" + /\ gp_ver # OBSOLETE + /\ gp_ver % 2 = 0 + /\ i_gp_ver' = gp_ver + /\ ipc' = "read_gp" + /\ UNCHANGED <> + +\* Step 2: Descend to parent — validate grandparent version unchanged +IterDescendToParent == + /\ ipc = "read_gp" + /\ IF gp_ver = i_gp_ver /\ gp_ver # OBSOLETE + THEN ipc' = "read_parent" + ELSE ipc' = "idle" + /\ UNCHANGED <> + +\* Step 3: Read parent — snapshot version +\* Enabled only when parent is unlocked and not obsolete (spin/restart) +IterReadParent == + /\ ipc = "read_parent" + /\ p_ver # OBSOLETE + /\ p_ver % 2 = 0 + /\ i_p_ver' = p_ver + /\ ipc' = "descend_to_child" + /\ UNCHANGED <> + +\* Step 3b: Restart if parent is obsolete +IterReadParentRestart == + /\ ipc = "read_parent" + /\ p_ver = OBSOLETE + /\ ipc' = "idle" + /\ UNCHANGED <> + +\* Step 4: Descend to child — validate parent version unchanged +IterDescendToChild == + /\ ipc = "descend_to_child" + /\ IF p_ver = i_p_ver /\ p_ver # OBSOLETE + THEN ipc' = "read_child" + ELSE ipc' = "idle" + /\ UNCHANGED <> + +\* Step 5: Read child — snapshot version +\* Enabled only when child is unlocked and not obsolete (spin/restart) +IterReadChild == + /\ ipc = "read_child" + /\ c_ver # OBSOLETE + /\ c_ver % 2 = 0 + /\ i_cver' = c_ver + /\ ipc' = "validate_child" + /\ UNCHANGED <> + +\* Step 5b: Restart if child is obsolete +IterReadChildRestart == + /\ ipc = "read_child" + /\ c_ver = OBSOLETE + /\ ipc' = "idle" + /\ UNCHANGED <> + +\* Step 6: Validate child — check version unchanged and not obsolete +IterValidateChild == + /\ ipc = "validate_child" + /\ IF c_ver = i_cver /\ c_ver # OBSOLETE + THEN ipc' = "act" + ELSE ipc' = "idle" + /\ UNCHANGED <> + +\* Step 7: Act on the data and finish +IterAct == + /\ ipc = "act" + /\ ipc' = "done" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Remover actions — targets either parent or child *) + +\* Choose target (non-deterministic) +RemoverChooseTarget == + /\ rpc = "idle" + /\ \E t \in {"parent", "child"} : + /\ r_target' = t + /\ rpc' = "lock" + /\ UNCHANGED <> + +\* Lock the grandparent (write-lock for structural change) +RemoverLockGP == + /\ rpc = "lock" + /\ gp_ver % 2 = 0 + /\ gp_ver # OBSOLETE + /\ gp_ver' = gp_ver + 1 + /\ rpc' = "lock_target" + /\ UNCHANGED <> + +\* Lock the target node +RemoverLockTarget == + /\ rpc = "lock_target" + /\ IF r_target = "parent" + THEN /\ p_ver % 2 = 0 + /\ p_ver # OBSOLETE + /\ p_ver' = p_ver + 1 + /\ UNCHANGED <> + ELSE /\ c_ver % 2 = 0 + /\ c_ver # OBSOLETE + /\ c_ver' = c_ver + 1 + /\ UNCHANGED <> + /\ rpc' = "obsolete" + /\ UNCHANGED <> + +\* Mark target obsolete and unlink +RemoverObsolete == + /\ rpc = "obsolete" + /\ IF r_target = "parent" + THEN /\ p_ver' = OBSOLETE + /\ gp_child' = FALSE + /\ UNCHANGED <> + ELSE /\ c_ver' = OBSOLETE + /\ c_obsolete' = TRUE + /\ p_child' = FALSE + /\ UNCHANGED <> + /\ rpc' = "unlock_gp" + /\ UNCHANGED <> + +\* Unlock grandparent (bump version to next even) +RemoverUnlockGP == + /\ rpc = "unlock_gp" + /\ gp_ver' = gp_ver + 1 + /\ rpc' = "done" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Normal writer: locks a node, bumps version, unlocks. No obsolescence. + Tests that iterator detects version changes from concurrent inserts. *) + +WriterChoose == + /\ wpc = "idle" + /\ \E t \in {"parent", "child"} : + /\ w_target' = t + /\ wpc' = "lock" + /\ UNCHANGED <> + +WriterLock == + /\ wpc = "lock" + /\ IF w_target = "parent" + THEN /\ p_ver % 2 = 0 /\ p_ver < MaxVersion + /\ p_ver' = p_ver + 1 + /\ UNCHANGED c_ver + ELSE /\ c_ver % 2 = 0 /\ c_ver < MaxVersion /\ ~c_obsolete + /\ c_ver' = c_ver + 1 + /\ UNCHANGED p_ver + /\ wpc' = "unlock" + /\ UNCHANGED <> + +WriterUnlock == + /\ wpc = "unlock" + /\ IF w_target = "parent" + THEN /\ p_ver' = p_ver + 1 + /\ UNCHANGED c_ver + ELSE /\ c_ver' = c_ver + 1 + /\ UNCHANGED p_ver + /\ wpc' = "idle" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +(* Specification *) + +Next == + \/ IterReadGP + \/ IterDescendToParent + \/ IterReadParent + \/ IterReadParentRestart + \/ IterDescendToChild + \/ IterReadChild + \/ IterReadChildRestart + \/ IterValidateChild + \/ IterAct + \/ RemoverChooseTarget + \/ RemoverLockGP + \/ RemoverLockTarget + \/ RemoverObsolete + \/ RemoverUnlockGP + \/ WriterChoose + \/ WriterLock + \/ WriterUnlock + +Spec == Init /\ [][Next]_vars + +----------------------------------------------------------------------------- +(* Invariants *) + +TypeOK == + /\ gp_ver \in (0..MaxVersion) \cup {OBSOLETE} + /\ gp_child \in BOOLEAN + /\ p_ver \in (0..MaxVersion) \cup {OBSOLETE} + /\ p_child \in BOOLEAN + /\ c_ver \in (0..MaxVersion) \cup {OBSOLETE} + /\ c_obsolete \in BOOLEAN + /\ ipc \in {"idle", "read_gp", "read_parent", "descend_to_child", + "read_child", "validate_child", "act", "done"} + /\ i_gp_ver \in 0..MaxVersion + /\ i_p_ver \in 0..MaxVersion + /\ i_cver \in 0..MaxVersion + /\ rpc \in {"idle", "lock", "lock_target", "obsolete", "unlock_gp", "done"} + /\ r_target \in {"parent", "child"} + /\ wpc \in {"idle", "lock", "unlock"} + /\ w_target \in {"parent", "child"} + +\* Safety: if iterator acts, it validated against an even (unlocked), +\* non-obsolete version. +SnapshotValid == + ipc = "act" => (i_cver % 2 = 0 /\ i_cver # OBSOLETE) + +\* State constraint to bound model checking +StateConstraint == + /\ (gp_ver # OBSOLETE => gp_ver <= MaxVersion) + /\ (p_ver # OBSOLETE => p_ver <= MaxVersion) + /\ (c_ver # OBSOLETE => c_ver <= MaxVersion) + +============================================================================= diff --git a/spec/tla/OLCIterator.tla b/spec/tla/OLCIterator.tla new file mode 100644 index 00000000..be2aa49a --- /dev/null +++ b/spec/tla/OLCIterator.tla @@ -0,0 +1,329 @@ +--------------------------- MODULE OLCIterator ---------------------------- +(* TLA+ model of the OLC ART stack-based iterator. + Models try_next() and try_left_most_traversal with concurrent writer. + + Tree geometry: depth 3, parametric width. + Root (inode) + ├── A (inode) + │ ├── L1 (leaf) + │ └── L2 (leaf) + └── B (inode) + ├── L3 (leaf) + └── L4 (leaf) + + Forward scan order: L1, L2, L3, L4. + + The iterator maintains a stack of (node, child_index, version) entries + and advances by: pop leaf, find next child in parent, descend left-most. + If no next child, pop parent (backtrack/ascend) and repeat. + + ConcurrencyEnabled: FALSE = sequential (db), TRUE = OLC (olc_db). + When FALSE, check() always succeeds and no writer runs. + + Properties verified: + - OrderPreservation: leaves are visited in correct order + - NoSkip: no leaf present throughout the scan is missed + - NoRepeat: no leaf is visited twice + - NoStaleAct: iterator never acts on stale version (OLC mode) + - Termination: iterator eventually reaches end or delivers all leaves +*) + +EXTENDS Naturals, Sequences, FiniteSets + +CONSTANTS + ConcurrencyEnabled, \* TRUE for olc_db, FALSE for db + MaxVersion \* Bound on version counter (typically 4) + +\* --- Node identity (fixed tree structure) --- +\* Nodes: Root, A, B, L1, L2, L3, L4 +\* Children relation (defines the tree): +\* Root -> [A, B] (child_index 0, 1) +\* A -> [L1, L2] (child_index 0, 1) +\* B -> [L3, L4] (child_index 0, 1) + +Nodes == {"Root", "A", "B", "L1", "L2", "L3", "L4"} +Inodes == {"Root", "A", "B"} +Leaves == {"L1", "L2", "L3", "L4"} + +\* Expected forward scan order +ScanOrder == <<"L1", "L2", "L3", "L4">> + +\* Tree topology: parent -> <> +Children(n) == + CASE n = "Root" -> <<"A", "B">> + [] n = "A" -> <<"L1", "L2">> + [] n = "B" -> <<"L3", "L4">> + [] OTHER -> <<>> \* leaves have no children + +NumChildren(n) == Len(Children(n)) + +Parent(n) == + CASE n = "A" -> "Root" + [] n = "B" -> "Root" + [] n = "L1" -> "A" + [] n = "L2" -> "A" + [] n = "L3" -> "B" + [] n = "L4" -> "B" + [] OTHER -> "None" + +IsLeaf(n) == n \in Leaves +IsInode(n) == n \in Inodes + +\* --- State variables --- +VARIABLES + \* Per-node version counter (even = unlocked, odd = write-locked) + ver, \* ver[n] \in 0..MaxVersion + + \* Iterator state + ipc, \* program counter + stack, \* sequence of [node, child_index, snap_ver] records + visited, \* sequence of leaves visited (in order) + restarts, \* count of restarts (for liveness reasoning) + + \* Writer state (only active when ConcurrencyEnabled) + wpc, \* writer program counter + w_target \* which inode the writer is modifying + +vars == <> + +\* --- Helper operators --- + +\* Stack entry constructor +Entry(node, ci, v) == [node |-> node, ci |-> ci, ver |-> v] + +\* Check if version is even (unlocked) and matches snapshot +CheckOK(node, snap_ver) == + IF ~ConcurrencyEnabled THEN TRUE + ELSE ver[node] = snap_ver /\ (snap_ver % 2 = 0) + +\* Version is even (can acquire read lock) +CanLock(node) == + IF ~ConcurrencyEnabled THEN TRUE + ELSE ver[node] % 2 = 0 + +\* Left-most leaf reachable from a node +RECURSIVE LeftMost(_) +LeftMost(n) == + IF IsLeaf(n) THEN n + ELSE LeftMost(Children(n)[1]) + +\* Next child index after ci in node n. 0 if no more. +NextChild(n, ci) == + IF ci + 1 <= NumChildren(n) THEN ci + 1 + ELSE 0 \* 0 means exhausted + +\* Get the i-th child (1-indexed) +GetChild(n, ci) == Children(n)[ci] + +\* Position of a leaf in the scan order (1-indexed). 0 if not found. +LeafPos(leaf) == + CASE leaf = "L1" -> 1 + [] leaf = "L2" -> 2 + [] leaf = "L3" -> 3 + [] leaf = "L4" -> 4 + [] OTHER -> 0 + +\* The leaf we need to seek to after a restart (successor of last visited). +\* If visited is empty, seek to L1 (first). Otherwise seek to successor. +SeekTarget == + IF visited = <<>> THEN 1 + ELSE LeafPos(visited[Len(visited)]) + 1 + +\* Find the path (sequence of child indices) from Root to the n-th leaf +\* in scan order. Returns a sequence of child indices for each level. +\* E.g., leaf 1 (L1): <<1, 1>>, leaf 3 (L3): <<2, 1>>, leaf 4 (L4): <<2, 2>> +SeekPath(pos) == + CASE pos = 1 -> <<1, 1>> \* Root[1]=A, A[1]=L1 + [] pos = 2 -> <<1, 2>> \* Root[1]=A, A[2]=L2 + [] pos = 3 -> <<2, 1>> \* Root[2]=B, B[1]=L3 + [] pos = 4 -> <<2, 2>> \* Root[2]=B, B[2]=L4 + [] OTHER -> <<>> + +\* --- Initial state --- +Init == + /\ ver = [n \in Nodes |-> 0] + /\ ipc = "start" + /\ stack = <<>> + /\ visited = <<>> + /\ restarts = 0 + /\ wpc = "idle" + /\ w_target = "Root" + +\* --- Iterator actions --- + +\* Start/Restart: lock root, descend toward the seek target. +\* On first call, seeks to leaf position 1 (left-most). +\* On restart after a check failure, seeks to successor of last visited. +IterStart == ipc = "start" /\ + LET target == SeekTarget IN + IF target > Len(ScanOrder) THEN + \* We've already visited everything — done + /\ ipc' = "done" + /\ UNCHANGED <> + ELSE IF ~CanLock("Root") THEN + \* Lock failed (writer holds root) — retry + /\ restarts' = restarts + 1 + /\ UNCHANGED <> + ELSE + \* Successful lock — begin descent toward target leaf + LET path == SeekPath(target) IN + /\ ipc' = "descend" + /\ stack' = <> + /\ UNCHANGED <> + +\* Descend: we have a stack with the current inode on top, ci points to +\* the child we want to descend into. Keep going until we reach a leaf. +IterDescend == ipc = "descend" /\ stack /= <<>> /\ + LET top == stack[Len(stack)] + node == top.node + ci == top.ci + child == GetChild(node, ci) + IN + \* Check the version of the node we're descending from + IF ~CheckOK(node, top.ver) THEN + \* Version check failed — full restart (seek to last visited + 1) + /\ ipc' = "start" + /\ stack' = <<>> + /\ restarts' = restarts + 1 + /\ UNCHANGED <> + ELSE IF IsLeaf(child) THEN + \* Reached a leaf — record visit, transition to "advance" + /\ ipc' = "advance" + /\ visited' = Append(visited, child) + /\ UNCHANGED <> + ELSE + \* Child is an inode — push it with the correct child_index for seek. + \* The child_index at the next level comes from the seek path. + LET target == SeekTarget + path == SeekPath(target) + depth == Len(stack) + 1 \* next level (1=root already on stack) + next_ci == IF depth <= Len(path) THEN path[depth] ELSE 1 + IN + /\ ipc' = "descend" + /\ stack' = Append(stack, Entry(child, next_ci, ver[child])) + /\ UNCHANGED <> + +\* Advance: find the next leaf after the current one. +\* This is try_next(): look for next sibling or backtrack up the stack. +IterAdvance == ipc = "advance" /\ stack /= <<>> /\ + LET top == stack[Len(stack)] + node == top.node + ci == top.ci + IN + \* Version check on the inode at top of stack + IF ~CheckOK(node, top.ver) THEN + \* Stale — restart with seek + /\ ipc' = "start" + /\ stack' = <<>> + /\ restarts' = restarts + 1 + /\ UNCHANGED <> + ELSE + LET nci == NextChild(node, ci) IN + IF nci /= 0 THEN + \* There is a next child — update top's ci and descend left-most + /\ stack' = [stack EXCEPT ![Len(stack)].ci = nci] + /\ ipc' = "descend_lm" + /\ UNCHANGED <> + ELSE + \* Exhausted this inode — pop and try parent (backtrack) + /\ stack' = SubSeq(stack, 1, Len(stack) - 1) + /\ ipc' = IF Len(stack) = 1 THEN "done" ELSE "advance" + /\ UNCHANGED <> + +\* Descend left-most: after advance finds a sibling, descend into its +\* left-most subtree. Always picks child_index 1. +IterDescendLM == ipc = "descend_lm" /\ stack /= <<>> /\ + LET top == stack[Len(stack)] + node == top.node + ci == top.ci + child == GetChild(node, ci) + IN + IF ~CheckOK(node, top.ver) THEN + /\ ipc' = "start" + /\ stack' = <<>> + /\ restarts' = restarts + 1 + /\ UNCHANGED <> + ELSE IF IsLeaf(child) THEN + /\ ipc' = "advance" + /\ visited' = Append(visited, child) + /\ UNCHANGED <> + ELSE + \* Push child inode, always pick first child (left-most descent) + /\ ipc' = "descend_lm" + /\ stack' = Append(stack, Entry(child, 1, ver[child])) + /\ UNCHANGED <> + +\* Terminal state +IterDone == ipc = "done" /\ UNCHANGED vars + +\* --- Writer actions (only when ConcurrencyEnabled) --- + +\* Writer picks a target inode and locks it (bumps version to odd) +WriterLock == ConcurrencyEnabled /\ wpc = "idle" /\ + \E n \in Inodes : + /\ ver[n] % 2 = 0 \* not already locked + /\ ver[n] + 1 <= MaxVersion \* don't exceed bound + /\ wpc' = "locked" + /\ w_target' = n + /\ ver' = [ver EXCEPT ![n] = ver[n] + 1] + /\ UNCHANGED <> + +\* Writer unlocks (bumps version to even) +WriterUnlock == ConcurrencyEnabled /\ wpc = "locked" /\ + /\ ver[w_target] + 1 <= MaxVersion \* don't exceed bound + /\ ver' = [ver EXCEPT ![w_target] = ver[w_target] + 1] + /\ wpc' = "idle" + /\ UNCHANGED <> + +\* --- Specification --- + +Next == + \/ IterStart + \/ IterDescend + \/ IterDescendLM + \/ IterAdvance + \/ IterDone + \/ WriterLock + \/ WriterUnlock + +Spec == Init /\ [][Next]_vars /\ WF_vars(Next) + +\* --- State Constraint (bounds exploration) --- +StateConstraint == restarts <= 3 + +\* --- Invariants and Properties --- + +\* Type invariant +TypeOK == + /\ \A n \in Nodes : ver[n] \in 0..MaxVersion + /\ ipc \in {"start", "descend", "descend_lm", "advance", "done"} + /\ visited \in Seq(Leaves) + /\ restarts \in Nat + +\* OrderPreservation: visited leaves are a prefix of the expected scan order +OrderPreservation == + /\ Len(visited) <= Len(ScanOrder) + /\ \A i \in 1..Len(visited) : visited[i] = ScanOrder[i] + +\* NoRepeat: no leaf appears twice +NoRepeat == + \A i, j \in 1..Len(visited) : i /= j => visited[i] /= visited[j] + +\* Completeness: when done, all leaves were visited +Completeness == + ipc = "done" => visited = ScanOrder + +\* NoStaleAct: if we're in "advance" or "descend" and acting on a stack entry, +\* that entry's version must still be current (OLC safety). +\* Note: This is implicitly enforced by CheckOK guards, but we verify it. +NoStaleAct == + (ipc \in {"advance", "descend"} /\ stack /= <<>>) => + LET top == stack[Len(stack)] IN + CheckOK(top.node, top.ver) + \* This is checked by the guards; if violated, we restart. + \* The real invariant is: we never append to visited[] with stale data. + +\* Termination (liveness): iterator eventually reaches "done" +Termination == <>(ipc = "done") + +============================================================================= diff --git a/spec/tla/OLCIteratorRemove.tla b/spec/tla/OLCIteratorRemove.tla new file mode 100644 index 00000000..cca5b4a6 --- /dev/null +++ b/spec/tla/OLCIteratorRemove.tla @@ -0,0 +1,371 @@ +------------------------- MODULE OLCIteratorRemove -------------------------- +(* Phase 1: Structural remove — writer removes a leaf, node collapses. + + Tree geometry: depth 3, width 2. The writer can remove ONE leaf (L2). + When L2 is removed from A, inode A collapses: A's remaining child (L1) + is promoted to Root's first child slot. + + Before: Root → [A, B], A → [L1, L2], B → [L3, L4] + After: Root → [L1, B], B → [L3, L4] + + The iterator's stale stack may reference A (now obsolete). The version + check on A detects this and triggers restart. + + Expected scan order: + Before removal: L1, L2, L3, L4 + After removal: L1, L3, L4 + + Key property: the iterator never visits a removed leaf, never skips + a surviving leaf, and visits surviving leaves in order. + + ConcurrencyEnabled: FALSE = sequential, TRUE = OLC. +*) + +EXTENDS Naturals, Sequences, FiniteSets + +CONSTANTS + ConcurrencyEnabled, + MaxVersion, + BugMode \* "none" | "skip_check" + +\* --- Nodes --- +Nodes == {"Root", "A", "B", "L1", "L2", "L3", "L4"} +Inodes == {"Root", "A", "B"} +Leaves == {"L1", "L2", "L3", "L4"} + +\* --- State variables --- +VARIABLES + ver, \* version counters + removed, \* TRUE if L2 has been removed (tree restructured) + ipc, \* iterator PC + stack, \* iterator stack + visited, \* leaves visited in order + restarts, \* restart count + wpc, \* writer PC: idle | locking_a | locked_a | locking_root | + \* locked_both | removing | unlocking | done + w_target \* (unused in this spec but kept for vars compat) + +vars == <> + +\* --- Dynamic tree topology --- + +\* Children depends on whether L2 has been removed +Children(n) == + IF ~removed THEN + CASE n = "Root" -> <<"A", "B">> + [] n = "A" -> <<"L1", "L2">> + [] n = "B" -> <<"L3", "L4">> + [] OTHER -> <<>> + ELSE + \* After removal: A collapsed, L1 promoted to Root[1] + CASE n = "Root" -> <<"L1", "B">> + [] n = "A" -> <<>> \* A is obsolete + [] n = "B" -> <<"L3", "L4">> + [] OTHER -> <<>> + +NumChildren(n) == Len(Children(n)) +GetChild(n, ci) == Children(n)[ci] + +IsLeaf(n) == n \in Leaves +IsInode(n) == n \in Inodes /\ (~removed \/ n /= "A") + +\* The current valid leaves in scan order +CurrentScanOrder == + IF ~removed THEN <<"L1", "L2", "L3", "L4">> + ELSE <<"L1", "L3", "L4">> + +\* --- Helpers --- + +Entry(node, ci, v) == [node |-> node, ci |-> ci, ver |-> v] + +CheckOK(node, snap_ver) == + IF ~ConcurrencyEnabled THEN TRUE + ELSE ver[node] = snap_ver /\ (snap_ver % 2 = 0) + +CanLock(node) == + IF ~ConcurrencyEnabled THEN TRUE + ELSE ver[node] % 2 = 0 + +NextChild(n, ci) == + IF ci + 1 <= NumChildren(n) THEN ci + 1 + ELSE 0 + +\* Seek target: position in CurrentScanOrder after last visited leaf. +\* Must account for the fact that CurrentScanOrder may have changed +\* (L2 removed). The seek finds the first leaf >= successor of last visited. +LeafPos(leaf) == + CASE leaf = "L1" -> 1 + [] leaf = "L2" -> 2 + [] leaf = "L3" -> 3 + [] leaf = "L4" -> 4 + [] OTHER -> 0 + +\* Given we last visited leaf at global position p, find the next leaf +\* that still exists in the current tree. +NextSurvivingPos(p) == + IF p >= 4 THEN 5 \* past end + ELSE IF p + 1 = 2 /\ removed THEN 3 \* skip removed L2 + ELSE p + 1 + +SeekTarget == + IF visited = <<>> THEN 1 + ELSE NextSurvivingPos(LeafPos(visited[Len(visited)])) + +\* Path from Root to leaf at global position, in current tree topology +SeekPath(pos) == + IF ~removed THEN + CASE pos = 1 -> <<1, 1>> \* Root[1]=A, A[1]=L1 + [] pos = 2 -> <<1, 2>> \* Root[1]=A, A[2]=L2 + [] pos = 3 -> <<2, 1>> \* Root[2]=B, B[1]=L3 + [] pos = 4 -> <<2, 2>> \* Root[2]=B, B[2]=L4 + [] OTHER -> <<>> + ELSE + \* After removal: Root → [L1, B], B → [L3, L4] + CASE pos = 1 -> <<1>> \* Root[1]=L1 (leaf directly) + [] pos = 3 -> <<2, 1>> \* Root[2]=B, B[1]=L3 + [] pos = 4 -> <<2, 2>> \* Root[2]=B, B[2]=L4 + [] OTHER -> <<>> + +\* --- Initial state --- +Init == + /\ ver = [n \in Nodes |-> 0] + /\ removed = FALSE + /\ ipc = "start" + /\ stack = <<>> + /\ visited = <<>> + /\ restarts = 0 + /\ wpc = "idle" + /\ w_target = "Root" + +\* --- Iterator actions --- + +IterStart == ipc = "start" /\ + LET target == SeekTarget IN + IF target > 4 THEN + /\ ipc' = "done" + /\ UNCHANGED <> + ELSE IF ~CanLock("Root") THEN + /\ restarts' = restarts + 1 + /\ UNCHANGED <> + ELSE + LET path == SeekPath(target) IN + /\ ipc' = "descend" + /\ stack' = <> + /\ UNCHANGED <> + +IterDescend == ipc = "descend" /\ stack /= <<>> /\ + LET top == stack[Len(stack)] + node == top.node + ci == top.ci + IN + IF ~CheckOK(node, top.ver) THEN + /\ ipc' = "start" + /\ stack' = <<>> + /\ restarts' = restarts + 1 + /\ UNCHANGED <> + ELSE IF NumChildren(node) = 0 THEN + \* Node is obsolete (A after collapse) — check should have caught this + \* but in case of race, restart + /\ ipc' = "start" + /\ stack' = <<>> + /\ restarts' = restarts + 1 + /\ UNCHANGED <> + ELSE + LET child == GetChild(node, ci) IN + IF IsLeaf(child) THEN + /\ ipc' = "advance" + /\ visited' = Append(visited, child) + /\ UNCHANGED <> + ELSE + LET target == SeekTarget + path == SeekPath(target) + depth == Len(stack) + 1 + next_ci == IF depth <= Len(path) THEN path[depth] ELSE 1 + IN + /\ ipc' = "descend" + /\ stack' = Append(stack, Entry(child, next_ci, ver[child])) + /\ UNCHANGED <> + +IterDescendLM == ipc = "descend_lm" /\ stack /= <<>> /\ + LET top == stack[Len(stack)] + node == top.node + ci == top.ci + IN + IF BugMode /= "skip_check" /\ ~CheckOK(node, top.ver) THEN + /\ ipc' = "start" + /\ stack' = <<>> + /\ restarts' = restarts + 1 + /\ UNCHANGED <> + ELSE + \* If stale (skip_check + version mismatch), the read is undefined. + \* Model as non-deterministic: could "see" any leaf (havoc). + LET stale == BugMode = "skip_check" /\ ~CheckOK(node, top.ver) IN + IF stale THEN + \* Havoc: non-deterministically visit any leaf + \E leaf \in Leaves : + /\ ipc' = "advance" + /\ visited' = Append(visited, leaf) + /\ UNCHANGED <> + ELSE IF NumChildren(node) = 0 THEN + /\ ipc' = "start" + /\ stack' = <<>> + /\ restarts' = restarts + 1 + /\ UNCHANGED <> + ELSE + LET child == GetChild(node, ci) IN + IF IsLeaf(child) THEN + /\ ipc' = "advance" + /\ visited' = Append(visited, child) + /\ UNCHANGED <> + ELSE + /\ ipc' = "descend_lm" + /\ stack' = Append(stack, Entry(child, 1, ver[child])) + /\ UNCHANGED <> + +IterAdvance == ipc = "advance" /\ stack /= <<>> /\ + LET top == stack[Len(stack)] + node == top.node + ci == top.ci + IN + \* BUG: skip_check — proceed without validating version + IF BugMode /= "skip_check" /\ ~CheckOK(node, top.ver) THEN + /\ ipc' = "start" + /\ stack' = <<>> + /\ restarts' = restarts + 1 + /\ UNCHANGED <> + ELSE + LET stale == BugMode = "skip_check" /\ ~CheckOK(node, top.ver) IN + IF stale THEN + \* Havoc: stale NextChild could go anywhere. + \* Non-deterministically: either find a "next" (descend to any leaf) + \* or exhaust (pop). Both are possible with garbage data. + \/ (\E leaf \in Leaves : + /\ ipc' = "advance" + /\ visited' = Append(visited, leaf) + /\ UNCHANGED <>) + \/ (/\ stack' = SubSeq(stack, 1, Len(stack) - 1) + /\ ipc' = IF Len(stack) = 1 THEN "done" ELSE "advance" + /\ UNCHANGED <>) + ELSE + LET nci == NextChild(node, ci) IN + IF nci /= 0 THEN + /\ stack' = [stack EXCEPT ![Len(stack)].ci = nci] + /\ ipc' = "descend_lm" + /\ UNCHANGED <> + ELSE + /\ stack' = SubSeq(stack, 1, Len(stack) - 1) + /\ ipc' = IF Len(stack) = 1 THEN "done" ELSE "advance" + /\ UNCHANGED <> + +IterDone == ipc = "done" /\ UNCHANGED vars + +\* --- Writer: Remove L2 (multi-step, like the real code) --- +\* Steps: lock A → lock Root → restructure → mark A obsolete → unlock Root + +WriterLockA == ConcurrencyEnabled /\ wpc = "idle" /\ ~removed /\ + /\ ver["A"] % 2 = 0 + /\ ver["A"] + 1 <= MaxVersion + /\ wpc' = "locked_a" + /\ ver' = [ver EXCEPT !["A"] = ver["A"] + 1] + /\ UNCHANGED <> + +WriterLockRoot == ConcurrencyEnabled /\ wpc = "locked_a" /\ + /\ ver["Root"] % 2 = 0 + /\ ver["Root"] + 1 <= MaxVersion + /\ wpc' = "locked_both" + /\ ver' = [ver EXCEPT !["Root"] = ver["Root"] + 1] + /\ UNCHANGED <> + +\* Perform the structural mutation: remove L2, collapse A, promote L1 +WriterRemove == ConcurrencyEnabled /\ wpc = "locked_both" /\ + /\ removed' = TRUE + /\ wpc' = "unlocking" + /\ UNCHANGED <> + +\* Unlock Root (A stays locked forever = obsolete, odd version permanently) +WriterUnlockRoot == ConcurrencyEnabled /\ wpc = "unlocking" /\ + /\ ver["Root"] + 1 <= MaxVersion + /\ ver' = [ver EXCEPT !["Root"] = ver["Root"] + 1] + /\ wpc' = "done" + /\ UNCHANGED <> + +WriterDone == wpc = "done" /\ UNCHANGED vars + +\* --- Specification --- + +Next == + \/ IterStart + \/ IterDescend + \/ IterDescendLM + \/ IterAdvance + \/ IterDone + \/ WriterLockA + \/ WriterLockRoot + \/ WriterRemove + \/ WriterUnlockRoot + \/ WriterDone + +Spec == Init /\ [][Next]_vars /\ WF_vars(Next) + +\* --- State Constraint --- +StateConstraint == restarts <= 4 + +\* --- Invariants --- + +TypeOK == + /\ \A n \in Nodes : ver[n] \in 0..MaxVersion + /\ ipc \in {"start", "descend", "descend_lm", "advance", "done"} + /\ removed \in BOOLEAN + /\ visited \in Seq(Leaves) + /\ restarts \in Nat + +\* OrderPreservation: visited leaves are always in the global key order +\* (L1 < L2 < L3 < L4). After removal, L2 may or may not have been +\* visited depending on timing, but order must be maintained. +OrderPreservation == + \A i \in 1..(Len(visited)-1) : + LeafPos(visited[i]) < LeafPos(visited[i+1]) + +\* NoRepeat: no leaf visited twice +NoRepeat == + \A i, j \in 1..Len(visited) : i /= j => visited[i] /= visited[j] + +\* NoRemovedAfterRemoval: once L2 is removed, it cannot be newly visited. +\* (It's OK if L2 was visited before removal.) +NoVisitRemoved == + removed => + \* If L2 appears in visited, it must be before the removal could + \* have been observed. Since removal happens atomically in our model, + \* we just check that L2 is not visited after a restart that occurred + \* post-removal. Simpler: L2 should not appear after any leaf that + \* follows it in order AND was visited after removal. + \* Actually simplest: L2 is never visited while removed=TRUE and + \* the last visited leaf was added in a state where removed=TRUE. + \* For now: just ensure if removed, no FUTURE visit adds L2. + TRUE \* Placeholder — real check below in SafeVisit + +\* The actually useful invariant: every leaf in visited[] existed in the tree +\* at the time the iterator descended to it. Since removal is atomic and +\* the iterator restarts on check failure, we verify: +\* If removed=TRUE and the iterator is past the restart point, L2 won't appear. +\* This is captured by OrderPreservation + the seek logic skipping L2. + +\* Completeness: when done, all currently-surviving leaves were visited. +\* The tricky case: if L2 was visited before removal, that's fine. +\* If removal happened before the scan reached L2's position, L2 is skipped. +Completeness == + ipc = "done" => + \* All surviving leaves must appear in visited + /\ \E i \in 1..Len(visited) : visited[i] = "L1" + /\ \E i \in 1..Len(visited) : visited[i] = "L3" + /\ \E i \in 1..Len(visited) : visited[i] = "L4" + \* B subtree always survives + /\ (removed => ~(\E i \in 1..Len(visited) : visited[i] = "L2") + \/ \* L2 can appear if it was visited before removal + TRUE) + +\* Canary: should be violated when writer removes L2 before iterator reaches it +L2AlwaysVisited == + ipc = "done" => \E i \in 1..Len(visited) : visited[i] = "L2" + +============================================================================= diff --git a/spec/tla/OLCIteratorRemove_Canary.cfg b/spec/tla/OLCIteratorRemove_Canary.cfg new file mode 100644 index 00000000..b81413ca --- /dev/null +++ b/spec/tla/OLCIteratorRemove_Canary.cfg @@ -0,0 +1,13 @@ +SPECIFICATION Spec + +CONSTANTS + ConcurrencyEnabled = TRUE + MaxVersion = 6 + BugMode = "none" + +CONSTRAINT + StateConstraint + +INVARIANTS + TypeOK + L2AlwaysVisited diff --git a/spec/tla/OLCIteratorRemove_OLC.cfg b/spec/tla/OLCIteratorRemove_OLC.cfg new file mode 100644 index 00000000..47229198 --- /dev/null +++ b/spec/tla/OLCIteratorRemove_OLC.cfg @@ -0,0 +1,15 @@ +SPECIFICATION Spec + +CONSTANTS + ConcurrencyEnabled = TRUE + MaxVersion = 6 + BugMode = "none" + +CONSTRAINT + StateConstraint + +INVARIANTS + TypeOK + OrderPreservation + NoRepeat + Completeness diff --git a/spec/tla/OLCIteratorRemove_SkipCheck.cfg b/spec/tla/OLCIteratorRemove_SkipCheck.cfg new file mode 100644 index 00000000..529f9954 --- /dev/null +++ b/spec/tla/OLCIteratorRemove_SkipCheck.cfg @@ -0,0 +1,15 @@ +SPECIFICATION Spec + +CONSTANTS + ConcurrencyEnabled = TRUE + MaxVersion = 6 + BugMode = "skip_check" + +CONSTRAINT + StateConstraint + +INVARIANTS + TypeOK + OrderPreservation + NoRepeat + Completeness diff --git a/spec/tla/OLCIteratorRoot.cfg b/spec/tla/OLCIteratorRoot.cfg new file mode 100644 index 00000000..badc1ab1 --- /dev/null +++ b/spec/tla/OLCIteratorRoot.cfg @@ -0,0 +1,13 @@ +SPECIFICATION Spec + +CONSTANTS + MaxVersion = 6 + BugMode = "none" + +CONSTRAINT + StateConstraint + +INVARIANTS + TypeOK + NoActOnInvalid + NoGarbage diff --git a/spec/tla/OLCIteratorRoot.tla b/spec/tla/OLCIteratorRoot.tla new file mode 100644 index 00000000..7a25763d --- /dev/null +++ b/spec/tla/OLCIteratorRoot.tla @@ -0,0 +1,198 @@ +-------------------------- MODULE OLCIteratorRoot ---------------------------- +(* Phase 5: Root pointer mutation and tree emptying. + + Models the two-level locking protocol at the root: + Level 1: root_pointer_lock (protects the root pointer variable) + Level 2: node version lock (protects the root node's contents) + + The iterator must: + 1. Take root_pointer_lock snapshot + 2. Load root pointer + 3. If null → return end() + 4. CHECK root_pointer_lock (validates loaded pointer is still current) + 5. Take node lock on loaded root + 6. Release root_pointer_lock + 7. Act on node + + The writer can: + - Set root = null (remove last key → tree empty) + - Replace root (tree structural change) + + TOCTOU: between step 2 and step 4, writer can change root. + Bug: skip step 4 → iterator uses stale/freed root pointer. +*) + +EXTENDS Naturals, Sequences + +CONSTANTS + MaxVersion, + BugMode \* "none" | "skip_rp_check" + +\* Possible root values +RootValues == {"L", "N", "null"} + +\* "Freed" represents memory that was reclaimed — accessing it is UB +AllNodes == {"L", "N", "null", "freed"} + +VARIABLES + rp_ver, \* root_pointer_lock version (even=unlocked, odd=locked) + root, \* current root pointer: "L" | "N" | "null" + + ipc, \* iterator PC + i_rp_snap, \* snapshot of rp_ver + i_loaded, \* what iterator loaded from root + visited, \* delivered results + restarts, + + wpc \* writer PC + +vars == <> + +\* --- Helpers --- +RPCheckOK == rp_ver = i_rp_snap /\ (rp_ver % 2 = 0) +RPCanLock == rp_ver % 2 = 0 + +\* --- Initial state: tree has root = "L" (a single leaf) --- +Init == + /\ rp_ver = 0 + /\ root = "L" + /\ ipc = "start" + /\ i_rp_snap = 0 + /\ i_loaded = "null" + /\ visited = <<>> + /\ restarts = 0 + /\ wpc = "idle" + +\* --- Iterator --- + +\* Step 1: take root_pointer_lock snapshot +IterStart == ipc = "start" /\ + IF ~RPCanLock THEN + /\ restarts' = restarts + 1 + /\ UNCHANGED <> + ELSE + /\ i_rp_snap' = rp_ver + /\ ipc' = "load_root" + /\ UNCHANGED <> + +\* Step 2: load root pointer (reads CURRENT value — may become stale) +IterLoadRoot == ipc = "load_root" /\ + /\ i_loaded' = root + /\ ipc' = "check_null" + /\ UNCHANGED <> + +\* Step 3: if null, return end() +IterCheckNull == ipc = "check_null" /\ + IF i_loaded = "null" THEN + /\ ipc' = "done" + /\ UNCHANGED <> + ELSE + /\ ipc' = "check_rp" + /\ UNCHANGED <> + +\* Step 4: CHECK root_pointer_lock — validates loaded root is still current +IterCheckRP == ipc = "check_rp" /\ + IF BugMode = "skip_rp_check" THEN + \* BUG: skip the check — proceed with potentially stale root + IF ~RPCheckOK THEN + \* Version changed — loaded root is stale. Havoc: could be anything + \E node \in AllNodes : + /\ i_loaded' = node + /\ ipc' = "act" + /\ UNCHANGED <> + ELSE + \* Version matches — loaded root is still valid + /\ ipc' = "act" + /\ UNCHANGED <> + ELSE + \* Correct code: validate + IF ~RPCheckOK THEN + /\ ipc' = "start" + /\ restarts' = restarts + 1 + /\ UNCHANGED <> + ELSE + /\ ipc' = "act" + /\ UNCHANGED <> + +\* Step 5-7: act on the loaded root (take node lock, traverse) +IterAct == ipc = "act" /\ + /\ visited' = Append(visited, i_loaded) + /\ ipc' = "done" + /\ UNCHANGED <> + +IterDone == ipc = "done" /\ UNCHANGED vars + +\* --- Writer: empty the tree (set root = null) --- + +WriterLockRP == wpc = "idle" /\ + /\ rp_ver % 2 = 0 + /\ rp_ver + 1 <= MaxVersion + /\ rp_ver' = rp_ver + 1 + /\ wpc' = "locked" + /\ UNCHANGED <> + +WriterEmpty == wpc = "locked" /\ + /\ root' = "null" + /\ wpc' = "mutated" + /\ UNCHANGED <> + +WriterUnlockRP == wpc = "mutated" /\ + /\ rp_ver + 1 <= MaxVersion + /\ rp_ver' = rp_ver + 1 + /\ wpc' = "done" + /\ UNCHANGED <> + +WriterDone == wpc = "done" /\ UNCHANGED vars + +\* --- Specification --- + +Next == + \/ IterStart + \/ IterLoadRoot + \/ IterCheckNull + \/ IterCheckRP + \/ IterAct + \/ IterDone + \/ WriterLockRP + \/ WriterEmpty + \/ WriterUnlockRP + \/ WriterDone + +Spec == Init /\ [][Next]_vars /\ WF_vars(Next) + +\* --- State Constraint --- +StateConstraint == restarts <= 3 + +\* --- Invariants --- + +TypeOK == + /\ rp_ver \in 0..MaxVersion + /\ root \in RootValues + /\ ipc \in {"start", "load_root", "check_null", "check_rp", "act", "done"} + /\ i_rp_snap \in 0..MaxVersion + /\ i_loaded \in AllNodes + /\ visited \in Seq(AllNodes) + /\ restarts \in Nat + /\ wpc \in {"idle", "locked", "mutated", "done"} + +\* NoStaleRoot: if the iterator acts, it acts on a VALID root (one that is +\* currently the root OR was the root at the time of a successful check). +\* Concretely: visited must never contain "freed" or "null" (acting on null = crash) +NoActOnInvalid == + \A i \in 1..Len(visited) : visited[i] \in {"L", "N"} + +\* SafeEmpty: if tree is empty when iterator finishes, visited is empty +\* (iterator correctly detected null and returned end()) +\* Note: if tree was non-empty when iterator started, it's fine to visit it +\* even if it was emptied later (snapshot consistency). + +\* The key safety property: iterator never dereferences a stale root pointer +\* that points to freed memory. In our model, "freed" = garbage value. +NoGarbage == + \A i \in 1..Len(visited) : visited[i] /= "freed" + +\* Canary: root is never emptied (should fail — proves writer interleaves) +RootNeverNull == + root /= "null" + +============================================================================= diff --git a/spec/tla/OLCIteratorRoot_Bug.cfg b/spec/tla/OLCIteratorRoot_Bug.cfg new file mode 100644 index 00000000..ef54def4 --- /dev/null +++ b/spec/tla/OLCIteratorRoot_Bug.cfg @@ -0,0 +1,13 @@ +SPECIFICATION Spec + +CONSTANTS + MaxVersion = 6 + BugMode = "skip_rp_check" + +CONSTRAINT + StateConstraint + +INVARIANTS + TypeOK + NoActOnInvalid + NoGarbage diff --git a/spec/tla/OLCIteratorRoot_Canary.cfg b/spec/tla/OLCIteratorRoot_Canary.cfg new file mode 100644 index 00000000..958cc19b --- /dev/null +++ b/spec/tla/OLCIteratorRoot_Canary.cfg @@ -0,0 +1,12 @@ +SPECIFICATION Spec + +CONSTANTS + MaxVersion = 6 + BugMode = "none" + +CONSTRAINT + StateConstraint + +INVARIANTS + TypeOK + RootNeverNull diff --git a/spec/tla/OLCIteratorVIS.cfg b/spec/tla/OLCIteratorVIS.cfg new file mode 100644 index 00000000..e568862c --- /dev/null +++ b/spec/tla/OLCIteratorVIS.cfg @@ -0,0 +1,15 @@ +SPECIFICATION Spec + +CONSTANTS + MaxVersion = 6 + BugMode = "none" + +CONSTRAINT + StateConstraint + +INVARIANTS + TypeOK + NoGarbage + OrderPreservation + Completeness + VISConsistency diff --git a/spec/tla/OLCIteratorVIS.tla b/spec/tla/OLCIteratorVIS.tla new file mode 100644 index 00000000..3b1e1db6 --- /dev/null +++ b/spec/tla/OLCIteratorVIS.tla @@ -0,0 +1,215 @@ +--------------------------- MODULE OLCIteratorVIS ---------------------------- +(* Phase 3: VIS (Value-In-Slot) TOCTOU model. + + Micro-model of the critical section where an iterator reads a packed + leaf (VIS) from a parent inode. The packed leaf has NO version lock — + the parent's version protects it. + + Geometry: One inode P with 3 child slots: + Slot 1: regular leaf L1 + Slot 2: VIS value V2 (mutable — writer can change it) + Slot 3: regular leaf L3 + + Forward scan: L1, V2, L3. + + The iterator: + 1. Arrives at P with version snapshot (i_snap = p_ver) + 2. Delivers L1 + 3. check1: validate p_ver == i_snap (before reading slot 2) + 4. Read slot 2: observe is_value_in_slot and get_child + 5. check2: validate p_ver == i_snap (after reading slot 2) + 6. Deliver slot 2 value + 7. Deliver L3, done + + The writer: + 1. Lock P (p_ver becomes odd) + 2. Mutate slot 2 (change VIS to different value) + 3. Unlock P (p_ver becomes next even) + + TOCTOU: Between check1 and check2, the writer can lock+mutate+unlock. + check2 catches this (version changed). Bug: skip check2 → stale/garbage read. +*) + +EXTENDS Naturals, Sequences + +CONSTANTS + MaxVersion, + BugMode \* "none" | "skip_check2" + +VARIABLES + p_ver, \* Parent inode version (even=unlocked, odd=locked) + slot2_value, \* Current value in slot 2: "V2" | "V2prime" + ipc, \* Iterator PC + i_snap, \* Iterator's version snapshot of P + i_read_val, \* What iterator read from slot 2 (may be stale) + visited, \* Delivered values + restarts, \* Restart count + wpc \* Writer PC: idle | locked | mutated | done + +vars == <> + +\* --- Helpers --- + +CheckOK == p_ver = i_snap /\ (p_ver % 2 = 0) +CanLock == p_ver % 2 = 0 + +\* All possible values that could appear in slot 2 (including garbage on havoc) +SlotValues == {"V2", "V2prime"} +AllValues == {"L1", "L3", "V2", "V2prime", "garbage"} + +\* --- Initial state --- +Init == + /\ p_ver = 0 + /\ slot2_value = "V2" + /\ ipc = "start" + /\ i_snap = 0 + /\ i_read_val = "V2" + /\ visited = <<>> + /\ restarts = 0 + /\ wpc = "idle" + +\* --- Iterator actions --- + +\* Take snapshot of parent version, deliver L1 +IterStart == ipc = "start" /\ + IF ~CanLock THEN + /\ restarts' = restarts + 1 + /\ UNCHANGED <> + ELSE + /\ i_snap' = p_ver + /\ visited' = <<"L1">> + /\ ipc' = "check1" + /\ UNCHANGED <> + +\* Check1: validate parent version before reading VIS slot +IterCheck1 == ipc = "check1" /\ + IF ~CheckOK THEN + \* Version changed — restart + /\ ipc' = "start" + /\ visited' = <<>> + /\ restarts' = restarts + 1 + /\ UNCHANGED <> + ELSE + /\ ipc' = "read_slot2" + /\ UNCHANGED <> + +\* Read slot 2: observe the current value +\* (This is the TOCTOU-vulnerable read — happens BETWEEN check1 and check2) +IterReadSlot2 == ipc = "read_slot2" /\ + /\ i_read_val' = slot2_value \* reads CURRENT value (may differ from snapshot time) + /\ ipc' = "check2" + /\ UNCHANGED <> + +\* Check2: validate parent version AFTER reading VIS slot +IterCheck2 == ipc = "check2" /\ + IF BugMode = "skip_check2" THEN + \* BUG: skip the check — deliver whatever was read + \* If version changed, the read was stale. Model with havoc. + IF ~CheckOK THEN + \* Stale read — havoc: could deliver any value + \E v \in AllValues : + /\ visited' = Append(visited, v) + /\ ipc' = "deliver_L3" + /\ UNCHANGED <> + ELSE + \* Version still matches — read is valid even without check + /\ visited' = Append(visited, i_read_val) + /\ ipc' = "deliver_L3" + /\ UNCHANGED <> + ELSE + \* Correct code: validate version + IF ~CheckOK THEN + /\ ipc' = "start" + /\ visited' = <<>> + /\ restarts' = restarts + 1 + /\ UNCHANGED <> + ELSE + \* Version matches — read is valid, deliver it + /\ visited' = Append(visited, i_read_val) + /\ ipc' = "deliver_L3" + /\ UNCHANGED <> + +\* Deliver L3 and finish +IterDeliverL3 == ipc = "deliver_L3" /\ + /\ visited' = Append(visited, "L3") + /\ ipc' = "done" + /\ UNCHANGED <> + +IterDone == ipc = "done" /\ UNCHANGED vars + +\* --- Writer actions --- + +WriterLock == wpc = "idle" /\ + /\ p_ver % 2 = 0 + /\ p_ver + 1 <= MaxVersion + /\ p_ver' = p_ver + 1 + /\ wpc' = "locked" + /\ UNCHANGED <> + +WriterMutate == wpc = "locked" /\ + /\ slot2_value' = "V2prime" + /\ wpc' = "mutated" + /\ UNCHANGED <> + +WriterUnlock == wpc = "mutated" /\ + /\ p_ver + 1 <= MaxVersion + /\ p_ver' = p_ver + 1 + /\ wpc' = "done" + /\ UNCHANGED <> + +WriterDone == wpc = "done" /\ UNCHANGED vars + +\* --- Specification --- + +Next == + \/ IterStart + \/ IterCheck1 + \/ IterReadSlot2 + \/ IterCheck2 + \/ IterDeliverL3 + \/ IterDone + \/ WriterLock + \/ WriterMutate + \/ WriterUnlock + \/ WriterDone + +Spec == Init /\ [][Next]_vars /\ WF_vars(Next) + +\* --- State Constraint --- +StateConstraint == restarts <= 3 + +\* --- Invariants --- + +TypeOK == + /\ p_ver \in 0..MaxVersion + /\ slot2_value \in SlotValues + /\ ipc \in {"start", "check1", "read_slot2", "check2", "deliver_L3", "done"} + /\ i_snap \in 0..MaxVersion + /\ i_read_val \in AllValues + /\ visited \in Seq(AllValues) + /\ restarts \in Nat + /\ wpc \in {"idle", "locked", "mutated", "done"} + +\* NoGarbage: the delivered slot2 value must be a real slot value, not garbage +NoGarbage == + Len(visited) >= 2 => visited[2] \in SlotValues + +\* OrderPreservation: L1 is always first, L3 is always last +OrderPreservation == + /\ (Len(visited) >= 1 => visited[1] = "L1") + /\ (Len(visited) >= 3 => visited[3] = "L3") + +\* Completeness: when done, exactly 3 values delivered +Completeness == + ipc = "done" => Len(visited) = 3 + +\* VISConsistency: the slot2 value delivered is one that actually existed +\* in slot2 at some point (either "V2" or "V2prime") +VISConsistency == + Len(visited) >= 2 => visited[2] \in {"V2", "V2prime"} + +\* Canary: slot2 is never mutated (should FAIL — proves writer interleaves) +SlotNeverMutated == + slot2_value = "V2" + +============================================================================= diff --git a/spec/tla/OLCIteratorVIS_Bug.cfg b/spec/tla/OLCIteratorVIS_Bug.cfg new file mode 100644 index 00000000..aedfdafa --- /dev/null +++ b/spec/tla/OLCIteratorVIS_Bug.cfg @@ -0,0 +1,14 @@ +SPECIFICATION Spec + +CONSTANTS + MaxVersion = 6 + BugMode = "skip_check2" + +CONSTRAINT + StateConstraint + +INVARIANTS + TypeOK + NoGarbage + OrderPreservation + VISConsistency diff --git a/spec/tla/OLCIteratorVIS_Canary.cfg b/spec/tla/OLCIteratorVIS_Canary.cfg new file mode 100644 index 00000000..64124b2b --- /dev/null +++ b/spec/tla/OLCIteratorVIS_Canary.cfg @@ -0,0 +1,12 @@ +SPECIFICATION Spec + +CONSTANTS + MaxVersion = 6 + BugMode = "none" + +CONSTRAINT + StateConstraint + +INVARIANTS + TypeOK + SlotNeverMutated diff --git a/spec/tla/OLCIterator_Bug850.tla b/spec/tla/OLCIterator_Bug850.tla new file mode 100644 index 00000000..10091ad4 --- /dev/null +++ b/spec/tla/OLCIterator_Bug850.tla @@ -0,0 +1,229 @@ +--------------------------- MODULE OLCIterator_Bug850 ------------------------- +(* Bug injection: simulate the #850 backtrack skip bug. + + The real bug: after exhausting a node's children and popping it, + the iterator failed to continue ascending — it stopped and reported + end() prematurely, skipping all leaves in sibling subtrees. + + We inject this by changing IterAdvance: when a node is exhausted, + instead of popping and continuing to try the parent, go directly + to "done". This should violate Completeness. + + Also tests: if IterAdvance skips the version check, the model + should catch NoStaleAct or OrderPreservation violations. +*) + +EXTENDS Naturals, Sequences, FiniteSets + +CONSTANTS + ConcurrencyEnabled, + MaxVersion, + BugMode \* "skip_backtrack" | "skip_check" | "none" + +Nodes == {"Root", "A", "B", "L1", "L2", "L3", "L4"} +Inodes == {"Root", "A", "B"} +Leaves == {"L1", "L2", "L3", "L4"} + +ScanOrder == <<"L1", "L2", "L3", "L4">> + +Children(n) == + CASE n = "Root" -> <<"A", "B">> + [] n = "A" -> <<"L1", "L2">> + [] n = "B" -> <<"L3", "L4">> + [] OTHER -> <<>> + +NumChildren(n) == Len(Children(n)) + +IsLeaf(n) == n \in Leaves +IsInode(n) == n \in Inodes + +VARIABLES ver, ipc, stack, visited, restarts, wpc, w_target + +vars == <> + +Entry(node, ci, v) == [node |-> node, ci |-> ci, ver |-> v] + +CheckOK(node, snap_ver) == + IF ~ConcurrencyEnabled THEN TRUE + ELSE ver[node] = snap_ver /\ (snap_ver % 2 = 0) + +CanLock(node) == + IF ~ConcurrencyEnabled THEN TRUE + ELSE ver[node] % 2 = 0 + +NextChild(n, ci) == + IF ci + 1 <= NumChildren(n) THEN ci + 1 + ELSE 0 + +GetChild(n, ci) == Children(n)[ci] + +LeafPos(leaf) == + CASE leaf = "L1" -> 1 + [] leaf = "L2" -> 2 + [] leaf = "L3" -> 3 + [] leaf = "L4" -> 4 + [] OTHER -> 0 + +SeekTarget == + IF visited = <<>> THEN 1 + ELSE LeafPos(visited[Len(visited)]) + 1 + +SeekPath(pos) == + CASE pos = 1 -> <<1, 1>> + [] pos = 2 -> <<1, 2>> + [] pos = 3 -> <<2, 1>> + [] pos = 4 -> <<2, 2>> + [] OTHER -> <<>> + +Init == + /\ ver = [n \in Nodes |-> 0] + /\ ipc = "start" + /\ stack = <<>> + /\ visited = <<>> + /\ restarts = 0 + /\ wpc = "idle" + /\ w_target = "Root" + +\* --- Iterator --- + +IterStart == ipc = "start" /\ + LET target == IF BugMode = "restart_from_beginning" THEN 1 + ELSE SeekTarget + IN + IF target > Len(ScanOrder) THEN + /\ ipc' = "done" + /\ UNCHANGED <> + ELSE IF ~CanLock("Root") THEN + /\ restarts' = restarts + 1 + /\ UNCHANGED <> + ELSE + LET path == SeekPath(target) IN + /\ ipc' = "descend" + /\ stack' = <> + /\ UNCHANGED <> + +IterDescend == ipc = "descend" /\ stack /= <<>> /\ + LET top == stack[Len(stack)] + node == top.node + ci == top.ci + child == GetChild(node, ci) + IN + IF ~CheckOK(node, top.ver) THEN + /\ ipc' = "start" + /\ stack' = <<>> + /\ restarts' = restarts + 1 + /\ UNCHANGED <> + ELSE IF IsLeaf(child) THEN + /\ ipc' = "advance" + /\ visited' = Append(visited, child) + /\ UNCHANGED <> + ELSE + LET target == SeekTarget + path == SeekPath(target) + depth == Len(stack) + 1 + next_ci == IF depth <= Len(path) THEN path[depth] ELSE 1 + IN + /\ ipc' = "descend" + /\ stack' = Append(stack, Entry(child, next_ci, ver[child])) + /\ UNCHANGED <> + +IterDescendLM == ipc = "descend_lm" /\ stack /= <<>> /\ + LET top == stack[Len(stack)] + node == top.node + ci == top.ci + child == GetChild(node, ci) + IN + IF ~CheckOK(node, top.ver) THEN + /\ ipc' = "start" + /\ stack' = <<>> + /\ restarts' = restarts + 1 + /\ UNCHANGED <> + ELSE IF IsLeaf(child) THEN + /\ ipc' = "advance" + /\ visited' = Append(visited, child) + /\ UNCHANGED <> + ELSE + /\ ipc' = "descend_lm" + /\ stack' = Append(stack, Entry(child, 1, ver[child])) + /\ UNCHANGED <> + +\* BUG INJECTION: IterAdvance +IterAdvance == ipc = "advance" /\ stack /= <<>> /\ + LET top == stack[Len(stack)] + node == top.node + ci == top.ci + IN + \* BUG: skip_check — don't validate version before acting + IF BugMode /= "skip_check" /\ ~CheckOK(node, top.ver) THEN + /\ ipc' = "start" + /\ stack' = <<>> + /\ restarts' = restarts + 1 + /\ UNCHANGED <> + ELSE + LET nci == NextChild(node, ci) IN + IF nci /= 0 THEN + /\ stack' = [stack EXCEPT ![Len(stack)].ci = nci] + /\ ipc' = "descend_lm" + /\ UNCHANGED <> + ELSE + \* BUG: skip_backtrack — stop instead of ascending to parent + IF BugMode = "skip_backtrack" THEN + /\ ipc' = "done" + /\ stack' = <<>> + /\ UNCHANGED <> + ELSE + /\ stack' = SubSeq(stack, 1, Len(stack) - 1) + /\ ipc' = IF Len(stack) = 1 THEN "done" ELSE "advance" + /\ UNCHANGED <> + +IterDone == ipc = "done" /\ UNCHANGED vars + +\* --- Writer --- + +WriterLock == ConcurrencyEnabled /\ wpc = "idle" /\ + \E n \in Inodes : + /\ ver[n] % 2 = 0 + /\ ver[n] + 1 <= MaxVersion + /\ wpc' = "locked" + /\ w_target' = n + /\ ver' = [ver EXCEPT ![n] = ver[n] + 1] + /\ UNCHANGED <> + +WriterUnlock == ConcurrencyEnabled /\ wpc = "locked" /\ + /\ ver[w_target] + 1 <= MaxVersion + /\ ver' = [ver EXCEPT ![w_target] = ver[w_target] + 1] + /\ wpc' = "idle" + /\ UNCHANGED <> + +Next == + \/ IterStart + \/ IterDescend + \/ IterDescendLM + \/ IterAdvance + \/ IterDone + \/ WriterLock + \/ WriterUnlock + +Spec == Init /\ [][Next]_vars /\ WF_vars(Next) + +\* --- Constraints and Properties --- + +StateConstraint == restarts <= 3 + +TypeOK == + /\ \A n \in Nodes : ver[n] \in 0..MaxVersion + /\ ipc \in {"start", "descend", "descend_lm", "advance", "done"} + /\ visited \in Seq(Leaves) + /\ restarts \in Nat + +OrderPreservation == + /\ Len(visited) <= Len(ScanOrder) + /\ \A i \in 1..Len(visited) : visited[i] = ScanOrder[i] + +NoRepeat == + \A i, j \in 1..Len(visited) : i /= j => visited[i] /= visited[j] + +Completeness == + ipc = "done" => visited = ScanOrder + +============================================================================= diff --git a/spec/tla/OLCIterator_Bug850_Backtrack.cfg b/spec/tla/OLCIterator_Bug850_Backtrack.cfg new file mode 100644 index 00000000..03640522 --- /dev/null +++ b/spec/tla/OLCIterator_Bug850_Backtrack.cfg @@ -0,0 +1,13 @@ +SPECIFICATION Spec + +CONSTANTS + ConcurrencyEnabled = FALSE + MaxVersion = 4 + BugMode = "skip_backtrack" + +CONSTRAINT + StateConstraint + +INVARIANTS + TypeOK + Completeness diff --git a/spec/tla/OLCIterator_Bug850_NoSeek.cfg b/spec/tla/OLCIterator_Bug850_NoSeek.cfg new file mode 100644 index 00000000..e1cec6e7 --- /dev/null +++ b/spec/tla/OLCIterator_Bug850_NoSeek.cfg @@ -0,0 +1,13 @@ +SPECIFICATION Spec + +CONSTANTS + ConcurrencyEnabled = TRUE + MaxVersion = 6 + BugMode = "restart_from_beginning" + +CONSTRAINT + StateConstraint + +INVARIANTS + TypeOK + NoRepeat diff --git a/spec/tla/OLCIterator_Bug850_SkipCheck.cfg b/spec/tla/OLCIterator_Bug850_SkipCheck.cfg new file mode 100644 index 00000000..529f9954 --- /dev/null +++ b/spec/tla/OLCIterator_Bug850_SkipCheck.cfg @@ -0,0 +1,15 @@ +SPECIFICATION Spec + +CONSTANTS + ConcurrencyEnabled = TRUE + MaxVersion = 6 + BugMode = "skip_check" + +CONSTRAINT + StateConstraint + +INVARIANTS + TypeOK + OrderPreservation + NoRepeat + Completeness diff --git a/spec/tla/OLCIterator_OLC.cfg b/spec/tla/OLCIterator_OLC.cfg new file mode 100644 index 00000000..9cf6c57c --- /dev/null +++ b/spec/tla/OLCIterator_OLC.cfg @@ -0,0 +1,14 @@ +SPECIFICATION Spec + +CONSTANTS + ConcurrencyEnabled = TRUE + MaxVersion = 6 + +CONSTRAINT + StateConstraint + +INVARIANTS + TypeOK + OrderPreservation + NoRepeat + Completeness diff --git a/spec/tla/OLCIterator_Seq.cfg b/spec/tla/OLCIterator_Seq.cfg new file mode 100644 index 00000000..0c847c7a --- /dev/null +++ b/spec/tla/OLCIterator_Seq.cfg @@ -0,0 +1,11 @@ +SPECIFICATION Spec + +CONSTANTS + ConcurrencyEnabled = FALSE + MaxVersion = 4 + +INVARIANTS + TypeOK + OrderPreservation + NoRepeat + Completeness diff --git a/spec/tla/OLCKeyViewChain.cfg b/spec/tla/OLCKeyViewChain.cfg new file mode 100644 index 00000000..aa5b41ce --- /dev/null +++ b/spec/tla/OLCKeyViewChain.cfg @@ -0,0 +1,15 @@ +SPECIFICATION Spec + +CONSTANTS + MaxVersion = 6 + OBSOLETE = 99 + +INVARIANTS + NoDataLoss + ChainMembershipCorrect + WellFormedness + +CONSTRAINT + StateConstraint + +CHECK_DEADLOCK FALSE diff --git a/spec/tla/OLCKeyViewChain.tla b/spec/tla/OLCKeyViewChain.tla new file mode 100644 index 00000000..21459757 --- /dev/null +++ b/spec/tla/OLCKeyViewChain.tla @@ -0,0 +1,295 @@ +--------------------------- MODULE OLCKeyViewChain ------------------------ +\* Stage 11: Variable-length keys with shared prefix and VIS. +\* +\* Models the critical scenario where two keys share a prefix: +\* Key A (short): value stored as VIS in shared_node +\* Key B (long): path continues through shared_node → chain_B → leaf_B +\* +\* Tree structure: +\* parent → shared_node(count depends on VIS + child) +\* ├── VIS entry (key A's value, bitmask-tracked) +\* └── chain_B → leaf_B (key B's exclusive path) +\* +\* The critical invariant: chain identification for key B must NOT +\* include shared_node when it has a VIS entry (count should be 2). +\* If VIS is invisible to count (the bug), shared_node appears to have +\* count=1, and removing key B would incorrectly cut shared_node, +\* LOSING key A's value. +\* +\* This stage verifies: +\* 1. Correct count (VIS-aware): chain identification stops at shared_node +\* 2. Buggy count (VIS-invisible): chain identification incorrectly +\* includes shared_node → data loss +\* 3. Concurrent insert/remove of key A while key B is being removed + +EXTENDS Integers + +CONSTANTS MaxVersion, OBSOLETE + +VARIABLES + \* Parent node (above shared_node) + p_ver, + p_count, \* >= 2 (shared_node + at least one sibling) + + \* Shared node (the node where keys A and B diverge) + s_ver, + s_has_vis, \* TRUE if key A's VIS entry is present + s_has_child_b, \* TRUE if pointer to chain_B is present + \* Correct count: s_has_vis + s_has_child_b (+ other children) + \* Buggy count: only counts non-null slots (misses VIS with value=0) + + \* Chain B node (key B's exclusive chain below shared_node) + cb_ver, + + \* Remover B: removing key B (chain cut through chain_B) + rbpc, \* idle|lock_cb|eval_shared|validate_shared| + \* upgrade_shared|eval_parent|cut|done|restart + rb_cb_locked, + rb_s_locked, \* TRUE if shared_node locked as chain member (BUG path) + rb_cached_ver, + rb_chain_includes_shared, \* TRUE if chain identification included shared_node + + \* Inserter/Remover A: can insert or remove key A's VIS entry + apc, \* idle|lock_s|insert_vis|remove_vis|unlock|done + a_op \* "insert" or "remove" + +vars == <> + +\* The CORRECT count of shared_node's children +CorrectCount == (IF s_has_vis THEN 1 ELSE 0) + (IF s_has_child_b THEN 1 ELSE 0) + +\* BUGGY count: only counts non-null slots. If VIS value=0, pack(0)=NULL, +\* so the VIS entry is invisible. This is the bug we're fixing. +\* Model this by assuming VIS entry has value=0 (worst case). +BuggyCount == (IF s_has_child_b THEN 1 ELSE 0) \* VIS always invisible + +\* Chain membership precondition (correct version) +IsChainMember == CorrectCount = 1 + +\* BUGGY chain membership (for bug demonstration) +BuggyIsChainMember == BuggyCount = 1 + +----------------------------------------------------------------------------- +Init == + /\ p_ver = 0 /\ p_count = 2 + /\ s_ver = 0 /\ s_has_vis = TRUE /\ s_has_child_b = TRUE + /\ cb_ver = 0 + /\ rbpc = "idle" + /\ rb_cb_locked = FALSE /\ rb_s_locked = FALSE + /\ rb_cached_ver = 0 /\ rb_chain_includes_shared = FALSE + /\ apc = "idle" /\ a_op = "remove" + +----------------------------------------------------------------------------- +\* REMOVER B: removing key B via chain cut + +\* Lock chain_B (bottom of key B's exclusive chain) +RBLockCB == + /\ rbpc = "idle" + /\ cb_ver % 2 = 0 /\ cb_ver # OBSOLETE + /\ s_has_child_b = TRUE \* chain_B still exists + /\ cb_ver' = cb_ver + 1 + /\ rb_cb_locked' = TRUE + /\ rbpc' = "eval_shared" + /\ UNCHANGED <> + +\* Evaluate shared_node for chain membership +RBEvalShared == + /\ rbpc = "eval_shared" + /\ rb_cached_ver' = s_ver + /\ rbpc' = "validate_shared" + /\ UNCHANGED <> + +\* Validate and check chain membership +RBValidateShared == + /\ rbpc = "validate_shared" + /\ IF s_ver = rb_cached_ver /\ s_ver % 2 = 0 + THEN \* Version valid — check chain membership using CORRECT count + IF IsChainMember + THEN \* shared_node IS a chain member (count=1) + \* This means only chain_B exists, no VIS → safe to include + /\ rb_chain_includes_shared' = TRUE + /\ rbpc' = "upgrade_shared" + ELSE \* shared_node is NOT a chain member (count>=2) + \* VIS entry present → shared_node is the CPP boundary + /\ rb_chain_includes_shared' = FALSE + /\ rbpc' = "eval_parent_as_cpp" + ELSE \* Version changed — re-read + /\ rbpc' = "eval_shared" + /\ UNCHANGED rb_chain_includes_shared + /\ UNCHANGED <> + +\* Upgrade shared_node to write (chain member path) +RBUpgradeShared == + /\ rbpc = "upgrade_shared" + /\ IF s_ver = rb_cached_ver /\ s_ver % 2 = 0 + THEN /\ s_ver' = s_ver + 1 + /\ rb_s_locked' = TRUE + /\ rbpc' = "eval_parent_as_cpp" + ELSE /\ rbpc' = "eval_shared" \* retry + /\ UNCHANGED <> + /\ UNCHANGED <> + +\* Evaluate parent as CPP (shared_node is either chain member or CPP itself) +RBEvalParentAsCPP == + /\ rbpc = "eval_parent_as_cpp" + /\ rb_cached_ver' = p_ver + /\ rbpc' = "validate_parent" + /\ UNCHANGED <> + +RBValidateParent == + /\ rbpc = "validate_parent" + /\ IF p_ver = rb_cached_ver /\ p_ver % 2 = 0 + THEN /\ p_ver' = p_ver + 1 \* lock parent as CPP + /\ rbpc' = "cut" + ELSE /\ rbpc' = "eval_parent_as_cpp" + /\ UNCHANGED p_ver + /\ UNCHANGED <> + +\* CUT +RBCut == + /\ rbpc = "cut" + /\ IF rb_chain_includes_shared + THEN \* Cut includes shared_node: remove shared_node from parent + /\ p_count' = p_count - 1 + /\ p_ver' = p_ver + 1 \* unlock parent + /\ s_ver' = OBSOLETE \* obsolete shared_node + /\ cb_ver' = OBSOLETE \* obsolete chain_B + /\ s_has_child_b' = FALSE + /\ UNCHANGED s_has_vis \* VIS entry lost if it existed! + ELSE \* Cut only chain_B: remove chain_B from shared_node + /\ s_has_child_b' = FALSE + /\ IF rb_s_locked + THEN s_ver' = s_ver + 1 \* unlock shared (was locked as CPP? no...) + ELSE s_ver' = s_ver \* shared wasn't locked + /\ p_ver' = p_ver + 1 \* unlock parent (CPP) + /\ cb_ver' = OBSOLETE + /\ UNCHANGED <> + /\ rb_cb_locked' = FALSE /\ rb_s_locked' = FALSE + /\ rbpc' = "done" + /\ UNCHANGED <> + +RBRestart == + /\ rbpc = "restart" + /\ cb_ver' = IF rb_cb_locked THEN cb_ver + 1 ELSE cb_ver + /\ s_ver' = IF rb_s_locked THEN s_ver + 1 ELSE s_ver + /\ rb_cb_locked' = FALSE /\ rb_s_locked' = FALSE + /\ rbpc' = "idle" + /\ UNCHANGED <> + +RBDone == + /\ rbpc = "done" + /\ rbpc' = "idle" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +\* ACTOR A: insert or remove key A's VIS entry in shared_node + +AChoose == + /\ apc = "idle" + /\ \E op \in {"insert", "remove"} : + /\ (op = "insert" => ~s_has_vis) \* can only insert if not present + /\ (op = "remove" => s_has_vis) \* can only remove if present + /\ a_op' = op + /\ apc' = "lock_s" + /\ UNCHANGED <> + +ALockS == + /\ apc = "lock_s" + /\ s_ver % 2 = 0 /\ s_ver # OBSOLETE /\ s_ver <= MaxVersion + /\ s_ver' = s_ver + 1 + /\ apc' = "write" + /\ UNCHANGED <> + +AWrite == + /\ apc = "write" + /\ IF a_op = "insert" + THEN s_has_vis' = TRUE + ELSE s_has_vis' = FALSE + /\ apc' = "unlock" + /\ UNCHANGED <> + +AUnlock == + /\ apc = "unlock" + /\ s_ver' = s_ver + 1 + /\ apc' = "idle" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +Step == + \/ RBLockCB \/ RBEvalShared \/ RBValidateShared \/ RBUpgradeShared + \/ RBEvalParentAsCPP \/ RBValidateParent \/ RBCut \/ RBRestart \/ RBDone + \/ AChoose \/ ALockS \/ AWrite \/ AUnlock + +Spec == Init /\ [][Step]_vars + +StateConstraint == + /\ p_ver <= MaxVersion + /\ (s_ver # OBSOLETE => s_ver <= MaxVersion) + /\ (cb_ver # OBSOLETE => cb_ver <= MaxVersion) + +----------------------------------------------------------------------------- +\* INVARIANTS + +\* CRITICAL: If chain cut includes shared_node, then at CUT TIME +\* shared_node must NOT have a VIS entry. Otherwise key A's value is lost. +NoDataLoss == + (rbpc = "cut" /\ rb_chain_includes_shared) => ~s_has_vis + +\* Chain membership was correctly evaluated: if shared_node is included +\* AND we reach cut, the VIS entry must have been absent when we validated. +\* (The OLC version check ensures our read was consistent.) +ChainMembershipCorrect == + (rbpc = "cut" /\ rb_chain_includes_shared) => ~s_has_vis + +\* Well-formedness: parent count stays valid +WellFormedness == p_count >= 1 + +----------------------------------------------------------------------------- +\* BUGGY VARIANT: Uses BuggyIsChainMember (VIS invisible to count) + +BuggyRBValidateShared == + /\ rbpc = "validate_shared" + /\ IF s_ver = rb_cached_ver /\ s_ver % 2 = 0 + THEN IF BuggyIsChainMember \* <-- THE BUG: ignores VIS entry + THEN /\ rb_chain_includes_shared' = TRUE + /\ rbpc' = "upgrade_shared" + ELSE /\ rb_chain_includes_shared' = FALSE + /\ rbpc' = "eval_parent_as_cpp" + ELSE /\ rbpc' = "eval_shared" + /\ UNCHANGED rb_chain_includes_shared + /\ UNCHANGED <> + +BuggyStep == + \/ RBLockCB \/ RBEvalShared \/ BuggyRBValidateShared \/ RBUpgradeShared + \/ RBEvalParentAsCPP \/ RBValidateParent \/ RBCut \/ RBRestart \/ RBDone + \/ AChoose \/ ALockS \/ AWrite \/ AUnlock + +BuggySpec == Init /\ [][BuggyStep]_vars + +============================================================================= diff --git a/spec/tla/OLCKeyViewChain_BugDemo.cfg b/spec/tla/OLCKeyViewChain_BugDemo.cfg new file mode 100644 index 00000000..dc27af2c --- /dev/null +++ b/spec/tla/OLCKeyViewChain_BugDemo.cfg @@ -0,0 +1,14 @@ +\* Bug demonstration: uses BuggyCount (VIS invisible to nullptr scan). +\* NoDataLoss SHOULD BE VIOLATED — demonstrating the key_view VIS bug. +SPECIFICATION BuggySpec + +CONSTANTS + MaxVersion = 6 + OBSOLETE = 99 + +INVARIANT NoDataLoss + +CONSTRAINT + StateConstraint + +CHECK_DEADLOCK FALSE diff --git a/spec/tla/OLCSlot.cfg b/spec/tla/OLCSlot.cfg new file mode 100644 index 00000000..118e6bf4 --- /dev/null +++ b/spec/tla/OLCSlot.cfg @@ -0,0 +1,10 @@ +SPECIFICATION Spec + +CONSTANTS + MaxVersion = 6 + +INVARIANTS + SnapshotConsistency + NoDereferenceValue + WriterProtocol + UnlockedConsistency diff --git a/spec/tla/OLCSlot.tla b/spec/tla/OLCSlot.tla new file mode 100644 index 00000000..789eb4b8 --- /dev/null +++ b/spec/tla/OLCSlot.tla @@ -0,0 +1,199 @@ +--------------------------- MODULE OLCSlot -------------------------------- +\* Stage 2: OLC protocol correctness for a single slot. +\* +\* One writer inserts/removes values (including 0) and pointers. +\* One reader reads (slot, bitmask), validates version, interprets. +\* +\* Verifies: reader never acts on inconsistent (slot, bitmask) pair, +\* and never dereferences a packed value as a pointer. + +EXTENDS Integers, FiniteSets + +CONSTANTS + MaxVersion \* Bound on version counter (e.g., 6) + +VARIABLES + \* Shared state (the single slot in the inode) + slot, \* 0=NULL, 1=nonzero_value, -1=pointer + bitmask, \* TRUE if slot holds a packed value + version, \* Even=unlocked, Odd=write-locked + + \* Writer state + wpc, \* idle|choose|lock|write_slot|write_bitmask|unlock + wval, \* What writer will store (-1, 0, or 1) + wbm, \* What bitmask writer will set + + \* Reader state + rpc, \* idle|read_slot|read_bitmask|validate|interpret|done + rver, \* Version captured at start + rslot, \* Local copy of slot + rbitmask \* Local copy of bitmask + +vars == <> + +----------------------------------------------------------------------------- +\* INITIAL STATE + +Init == + /\ slot = 0 + /\ bitmask = FALSE + /\ version = 0 + /\ wpc = "idle" + /\ wval = 0 + /\ wbm = FALSE + /\ rpc = "idle" + /\ rver = 0 + /\ rslot = 0 + /\ rbitmask = FALSE + +----------------------------------------------------------------------------- +\* WRITER ACTIONS + +\* Writer chooses to insert a value (0 or 1) or pointer (-1), or remove +WriterChoose == + /\ wpc = "idle" + /\ version <= MaxVersion \* bound version growth + /\ \E v \in {-1, 0, 1}, b \in {TRUE, FALSE} : + \* Valid operations: + \* (0, FALSE) = remove/clear slot + \* (0, TRUE) = insert value 0 (the critical case!) + \* (1, TRUE) = insert value 1 (nonzero value) + \* (-1, FALSE) = insert pointer + /\ (v > 0 => b = TRUE) \* positive values MUST have bitmask + /\ (v = -1 => b = FALSE) \* pointer never has bitmask + /\ (v = 0 /\ b = FALSE => TRUE) \* remove is always valid + /\ wval' = v + /\ wbm' = b + /\ wpc' = "lock" + /\ UNCHANGED <> + +\* Writer acquires lock +WriterLock == + /\ wpc = "lock" + /\ version % 2 = 0 \* must be unlocked + /\ version' = version + 1 \* odd = locked + /\ wpc' = "write_slot" + /\ UNCHANGED <> + +\* Writer stores slot value +WriterWriteSlot == + /\ wpc = "write_slot" + /\ slot' = wval + /\ wpc' = "write_bitmask" + /\ UNCHANGED <> + +\* Writer stores bitmask +WriterWriteBitmask == + /\ wpc = "write_bitmask" + /\ bitmask' = wbm + /\ wpc' = "unlock" + /\ UNCHANGED <> + +\* Writer releases lock +WriterUnlock == + /\ wpc = "unlock" + /\ version' = version + 1 \* even = unlocked + /\ wpc' = "idle" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +\* READER ACTIONS + +\* Reader starts: capture version +ReaderStart == + /\ rpc = "idle" + /\ rver' = version + /\ rpc' = "read_slot" + /\ UNCHANGED <> + +\* Reader reads slot +ReaderReadSlot == + /\ rpc = "read_slot" + /\ rslot' = slot + /\ rpc' = "read_bitmask" + /\ UNCHANGED <> + +\* Reader reads bitmask +ReaderReadBitmask == + /\ rpc = "read_bitmask" + /\ rbitmask' = bitmask + /\ rpc' = "validate" + /\ UNCHANGED <> + +\* Reader validates: version must be even AND unchanged +ReaderValidateOK == + /\ rpc = "validate" + /\ version = rver + /\ version % 2 = 0 + /\ rpc' = "interpret" + /\ UNCHANGED <> + +\* Reader validates: FAILS → discard and retry +ReaderValidateFail == + /\ rpc = "validate" + /\ (version # rver \/ version % 2 = 1) + /\ rpc' = "idle" + /\ UNCHANGED <> + +\* Reader interprets using CORRECT predicate +ReaderInterpret == + /\ rpc = "interpret" + /\ rpc' = "done" + /\ UNCHANGED <> + +\* Reader resets to idle +ReaderReset == + /\ rpc = "done" + /\ rpc' = "idle" + /\ UNCHANGED <> + +----------------------------------------------------------------------------- +\* NEXT STATE + +Step == + \/ WriterChoose + \/ WriterLock + \/ WriterWriteSlot + \/ WriterWriteBitmask + \/ WriterUnlock + \/ ReaderStart + \/ ReaderReadSlot + \/ ReaderReadBitmask + \/ ReaderValidateOK + \/ ReaderValidateFail + \/ ReaderInterpret + \/ ReaderReset + +Spec == Init /\ [][Step]_vars + +----------------------------------------------------------------------------- +\* INVARIANTS + +\* If reader successfully validated and is interpreting/done, +\* its local (rslot, rbitmask) is a consistent committed pair. +\* Specifically: if rbitmask=TRUE, the slot holds a value (not a pointer). +\* If rbitmask=FALSE and rslot#0, it's a pointer. +SnapshotConsistency == + rpc \in {"interpret", "done"} => + /\ (rbitmask = TRUE => rslot >= 0) \* value slots hold values (>=0) + /\ (rslot = -1 => rbitmask = FALSE) \* pointer slots have bitmask=FALSE + +\* Reader never dereferences a value as a pointer. +\* A dereference would happen if: rslot#0 AND rbitmask=FALSE (thinks it's a ptr) +\* but actually it's a value. With correct protocol, this can't happen. +NoDereferenceValue == + rpc \in {"interpret", "done"} => + ~(rslot > 0 /\ rbitmask = FALSE) + \* rslot>0 means nonzero value; if bitmask=FALSE reader would think it's a ptr + +\* Writer only modifies shared state when version is odd (locked) +WriterProtocol == + wpc \in {"write_slot", "write_bitmask"} => version % 2 = 1 + +\* Shared state consistency: when unlocked, slot and bitmask agree +UnlockedConsistency == + version % 2 = 0 => + /\ (bitmask = TRUE => slot >= 0) + /\ (slot = -1 => bitmask = FALSE) + +============================================================================= diff --git a/spec/tla/iterator-model-plan.md b/spec/tla/iterator-model-plan.md new file mode 100644 index 00000000..7026940f --- /dev/null +++ b/spec/tla/iterator-model-plan.md @@ -0,0 +1,123 @@ +# TLA+ Iterator Verification Model — Plan + +**Epic:** S-e80a92f0 (TLA+ Iterator Verification Model) +**Parent:** S-19f88e0e (E4: TLA+ formal verification) + +## Completed Phases + +### Phase 0: Base Forward Scan (T-d693d16a) ✅ + +- `OLCIterator.tla` — parametric `ConcurrencyEnabled` (db vs olc_db) +- Forward scan with seek-restart on version check failure +- Properties: OrderPreservation, NoRepeat, Completeness +- 96K states (OLC mode), 14 states (sequential) + +### Phase 1: Structural Remove + Havoc (T-78f6239d) ✅ + +- `OLCIteratorRemove.tla` — writer removes L2, collapses inode A +- Havoc model: stale read through obsolete node returns any leaf +- Correct code: 299 states, all properties pass +- Bug injection catches all three classes: + - `skip_backtrack` → Completeness violated (7 states) + - `restart_from_beginning` → NoRepeat violated (12 states) + - `skip_check` + havoc → OrderPreservation violated (6 states) +- Canary (L2AlwaysVisited) proves structural interleaving + +## Remaining Phases (Revised) + +### Phase 3: VIS TOCTOU (HIGH priority) — NEXT + +**Problem:** Packed leaves (value-in-slot) have no version lock. The parent +inode's version protects them. A TOCTOU window exists between check1 (before +`is_value_in_slot`) and check2 (after `get_child`). If check2 is missing, +a concurrent writer can mutate the slot mid-read. + +**Geometry:** Single inode P with 3 slots: +- Slot 1: regular leaf L1 +- Slot 2: VIS value V2 (mutable — writer can convert to regular child L2') +- Slot 3: regular leaf L3 + +**Iterator state machine:** +``` +start → snap_ver → at_L1 → check1 → read_slot2 → check2 → deliver → at_L3 → done + ↓ (fail) + restart +``` + +**Writer:** Lock P → mutate slot2 (VIS↔regular, value changes) → unlock P + +**Properties:** +- `NoGarbage`: delivered slot2 value ∈ {"V2", "L2prime"} +- `OrderPreservation`: delivered values in slot order +- `VISConsistency`: value delivered matches actual slot state at time of successful check + +**Bug injection:** `skip_check2` — havoc on stale read → `NoGarbage` violated + +**Expected:** ~500–2000 states. <1s. + +**Files:** `OLCIteratorVIS.tla`, `OLCIteratorVIS.cfg`, `OLCIteratorVIS_Bug.cfg` + +### Phase 5: Root Pointer Mutation + Emptying (MEDIUM priority) + +**Problem:** Root pointer can change (tree grows/shrinks). Iterator takes +`root_pointer_lock`, loads root, then takes node lock. If root changes between +load and node lock, the iterator follows a stale root. Also: tree can become +empty (root→null) during active scan. + +**Geometry:** Root pointer variable (mutable). Tree starts with Root→[L1, L2]. +Writer can: delete all keys (root→null), or replace root (root→NewRoot). + +**Properties:** +- `SafeTermination`: if tree empties, iterator reaches done (not crash) +- `NoStaleRoot`: iterator never descends into a freed root node + +**Expected:** ~1000–5000 states. + +### Phase 2: Structural Insert (LOW priority — subsumed by havoc) + +The havoc model already proves skip_check causes violations for any stale +read. Phase 2 would add a concrete insert scenario (node split, child +migration) but doesn't catch new bug classes. Value is in proving the +correct code's SeekPath handles post-insert topology. + +**Demoted.** Do only if a specific insert-related bug is suspected. + +### Phase 6: Two Concurrent Writers (LOW priority) + +Two writers don't interact with the iterator differently than one — the +iterator only sees version changes. Two writers interacting with each other +is covered by existing OLC chain cut models (Stages 5-10 in the suite). + +**Demoted.** Do only if multi-writer iterator bugs are suspected. + +### Phase 4: Reverse Scan — DROPPED + +Forward and reverse scan are structurally symmetric (`next→prior`, +`left_most→right_most`). If the forward model verifies the backtrack pattern, +the reverse direction holds by symmetry. Bugs in reverse-only would be +implementation typos — not catchable by TLA+. + +## Design Decisions + +1. **Havoc for stale reads** — non-deterministic value on unchecked stale read. + Sound (overapproximation), catches all ordering violations, no need to model + specific memory reuse patterns. + +2. **Decomposed verification** — Phase 0-1 proves traversal algorithm correct. + Phase 3 proves VIS access protocol correct. Compose for full correctness. + +3. **Single parameterized spec** — `ConcurrencyEnabled` flag covers both db + (sequential) and olc_db (concurrent) in one file. + +4. **Bug injection validation** — every spec includes a buggy config that must + fail. If the buggy config passes, the model is too weak. + +## Task Mapping + +| Phase | Task | Priority | Status | +|-------|------|----------|--------| +| 0 | T-d693d16a | — | done | +| 1 | T-78f6239d | — | done | +| 3 | T-61829475 | high | done | +| 5 | T-1d41fb6a | medium | done | +| — | T-ef029958 | medium | done | diff --git a/spec/tla/run-all-stages.sh b/spec/tla/run-all-stages.sh new file mode 100755 index 00000000..35ec2c17 --- /dev/null +++ b/spec/tla/run-all-stages.sh @@ -0,0 +1,52 @@ +#!/bin/bash +# Run all TLA+ model checking stages sequentially. +# Resource limits: 4GB heap, 4 workers, 5min timeout per stage. +set -e +cd "$(dirname "$0")" + +RED='\033[0;31m'; GREEN='\033[0;32m'; NC='\033[0m' +FAIL=0 + +run_stage() { + local name="$1" tla="$2" cfg="$3" + printf " %-50s " "$name" + rm -rf /tmp/tlc-run + local output + output=$(timeout 300 java -Xmx4g -XX:+UseParallelGC \ + -cp ~/tools/tla/tla2tools.jar tlc2.TLC \ + "$tla" -config "$cfg" -workers 4 \ + -metadir /tmp/tlc-run -noGenerateSpecTE 2>&1) + local rc=$? + rm -rf /tmp/tlc-run + if echo "$output" | grep -q "No error has been found"; then + local states + states=$(echo "$output" | grep "distinct states found" | grep -oP "\\d+ distinct" | tail -1) + echo -e "${GREEN}PASS${NC} ($states)" + else + echo -e "${RED}FAIL${NC}" + echo "$output" | grep -A5 "Error:" | head -10 + FAIL=1 + fi +} + +echo "=== TLA+ OLC ART Verification Suite ===" +echo +run_stage "Stage 1: Inode256VIS (sequential scan)" Inode256VIS.tla Inode256VIS.cfg +run_stage "Stage 2: OLCSlot (single-slot protocol)" OLCSlot.tla OLCSlot.cfg +run_stage "Stage 3: OLCInsert (two writers race)" OLCInsert.tla OLCInsert.cfg +run_stage "Stage 4: OLCChainMembership (revalidation)" OLCChainMembership.tla OLCChainMembership.cfg +run_stage "Stage 5: OLCChainCut (Cases A/B/C)" OLCChainCut.tla OLCChainCut.cfg +run_stage "Stage 6: OLCIterRemove (obsolescence)" OLCIterRemove.tla OLCIterRemove.cfg +run_stage "Stage 7: OLCInsertChainVIS (transient VIS)" OLCInsertChainVIS.tla OLCInsertChainVIS.cfg +run_stage "Stage 8: OLCDoubleCut (two removes)" OLCDoubleCut.tla OLCDoubleCut.cfg +run_stage "Stage 9: OLCChainMultiLevel (multi-level chain)" OLCChainMultiLevel.tla OLCChainMultiLevel.cfg +run_stage "Stage 10: OLCChainCutFull (root/shrink/cascade)" OLCChainCutFull.tla OLCChainCutFull.cfg +run_stage "Stage 11: OLCKeyViewChain (VIS + shared prefix)" OLCKeyViewChain.tla OLCKeyViewChain.cfg +run_stage "Stage 12: ARTTreeMaintenance (sequential tree)" ARTTreeMaintenance.tla ARTTreeMaintenance.cfg +echo +if [ $FAIL -eq 0 ]; then + echo -e "${GREEN}All stages passed!${NC}" +else + echo -e "${RED}Some stages failed.${NC}" + exit 1 +fi diff --git a/spec/tla/run-iterator-validation.sh b/spec/tla/run-iterator-validation.sh new file mode 100755 index 00000000..90a9a6eb --- /dev/null +++ b/spec/tla/run-iterator-validation.sh @@ -0,0 +1,86 @@ +#!/bin/bash +# Run all TLA+ iterator model specs and verify expected results. +# Each spec has: correct config (must PASS), bug config (must FAIL), canary config (must FAIL). +cd "$(dirname "$0")" + +RED='\033[0;31m'; GREEN='\033[0;32m'; YELLOW='\033[0;33m'; NC='\033[0m' +PASS=0; FAIL=0; ERRORS=0 + +run_check() { + local desc="$1" tla="$2" cfg="$3" expect="$4" + printf " %-60s " "$desc" + rm -rf /tmp/tlc-iter-val + local output + output=$(timeout 60 java -Xmx4g -XX:+UseParallelGC \ + -cp ~/tools/tla/tla2tools.jar tlc2.TLC \ + "$tla" -config "$cfg" -workers 4 \ + -metadir /tmp/tlc-iter-val -noGenerateSpecTE 2>&1) || true + rm -rf /tmp/tlc-iter-val + local found_error=false + if echo "$output" | grep -q "is violated\|Error:.*Invariant\|Error:.*Property"; then + found_error=true + fi + + if [ "$expect" = "pass" ]; then + if [ "$found_error" = "false" ] && echo "$output" | grep -q "No error has been found"; then + local states + states=$(echo "$output" | grep "distinct states found" | grep -oP "\d+ distinct" | tail -1) + echo -e "${GREEN}PASS${NC} ($states)" + PASS=$((PASS + 1)) + else + echo -e "${RED}UNEXPECTED FAIL${NC}" + echo "$output" | grep -E "Error:|violated" | head -3 + ERRORS=$((ERRORS + 1)) + fi + elif [ "$expect" = "fail" ]; then + if [ "$found_error" = "true" ]; then + local violated + violated=$(echo "$output" | grep "is violated" | sed 's/.*Invariant //' | sed 's/ is.*//') + echo -e "${GREEN}CAUGHT${NC} ($violated)" + PASS=$((PASS + 1)) + else + echo -e "${RED}MISSED — should have failed${NC}" + ERRORS=$((ERRORS + 1)) + fi + fi +} + +echo "=== TLA+ Iterator Model Validation Suite ===" +echo + +echo -e "${YELLOW}Phase 0: Base Forward Scan (OLCIterator)${NC}" +run_check "Sequential (db) — correct" OLCIterator.tla OLCIterator_Seq.cfg pass +run_check "OLC (olc_db) — correct" OLCIterator.tla OLCIterator_OLC.cfg pass + +echo +echo -e "${YELLOW}Phase 0: Bug Injection (OLCIterator_Bug850)${NC}" +run_check "skip_backtrack — catches Completeness" OLCIterator_Bug850.tla OLCIterator_Bug850_Backtrack.cfg fail +run_check "restart_from_beginning — catches NoRepeat" OLCIterator_Bug850.tla OLCIterator_Bug850_NoSeek.cfg fail + +echo +echo -e "${YELLOW}Phase 1: Structural Remove (OLCIteratorRemove)${NC}" +run_check "Correct code — all invariants" OLCIteratorRemove.tla OLCIteratorRemove_OLC.cfg pass +run_check "Canary — L2AlwaysVisited fails" OLCIteratorRemove.tla OLCIteratorRemove_Canary.cfg fail +run_check "skip_check + havoc — OrderPreservation" OLCIteratorRemove.tla OLCIteratorRemove_SkipCheck.cfg fail + +echo +echo -e "${YELLOW}Phase 3: VIS TOCTOU (OLCIteratorVIS)${NC}" +run_check "Correct code — all invariants" OLCIteratorVIS.tla OLCIteratorVIS.cfg pass +run_check "Canary — SlotNeverMutated fails" OLCIteratorVIS.tla OLCIteratorVIS_Canary.cfg fail +run_check "skip_check2 — NoGarbage violated" OLCIteratorVIS.tla OLCIteratorVIS_Bug.cfg fail + +echo +echo -e "${YELLOW}Phase 5: Root Pointer (OLCIteratorRoot)${NC}" +run_check "Correct code — all invariants" OLCIteratorRoot.tla OLCIteratorRoot.cfg pass +run_check "Canary — RootNeverNull fails" OLCIteratorRoot.tla OLCIteratorRoot_Canary.cfg fail +run_check "skip_rp_check — NoActOnInvalid" OLCIteratorRoot.tla OLCIteratorRoot_Bug.cfg fail + +echo +echo "────────────────────────────────────────────────────────" +echo -e "Results: ${GREEN}$PASS passed${NC}, ${RED}$ERRORS errors${NC}" +if [ $ERRORS -gt 0 ]; then + echo -e "${RED}VALIDATION FAILED${NC}" + exit 1 +else + echo -e "${GREEN}All checks passed!${NC}" +fi diff --git a/spec/tla/staged-model-plan.md b/spec/tla/staged-model-plan.md new file mode 100644 index 00000000..dfa124d5 --- /dev/null +++ b/spec/tla/staged-model-plan.md @@ -0,0 +1,320 @@ +# TLA+ Staged Model Plan: OLC ART Tree Maintenance + +## Goal + +High confidence in the correctness of the unodb OLC ART tree maintenance +algorithm under concurrent insert, remove, and scan operations. Specifically: + +1. No lost updates (insert/remove linearizable) +2. No use-after-free (QSBR + version obsolescence) +3. No value-as-pointer dereference (VIS bitmask correctness) +4. No missed or phantom entries in scans (iterator consistency) +5. Chain cut maintains well-formedness invariant +6. No deadlock (lock ordering is always bottom-up or parent→child) + +## Resource Constraints (HARD LIMITS) + +| Resource | Limit | +|----------|-------| +| JVM heap | 4 GB (`-Xmx4g`) | +| Disk (metadir) | 10 GB max | +| Workers | 4 (`-workers 4`) | +| Wall time | 5 min per stage | +| Cleanup | `rm -rf /tmp/tlc-run` after EVERY run | + +**Invocation template:** +```bash +cd .unodb-work/tla && \ + java -Xmx4g -XX:+UseParallelGC \ + -cp ~/tools/tla/tla2tools.jar tlc2.TLC \ + MODULE.tla -config CONFIG.cfg \ + -workers 4 -metadir /tmp/tlc-run \ + -noGenerateSpecTE 2>&1; \ + rm -rf /tmp/tlc-run +``` + +--- + +## Critical Interleavings Identified + +From the research, these are the hazardous concurrent scenarios: + +### H1: Insert × Scan (VIS slot interpretation) +- Writer inserts value=0 into inode256 slot (pack(0)=NULL, sets bitmask) +- Reader scans slots using `children[i] != nullptr` (misses the entry) +- **Property violated:** scan completeness + +### H2: Insert × Remove (chain membership) +- Remove's downward pass reads I4 with count=1 (chain candidate) +- Concurrent insert adds a second child to that I4 +- Remove's upward locking phase revalidates — must detect count change +- **Property violated:** chain membership precondition correctness + +### H3: Remove × Scan (node obsolescence) +- Iterator holds cached version for a node +- Remove obsoletes that node (unlock_and_obsolete) +- Iterator tries to rehydrate — must detect obsolescence and restart +- **Property violated:** iterator safety (use-after-free) + +### H4: Remove × Remove (chain cut race) +- Two removes target keys in the same chain +- Both identify overlapping chain segments +- Upward locking must serialize — second remove sees version change +- **Property violated:** well-formedness (double-cut) + +### H5: Insert × Insert (node growth race) +- Two inserts target the same full node +- Both pre-allocate larger nodes +- Only one succeeds at upgrade; other restarts +- **Property violated:** lost update + +### H6: Insert chain × Remove chain (VIS bitmask race) +- Insert does: add_to_nonfull(pack_value) → set_value_bit → overwrite with chain_ptr → clear_value_bit +- Concurrent scan reads between set_value_bit and clear_value_bit +- OLC version must cover the entire sequence +- **Property violated:** transient inconsistency visible to reader + +### H7: Remove shrink × Scan descent +- Remove shrinks I48→I16, replaces pointer in grandparent +- Scanner descending through grandparent reads old pointer, descends into obsoleted I48 +- Scanner must detect version change on grandparent before acting +- **Property violated:** stale pointer dereference + +--- + +## Staged Model Design + +### Abstraction Principles + +1. **Model the protocol, not the data structure.** We don't need to model + actual key bytes or prefix compression. We model: nodes with slots, + version counters, and the lock protocol. + +2. **One hazard per stage.** Each stage targets one or two specific + interleavings. This keeps state space small and failures diagnosable. + +3. **Minimal domain.** Use the smallest constants that exercise the hazard: + typically 1-2 nodes, 2-3 slots, 1-2 values. + +4. **Bound version counters.** Version is modular — only even/odd and + same/different matter. Cap at 6 (3 full cycles). + +5. **Bound process counts.** 1 writer + 1 reader per stage (except H4/H5 + which need 2 writers). + +--- + +### Stage 1: VIS Slot Interpretation (Sequential) +**File:** `Inode256VIS.tla` — DONE ✓ +**Hazard:** H1 (foundation) +**What:** Single inode256, insert/remove values and pointers, verify scan predicates +**Domain:** N=4 slots, Values={0,1,2}, Pointers={-1,-2,-3,-4} +**Result:** 4,096 states, <1s. Correct predicate verified, buggy predicate violated. + +--- + +### Stage 2: OLC Single-Slot Protocol +**File:** `OLCSlot.tla` +**Hazard:** H1 + H6 (concurrent VIS modification) +**What:** 1 writer + 1 reader on a single slot. Writer modifies (slot, bitmask) +under version lock. Reader reads both, validates, interprets. +**Variables (7 scalars):** +- Shared: `slot`, `bitmask`, `version` +- Writer: `wpc` (idle|lock|write_slot|write_bitmask|unlock) +- Reader: `rpc` (idle|read_slot|read_bitmask|validate|interpret|done), `rslot`, `rbitmask` + +**Domain:** slot ∈ {-1, 0, 1}, version ∈ 0..6 +**State constraint:** `version <= 6` +**Expected:** ~5K states, <5s +**Properties:** +- `NoDereferenceValue`: reader in "done" never has value in deref set +- `SnapshotConsistency`: if validate passes, (rslot, rbitmask) is a committed pair +- `WriterProtocol`: shared state only modified when version is odd + +--- + +### Stage 3: OLC Lock Coupling (Insert Path) +**File:** `OLCInsert.tla` +**Hazard:** H5 (two inserts racing for same slot) +**What:** 2 writers + 1 node with N=3 slots. Each writer: read version → find +empty slot → upgrade → write. Tests that only one succeeds. +**Variables (~10):** +- Shared: `slots[1..3]`, `version`, `count` +- Writer1: `w1pc`, `w1_target` +- Writer2: `w2pc`, `w2_target` + +**Domain:** slots ∈ {0, 1} (empty/full), version ∈ 0..6 +**Expected:** ~50K states, <30s +**Properties:** +- `NoLostUpdate`: if both target same slot, exactly one succeeds +- `CountConsistency`: count always equals number of non-empty slots +- `MutualExclusion`: at most one writer holds write lock at a time + +--- + +### Stage 4: Chain Membership Under Concurrent Insert +**File:** `OLCChainMembership.tla` +**Hazard:** H2 (insert invalidates chain precondition) +**What:** 1 remover evaluating chain membership on an I4 node, 1 inserter +adding a child to that same I4. Models the revalidation pattern. +**Variables (~10):** +- Shared: `count` (1 or 2), `version` +- Remover: `rpc` (read_count|validate|upgrade|locked|done|restart), `r_cached_count`, `r_cached_ver` +- Inserter: `ipc` (idle|lock|insert|unlock) + +**Domain:** count ∈ {1, 2}, version ∈ 0..6 +**Expected:** ~2K states, <5s +**Properties:** +- `ChainSafety`: remover never proceeds with cut when count=2 +- `ProgressUnderContention`: remover eventually either cuts or restarts +- `NoFalseChain`: if remover locks and proceeds, count was 1 at lock time + +--- + +### Stage 5: Chain Cut with Concurrent Insert (Cases A/B/C) +**File:** `OLCChainCut.tla` +**Hazard:** H2 + H4 (cut_point_parent evaluation under mutation) +**What:** A 3-node chain (parent → chain_node → leaf). Remover does upward +locking + CPP evaluation. Inserter can add children to parent or chain_node. +**Variables (~14):** +- Shared: `parent_count`, `chain_count`, `parent_ver`, `chain_ver`, `parent_child` (points to chain or null) +- Remover: `rpc` (lock_chain|eval_cpp|cut|done|restart), `cut_level`, `holds_chain_lock` +- Inserter: `ipc`, `i_target` (parent or chain) + +**Domain:** counts ∈ {1,2,3}, version ∈ 0..6 +**Expected:** ~100K states, <60s +**Properties:** +- `WellFormedness`: after cut, no node has count < 1 (for I4 in key_view mode) +- `NoCutWithStaleView`: remover never cuts based on outdated count +- `CaseACorrect`: if parent has 2+ children including chain, cut proceeds +- `CaseBCorrect`: if parent became single-child, chain extends upward +- `CaseCCorrect`: if child pointer gone, remover restarts + +--- + +### Stage 6: Iterator × Concurrent Remove (Obsolescence) +**File:** `OLCIterRemove.tla` +**Hazard:** H3 + H7 (node obsolescence during scan) +**What:** 1 iterator descending/advancing, 1 remover that can obsolete a node. +Tests that iterator detects obsolescence and restarts. +**Variables (~12):** +- Shared: `nodes[1..2]` each with `{version, obsolete, child}` +- Iterator: `ipc`, `i_stack` (cached versions), `i_current` +- Remover: `rpc`, `r_target` + +**Domain:** 2 nodes, version ∈ 0..6 +**Expected:** ~50K states, <30s +**Properties:** +- `NoUseAfterObsolete`: iterator never acts on data from an obsoleted node +- `RestartOnObsolete`: if rehydrate finds obsolete, iterator restarts +- `ProgressAfterRestart`: iterator eventually re-seeks and advances + +--- + +### Stage 7: Insert Chain × Scan (VIS Transient State) +**File:** `OLCInsertChainVIS.tla` +**Hazard:** H6 (set_value_bit → overwrite → clear_value_bit sequence) +**What:** 1 writer performing the chain-insert protocol (4 steps under one +write lock), 1 reader scanning. Verifies reader never sees the transient +state where bitmask=TRUE but slot holds a chain pointer. +**Variables (~10):** +- Shared: `slot`, `bitmask`, `version` +- Writer: `wpc` (lock|set_bit|write_chain|clear_bit|unlock) +- Reader: `rpc`, `rslot`, `rbitmask`, `rver` + +**Domain:** slot ∈ {0, "chain_ptr", "packed_val"}, version ∈ 0..6 +**Expected:** ~3K states, <5s +**Properties:** +- `NoTransientVisible`: reader in "done" never sees (bitmask=TRUE, slot=chain_ptr) +- `ProtocolCovers`: all 4 writer steps are under one version lock + +--- + +### Stage 8: Remove × Remove (Double Cut Prevention) +**File:** `OLCDoubleCut.tla` +**Hazard:** H4 (two removes targeting same chain) +**What:** 2 removers, 1 chain of 2 nodes. Both try to lock the chain bottom-up. +Only one can succeed at upgrading; the other sees version change. +**Variables (~12):** +- Shared: `chain_ver`, `chain_obsolete`, `parent_ver`, `parent_child` +- Remover1: `r1pc`, `r1_holds_lock` +- Remover2: `r2pc`, `r2_holds_lock` + +**Domain:** version ∈ 0..8 (need more cycles for 2 writers) +**Expected:** ~20K states, <15s +**Properties:** +- `AtMostOneCut`: at most one remover reaches point-of-no-return +- `LoserRestarts`: the other remover detects conflict and restarts +- `NoDoubleFree`: a node is obsoleted at most once + +--- + +## Verification Matrix + +| Stage | Hazards | Slots | Procs | Est. States | Time | Key Property | +|-------|---------|-------|-------|-------------|------|--------------| +| 1 ✓ | H1 | 4 | 0 | 4K | <1s | Scan completeness | +| 2 | H1,H6 | 1 | 1W+1R | ~5K | <5s | No value-as-ptr | +| 3 | H5 | 3 | 2W | ~50K | <30s | No lost update | +| 4 | H2 | 1 | 1W+1R | ~2K | <5s | Chain membership | +| 5 | H2,H4 | — | 1W+1R | ~100K | <60s | Cut correctness | +| 6 | H3,H7 | — | 1W+1R | ~50K | <30s | No use-after-obsolete | +| 7 | H6 | 1 | 1W+1R | ~3K | <5s | No transient visible | +| 8 | H4 | — | 2W | ~20K | <15s | At-most-one cut | + +**Total estimated time:** <4 minutes for all 8 stages. + +--- + +## Success Criteria + +All 8 stages pass TLC with 0 errors. This gives us: +- **Insert correctness:** Stages 3, 7 (mutual exclusion, VIS protocol) +- **Remove correctness:** Stages 4, 5, 8 (chain membership, cut, double-cut) +- **Scan correctness:** Stages 1, 2, 6 (slot interpretation, OLC protocol, obsolescence) +- **Cross-operation:** Stages 4, 5, 6, 7 (insert×remove, remove×scan, insert×scan) + +After all stages pass, we implement the code fix with confidence that: +1. The bitmask-only predicate is correct (Stage 1) +2. OLC prevents partial observation (Stage 2) +3. The chain cut algorithm handles concurrent mutations (Stages 4, 5) +4. Iterators correctly detect and recover from concurrent changes (Stage 6) + +--- + +## File Organization + +``` +.unodb-work/tla/ +├── staged-model-plan.md # THIS FILE +├── Inode256VIS.tla # Stage 1 (DONE) +├── Inode256VIS.cfg +├── Inode256VIS_BugDemo.cfg +├── OLCSlot.tla # Stage 2 +├── OLCSlot.cfg +├── OLCInsert.tla # Stage 3 +├── OLCInsert.cfg +├── OLCChainMembership.tla # Stage 4 +├── OLCChainMembership.cfg +├── OLCChainCut.tla # Stage 5 +├── OLCChainCut.cfg +├── OLCIterRemove.tla # Stage 6 +├── OLCIterRemove.cfg +├── OLCInsertChainVIS.tla # Stage 7 +├── OLCInsertChainVIS.cfg +├── OLCDoubleCut.tla # Stage 8 +├── OLCDoubleCut.cfg +└── run-all-stages.sh # Orchestrator script +``` + +--- + +## Incremental Expansion + +After all stages pass at minimal domain, we can selectively expand: +- Stage 5: Add a second inserter (H2+H5 combined) — expect ~500K states +- Stage 6: Add 2 nodes → 3 nodes (deeper tree) — expect ~200K states +- Stage 3: Increase to N=4 slots — expect ~200K states + +Only expand if the base passes AND we have specific doubt about a larger case. +Never expand all stages simultaneously. diff --git a/spec/tla/tree-structure-model-design.md b/spec/tla/tree-structure-model-design.md new file mode 100644 index 00000000..7f30bdc7 --- /dev/null +++ b/spec/tla/tree-structure-model-design.md @@ -0,0 +1,193 @@ +# Stage 12: ART key_view Tree Structure Model — Design Parameters + +## Overview + +This document captures the design decisions for a TLA+ model of the ART (Adaptive Radix Tree) `key_view` algorithm. The model verifies structural invariants of insert and remove operations, focusing on chain nodes and the `try_collapse_i4` algorithm. + +This is Stage 12 in the unodb verification suite. Stages 2–11 cover concurrency; this stage verifies sequential correctness of tree structure maintenance. + +--- + +## Context + +The ART `key_view` algorithm stores variable-length keys in the inode path (prefix bytes + dispatch bytes). Each inode level consumes up to 7 prefix bytes + 1 dispatch byte = 8 bytes. Keys that share a prefix create a shared path; where they diverge, a branching node is created. + +**Chain nodes** are I4 inodes with exactly 1 child — they exist solely to encode key bytes in the path. The chain cut algorithm removes chains atomically when a leaf is deleted. + +**try_collapse_i4** merges a single-child I4 with its child when the combined prefix fits: + +``` +parent_prefix + 1 (dispatch) + child_prefix ≤ 7 +``` + +--- + +## Verification Goals + +| # | Invariant | Description | +|---|-----------|-------------| +| 1 | Well-formedness | No single-child I4 exists unless prefix overflow blocks collapse OR child is a keyless VIS entry | +| 2 | Key preservation | Every inserted key not yet removed is reachable from root | +| 3 | No orphans | Every node in the tree is reachable from root | +| 4 | Correct chain identification | Chain membership identifies the longest sequence of single-child I4s above a leaf | +| 5 | Correct collapse | `try_collapse_i4` fires exactly when prefix fits AND child is not keyless | + +--- + +## Abstraction Choices + +### Abstracted away (not modeled) + +- Concurrency (sequential model — covered by Stages 2–11) +- Actual byte values (use abstract key segments) +- Inode type transitions (I4→I16→I48→I256) — model only I4 for chains, generic "inode" for branching +- Memory allocation/deallocation + +### Must capture + +- Key length variety (keys of 1, 2, 3 segments; each segment = 8 bytes of real key) +- Prefix capacity (7 bytes per node = modeled as capacity of 1 abstract unit per node) +- Shared prefix divergence (two keys sharing 0, 1, or 2 segments then diverging) +- Chain depth (0, 1, 2 levels) +- Collapse decision (prefix fits vs overflow) +- VIS entries (value-in-slot: leaf value stored directly in parent's child slot) + +--- + +## State Space Design + +Target: **<5000 distinct states, <30s TLC runtime**. + +| Parameter | Choice | Rationale | +|-----------|--------|-----------| +| Keys | 5 abstract keys | Exercises all paths including prefix overflow | +| Key lengths | 1–5 segments | Exercises no-chain through multi-segment chains | +| Key alphabet | 2 symbols {1, 2} | Minimum for branching without explosion | +| Prefix capacity | 2 | Exercises both collapse-success (combined ≤ 2) and collapse-blocked (combined > 2) | +| Tree representation | `node_id → {prefix, children, is_vis}` | Minimal record per node | +| Operations | `Insert(key)`, `Remove(key)` non-deterministic | Full insert/remove interleaving | +| StateConstraint | nxt ≤ 8 (max 7 nodes) | Keeps state space at ~5000 | + +**Actual TLC results:** 5,035 distinct states, depth 14, 1 second. + +**Key set:** `{<<1>>, <<1,2>>, <<1,2,1>>, <<2,1>>, <<1,2,1,2,1>>}` +- `<<1>>`: length 1, VIS at branching node +- `<<1,2>>`: length 2, shares prefix with `<<1>>` +- `<<1,2,1>>`: length 3, extends `<<1,2>>` +- `<<2,1>>`: length 2, diverges at root from `<<1,...>>` +- `<<1,2,1,2,1>>`: length 5, creates prefix overflow scenario + +--- + +## Key Variety Dimensions + +Derived from test survey of the C++ implementation: + +| Dimension | Values modeled | Exercises | +|-----------|---------------|-----------| +| Key length | {1, 2, 3} segments | no-chain, 1-chain, 2-chain | +| Shared prefix | {0, 1, 2} segments | immediate diverge, partial share, deep share | +| Prefix capacity | 1 unit per node | collapse fits vs overflow | +| Chain depth | {0, 1, 2} | no-chain, single-chain, multi-chain | +| VIS vs leaf | both | collapse blocked by keyless child | +| Collapse decision | fits / overflow | `try_collapse_i4` success / failure | + +--- + +## Invariant Definitions + +``` +WellFormed == + ∀ node ∈ tree: + node.child_count = 1 => + \/ node.prefix_len + 1 + child.prefix_len > CAPACITY \* overflow + \/ child is VIS entry \* keyless, cannot promote + +KeyPreservation == + ∀ key ∈ inserted_keys \ removed_keys: + Reachable(root, key) + +NoOrphans == + ∀ node ∈ tree: + node = root \/ ∃ parent ∈ tree: node ∈ parent.children + +CorrectChainId == + ∀ leaf reachable from root: + chain_above(leaf) = longest sequence of single-child I4s ending at leaf + +CollapseCorrect == + After every remove that leaves a single-child I4: + IF prefix_fits ∧ child_is_not_keyless THEN collapse happened + ELSE single-child I4 persists +``` + +--- + +## Operations Modeled + +### Insert(key) + +1. Traverse tree following key segments +2. At divergence point: split existing node's prefix, create new branching node +3. Build chain for remaining key segments below divergence +4. Place leaf (or VIS entry if key is fully consumed at an existing node) + +### Remove(key) + +1. Find leaf/VIS entry +2. Identify chain above leaf (longest sequence of single-child I4s) +3. Cut chain: remove all chain nodes + leaf atomically +4. Update cut_point_parent (remove child entry) +5. If cut_point_parent becomes single-child I4: `try_collapse_i4` + +### try_collapse_i4(node) + +1. Check: node has exactly 1 child +2. Check: child is not a VIS/keyless entry +3. Check: `node.prefix_len + 1 + child.prefix_len ≤ CAPACITY` +4. If all pass: merge node into child (prepend prefix + dispatch to child's prefix) +5. Replace node with child in parent + +--- + +## Expected Algorithmic Paths Exercised + +With 3–4 keys of lengths {1, 2, 3}: + +| Path | Trigger | +|------|---------| +| Insert into empty tree | First key | +| Insert creating chain | Second key shares prefix | +| Insert splitting chain | Third key diverges mid-chain | +| Remove with no chain | Short key, direct child of branching node | +| Remove with chain cut | Long key, chain above leaf | +| Remove triggering collapse | cut_point_parent becomes single-child, prefix fits | +| Remove — collapse blocked (overflow) | Combined prefix > CAPACITY | +| Remove — collapse blocked (VIS child) | Child is keyless VIS entry | +| Insert/remove VIS entry | Key fully consumed at branching node | + +--- + +## Design Notes + +- **PrefixCapacity = 2**: Exercises both collapse-success (combined ≤ 2) and collapse-blocked (combined > 2). With capacity=1, collapse would almost never fire; with capacity=3+, overflow would be unreachable with short keys. +- **Root handling**: Root is excluded from WellFormed — a single-child root is valid (no parent to merge into). +- **VIS entries**: Modeled as `is_vis` flag on nodes. A node with `is_vis=TRUE` and children has 2+ "occupants" and is not a chain candidate. +- **Collapse during insert**: When a prefix split shortens a node's prefix, the node may become newly collapsible. The model performs collapse eagerly after every structural change. + +--- + +## Verified Coverage (from expert review) + +| Algorithmic Path | Exercised? | Example Scenario | +|-----------------|------------|-----------------| +| Prefix overflow persistence | ✓ | Insert <<1,2,1,2,1>> then <<1>> | +| Collapse after remove | ✓ | Insert <<1>>, <<1,2,1>>, <<1,2>>, Remove <<1,2>> | +| Collapse after insert (prefix split) | ✓ | Insert <<1,2,1>> then <<2,1>> | +| VIS + child coexistence | ✓ | Insert <<1,2>> then <<1,2,1>> | +| Key-as-prefix-of-another | ✓ | <<1>> and <<1,2>> in either order | +| Chain split (diverge mid-chain) | ✓ | Insert <<1,2,1,2,1>> then <<1>> | +| Collapse blocked by overflow | ✓ | Node with prefix=<<>> + child prefix=<<2,1>> = 3 > 2 | +| Multi-level CleanUp recursion | ⚠️ Not exercised | Collapse prevents prerequisite chains from forming | + +**Gap analysis**: Multi-level CleanUp is not reachable because collapse eagerly merges single-child non-VIS nodes, preventing the prerequisite chain structure. This is correct behavior — the same happens in the real algorithm. Multi-level chain cut under concurrency is covered by Stages 5, 9, and 10.