-
Notifications
You must be signed in to change notification settings - Fork 83
Avoid TC(x, z) :- TC(x, y), TC(y, z) when computing transitive closures #176
Description
When computing a transitive closure (TC) for a graph G using a semi-naive datalog solver, it is more efficient to use the first rule than the second.
TC(x, z) :- TC(x, y), G(y, z)
% -vs-
TC(x, z) :- TC(x, y), TC(y, z)The solver must join any newly created facts on either side of the join with the stable facts of the other side. Assuming stratification, G will remain constant while TC is computed (no newly created facts) and, by definition, will have fewer facts than TC.
The inefficient second pattern appears twice in polonius, albeit in more complex forms. First, in the naive variant:
polonius/polonius-engine/src/output/naive.rs
Lines 136 to 145 in 741e609
| // Rule 2: compute the subset transitive closure, at a given point. | |
| // | |
| // subset(Origin1, Origin3, Point) :- | |
| // subset(Origin1, Origin2, Point), | |
| // subset(Origin2, Origin3, Point). | |
| subset.from_join( | |
| &subset_o2p, | |
| &subset_o1p, | |
| |&(_origin2, point), &origin1, &origin3| (origin1, origin3, point), | |
| ); |
This can be fixed by computing an intermediate relation, which I'll call subset_base_cfg, that propagates subset_base facts across the control-flow graph. We can then compute the transitive closure of subset_base_cfg at each point to obtain the original subset relation, like so:
subset_base_cfg(Origin1, Origin2, Point) :-
subset_base(Origin1, Origin2, Point)
subset_base_cfg(Origin1, Origin2, Point2) :-
subset_base_cfg(Origin1, Origin2, Point1),
cfg_edge(Point1, Point2),
origin_live_on_entry(Origin1, Point2),
origin_live_on_entry(Origin2, Point2).
subset(Origin1, Origin3, Point) :-
subset(Origin1, Origin2, Point),
subset_base_cfg(Origin2, Origin3, Point).AFAICT, the optimized variant is doing something similar, although subset passes through several intermediate relations, so it's hard to tell. Speed is also probably less important there, because the subset relation is aggressively filtered. This may have changed somewhat now that we compute subset_errors, however.