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

tweak GC #5982

Merged
merged 1 commit into from
Apr 15, 2022
Merged

tweak GC #5982

merged 1 commit into from
Apr 15, 2022

Conversation

c-cube
Copy link
Contributor

@c-cube c-cube commented Apr 15, 2022

Related to #5970. This improves times for us (backported on an older version); I haven't checked the memory usage yet. @giltho would you be interested in trying this branch?

@@ -294,7 +294,8 @@ static struct custom_operations Z3_ast_plus_custom_ops = {
Z3_ast_compare_ext
};

MK_CTX_OF(ast, 16) // let's say 16 bytes per ast
// FUDGE
MK_CTX_OF(ast, 8) // let's say 16 bytes per ast
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"let's say?" 8 is the new 16?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ah, need to remove the comment :). These are size estimations, that the GC uses to guestimate how heavy a foreign value is. Seems like giving OCaml smaller estimations makes it faster here, it might be that it started garbage collecting like crazy with the previous change.

MK_PLUS_OBJ(ast_vector, 128)
MK_PLUS_OBJ(fixedpoint, 20 * 1000 * 1000)
MK_PLUS_OBJ(optimize, 20 * 1000 * 1000)
// FUDGE
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

vanilla size?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

it's something I stole from Jasmin B, it's just to indicate a potential tweaking point for heuristics :).

@giltho
Copy link
Contributor

giltho commented Apr 15, 2022

Hi! Thank you very much for looking into this!
With these changes, it looks like now times have gone up only 10%, instead of 330% for our set of benchmarks. That's definitely an acceptable time regression, especially if the gains in terms of memory are interesting

@NikolajBjorner NikolajBjorner marked this pull request as ready for review April 15, 2022 18:08
@NikolajBjorner NikolajBjorner merged commit 11d992a into Z3Prover:master Apr 15, 2022
@c-cube c-cube deleted the ml-gc-5970 branch April 15, 2022 18:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants