Lin2var relations fine-tuning - switching from array to map

[DrMichaelPetter]

This swaps out the basic datastructure in lin2var analysis from an array to a hashtable. Since we expect very sparse information kept in the relational part anyway, we expect a sizeable amount of runtime improvements vs. the conventional array implementation.

[michael-schwarz]

Already very curious how the performance is gonna be!

[sim642]

Depends on the benchmark results, but I'm wondering if maybe immutable Maps would be the better choice even. You get the same sparsity benefit, but Maps also can share unmodified subtrees while Hashtbls cannot (due to the mutability). Moreover, copy (which we do a lot) for a Map would essentially be identity as opposed to copying of Hashtbls. The only complication is that we sometimes want to exploit mutable _with operations on relational domains, which wouldn't be possible with Map. A generic lifting via ref (to a Map) like I already have in #1339 easily provides the necessary conversion.

[DrMichaelPetter]

Depends on the benchmark results, but I'm wondering if maybe immutable Maps would be the better choice even. You get the same sparsity benefit, but Maps also can share unmodified subtrees while Hashtbls cannot (due to the mutability). Moreover, copy (which we do a lot) for a Map would essentially be identity as opposed to copying of Hashtbls. The only complication is that we sometimes want to exploit mutable _with operations on relational domains, which wouldn't be possible with Map. A generic lifting via ref (to a Map) like I already have in #1339 easily provides the necessary conversion.

This sounds reasonable. Thank you for this in-depth insight into Ocaml data-structures. This is where my lack of experience in Ocaml shines through :disappointed:

[DrMichaelPetter]

So, I now have the results of the testrun with the correct hash and equal functions; finally, this eliminated the notorious "fixpoint not reached" errors. Performance wise, profiling points to the optimization of the copy function as Simmo has already suspected. So I will look into migrating to a version of immutable Maps + refs.

[DrMichaelPetter]

In the current version, I have switched to maps - this eliminated the copy overhead. Still, some work had to be put into dim_add, which during runtime created a full-blown array of size of the dimension of the state. It's replaced by some compromise between runtime and space now. Runtime benchmarks are pending, depending on the availability of our servers.