search

sybila / biodivine-lib-bdd

A small library for BDD manipulation in Rust. Part of the BioDivine toolset.
MIT License
20 stars 4 forks source link

Hash function #17

Closed lengyijun closed 3 years ago

lengyijun commented 3 years ago

In https://www.cmi.ac.in/~madhavan/courses/verification-2011/andersen-bdd.pdf Chap 5, use pair and a prime as hash function. If this approach works faster than fxhash?

daemontus commented 3 years ago

That is a good suggestion. I made a quick comparison of the "raw performance" of the two approaches here (run cargo bench to see the results).

On my i5-6500, they are both essentially equal:

fx hash                 time:   [294.96 ps 296.39 ps 298.21 ps]                    
andersen hash           time:   [294.32 ps 294.94 ps 295.59 ps]

However, note that this is without the remainder operation, which would need to be performed twice for the "andersen hash" (or we'd need a hash table which is always prime-sized, which rust tables aren't). Another important note is that this does not account for the price of collisions. I am not sure which hash will be more resilient to those, but from what I've seen, it is hard to come up with anything more robust than fxhash on non-adversarial data.

With sufficiently large BDDs, the limiting performance factor usually becomes the random memory access as the hash table will not fit into the L3 cache. So for these situations, anything that can compute the hash fast enough will be bottlenecked by RAM latency anyway :)

However, I'd be happy to accept a pull request if it turns out this hash is indeed significantly faster in practice.

lengyijun commented 3 years ago

Thanks for your reply. I have no more idea about it. You can close this pr if necessary. I will post some other ideas about this repo later.

daemontus commented 3 years ago

Cool! Ideas are always welcome. Also, if you need some API which we currently don't have, feel free to submit an issue for that. We are mostly adding features as we need them, so if you have a use case for something that we haven't thought of already, we'd be happy to add it.