Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Lin2var relations fine-tuning - switching from array to map #1412

Merged
merged 73 commits into from
May 15, 2024

Conversation

DrMichaelPetter
Copy link
Collaborator

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
Copy link
Member

Already very curious how the performance is gonna be!

@sim642
Copy link
Member

sim642 commented Apr 17, 2024

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
Copy link
Collaborator Author

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 😞

src/cdomains/apron/sharedFunctions.apron.ml Outdated Show resolved Hide resolved
@sim642 sim642 added this to the v2.4.0 milestone May 15, 2024
@sim642 sim642 added the relational Relational analyses (Apron, affeq, lin2var) label May 15, 2024
@DrMichaelPetter DrMichaelPetter merged commit 91dce01 into master May 15, 2024
21 checks passed
@DrMichaelPetter DrMichaelPetter deleted the lin2var-hashtables branch May 15, 2024 08:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
performance time, memory relational Relational analyses (Apron, affeq, lin2var)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants