Skip to content

Commit 42d0efe

Browse files
committed
Optimize fixpoint batch handling with single BFS expansion
Instead of calling apply_init_delta (which runs BFS) for each entry in a batch, collect all new roots first and run a single BFS expansion. Before: Batch of N roots → N separate BFS operations After: Batch of N roots → 1 BFS with N-element frontier This matches how the fixpoint initialization already works. Note: The main CMT processing overhead (~2.5s) comes from other combinators (flatMaps, joins), not the fixpoint. The fixpoint only receives 13 batch updates vs 600K+ individual deltas before batching.
1 parent ed29f4d commit 42d0efe

File tree

1 file changed

+26
-9
lines changed

1 file changed

+26
-9
lines changed

analysis/reactive/src/Reactive.ml

Lines changed: 26 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1081,25 +1081,42 @@ let fixpoint ~(init : ('k, unit) t) ~(edges : ('k, 'k list) t) () : ('k, unit) t
10811081
my_stats.updates_received <- my_stats.updates_received + 1;
10821082
match delta with
10831083
| Batch entries ->
1084-
(* Process all init entries as a batch *)
1085-
let all_added = ref [] in
1086-
let all_removed = ref [] in
1084+
(* OPTIMIZED: Process all entries with single BFS instead of per-entry BFS *)
1085+
(* Phase 1: Separate adds and removes, collect new roots *)
1086+
let new_roots = ref [] in
1087+
let removes = ref [] in
10871088
entries
10881089
|> List.iter (fun (k, v_opt) ->
1089-
let d =
1090-
match v_opt with
1091-
| Some () -> Set (k, ())
1092-
| None -> Remove k
1090+
match v_opt with
1091+
| Some () ->
1092+
if not (Hashtbl.mem state.base k) then begin
1093+
Hashtbl.replace state.base k ();
1094+
new_roots := k :: !new_roots
1095+
end
1096+
| None -> removes := k :: !removes);
1097+
1098+
(* Phase 2: Single BFS expansion from all new roots *)
1099+
let added_from_expansion =
1100+
if !new_roots <> [] then Fixpoint.expand state ~frontier:!new_roots
1101+
else []
1102+
in
1103+
1104+
(* Phase 3: Handle removes (may trigger contraction) *)
1105+
let all_added = ref added_from_expansion in
1106+
let all_removed = ref [] in
1107+
!removes
1108+
|> List.iter (fun k ->
1109+
let added, removed =
1110+
Fixpoint.apply_init_delta state (Remove k)
10931111
in
1094-
let added, removed = Fixpoint.apply_init_delta state d in
10951112
all_added := added @ !all_added;
10961113
all_removed := removed @ !all_removed);
1114+
10971115
(* Deduplicate and emit as batch *)
10981116
let added_set = Hashtbl.create (List.length !all_added) in
10991117
List.iter (fun k -> Hashtbl.replace added_set k ()) !all_added;
11001118
let removed_set = Hashtbl.create (List.length !all_removed) in
11011119
List.iter (fun k -> Hashtbl.replace removed_set k ()) !all_removed;
1102-
(* Net changes: added if in added_set but not removed_set, etc. *)
11031120
let net_added =
11041121
Hashtbl.fold
11051122
(fun k () acc -> if Hashtbl.mem removed_set k then acc else k :: acc)

0 commit comments

Comments
 (0)