Split octagon autotuner to separate octagonAnalysis and octagonVars autotuners#1952
Split octagon autotuner to separate octagonAnalysis and octagonVars autotuners#1952karoliineh wants to merge 2 commits intomasterfrom
Conversation
karoliineh
added
cleanup
michael-schwarz
left a comment
michael-schwarz
left a comment
There was a problem hiding this comment.
We should start to document what these autotuners do somehow. Maybe we can have some way they are registered and a command line option to get the description of all autotuners like you can get one for the analyses?
We don't actually have the analysis descriptions available at runtime. They exist as module documentation in the API docs for now (which isn't too user-friendly but better than none at all). But documenting the autotuners would definitely be a good idea. A separate next step would be to split |
| @@ -1,4 +1,4 @@ | |||
| // SKIP PARAM: --enable ana.sv-comp.functions --enable ana.autotune.enabled --set ana.autotune.activated[+] octagon | |||
| // SKIP PARAM: --enable ana.sv-comp.functions --enable ana.autotune.enabled --set ana.autotune.activated[+] octagonVars | |||
There was a problem hiding this comment.
Why just octagonVars? I'd think that octagonAnalysis also needs to be activated.
And perhaps octagonVars isn't even necessary? Depends on what the test was added to test: the activation of the analysis or the selection of the variables.
| $ goblint --enable ana.autotune.enabled --set ana.autotune.activated[*] octagonVars 38-autotune-octagon-fun.c | ||
| [Info] Enabled octagon domain. |
There was a problem hiding this comment.
So octagonVars also enables octagonAnalysis autotuner implicitly?
I think for #1449 they should be independent.
| let activateOctagonAnalysis () = | ||
| set_string "ana.apron.domain" "octagon"; | ||
| set_auto "ana.activated[+]" "apron"; | ||
| set_bool "ana.apron.threshold_widening" true; | ||
| set_string "ana.apron.threshold_widening_constants" "comparisons"; | ||
| Logs.info "Enabled octagon domain." |
There was a problem hiding this comment.
This doesn't seem right without the costs thing. It will always enable octagons if octagonAnalysis autotuner is activated.
That's not much of an autotuner if it just unconditionally activates things which could be activated directly.
I think I wasn't aware of this dependency when I opened #1449. Maybe it's actually impossible to separate them then?
There was a problem hiding this comment.
So, what I did was to just implement the requirements from the issue:
split the autotuner into two:
- octagonAnalysis, which is just in charge of enabling the octagon analysis, but not choosing a subset of the variables.
- octagonVars, which is in charge of choosing the variables, i.e. disabling octagon analysis for all other variables (because that's what it's really doing, not enabling for additional variables).
where the main problem was that the option octagon:
implicitly means "disabling octagon analysis for all other variables, even if explicitly enabled by the user".
Due to the separation, the confusing behavior is gone as the option names now better reflect what they actually do.
However, it is true that I did not really consider that the autotuner should actually tune something with each option, which is not the case for octagonAnalysis now.
The reason I separated it the way I did is that the cost calculation depends on the number of selected variables. At first glance, this made it seem like the cost belonged purely to the variable selection step. Because of that, I overlooked the fact that the cost value is later used.
Looking at this again from the perspective of autotuning, I see two possible approaches:
- Base the cost on all program variables. The cost calculation for
octagonAnalysiscould consider all variables present in the program, but I am not sure if we can count these easily with some visitor. I am also not sure if the cost will then ever stay under some threshold that the analysis would even be considered (I haven't looked into how the cost is used). - Actually tune the activation of
octagonAnalysismeaningfully Instead of simply enabling it through a portfolio configuration, the tuner could decide whether activating it makes sense based not only on the number of variables but also on their structure, e.g., the presence of patterns that would require relational analyses likey = x + 1;.
It definitely is not impossible to separate them cleanly. The question is whether this change is already worthwhile because it makes the options less confusing, even though one of them does not actually tune anything yet, or whether we should wait and introduce that separation only once we also improve the autotuning of enabling octagon in some way.
3 participants
Solves #1449