alt-romes / hegg

Fast equality saturation in Haskell
https://hackage.haskell.org/package/hegg
BSD 3-Clause "New" or "Revised" License
75 stars 8 forks source link

Fix de-duplication and use list for worklist #13

Closed alt-romes closed 2 years ago

alt-romes commented 2 years ago

Closes #2

We were previously using a Map for the worklist, and the deduplication step wasn't being done correctly. This came to be from historic changes to the representations that ultimately led to deduplication being overlooked.

The performance significantly improves with these changes.

I think the classes parents representation was also improved. We use SList instead of just list because we need a O(1) size function

alt-romes commented 2 years ago

@aspiwack if you could add a drive-by comment on whether everything looks alright/this is what you had in mind/performance insights on this.

Anyway, it's already improved the performance significantly. We can run all individual unit tests under 0.10 seconds now, while before a couple took ~0.15 seconds

Thanks!

aspiwack commented 2 years ago

Something else that could be experimented is to force the entire list (rather than just the head) after a nub. It may be better, or it may be worse.

alt-romes commented 2 years ago
  1. I added a commit that removes the cost centers which boosts performance as well

Something else that could be experimented is to force the entire list (rather than just the head) after a nub. It may be better, or it may be worse.

After experimenting I would say it makes no difference other than then having (..., NFData1 l) => Language l which is undesirable.

Are we going to append this list to the worklist when we merge this class? Then maybe we would like a data structure that appends better? On the other hand, we do have to traverse the whole structure anyway for deduping, so probably it doesn't matter. This requires a finer understanding of the data structure than I have 🙂 .

I tried both Seq and Set. Honestly, the benchmarks aren't fine grained enough to notice the difference. They kind of all perform the same, with the simple SizedList performing just so very slightly better.

They suffer from different things and perhaps it's too late in the night for me to figure it out.

However, having the main worklist be anything other than a list resulted in performance decrease. Which meant the O(log n) concat structures had to be converted to a list before appending to the worklist. I did, however, use the same representation for the analysis worklist as for the class parents -- and the concat load seems to be heavier for the analysis worklist. But in the end I don't think it makes a difference, and the places where the O(n) toList showed up scared me a bit.

Perhaps we can try this again later.

Overall, this patch makes performance much better! It also makes everything a bit simpler by having worklists be lists and e-class parents being just lists with a cached size (which makes their toListO(1)).

@aspiwack I think we can merge this now and come to performance later again. I'd rather go back to profiling to figure this out later correctly

aspiwack commented 2 years ago

@aspiwack I think we can merge this now and come to performance later again. I'd rather go back to profiling to figure this out later correctly

Yes.