feat: support (get-info :all-statistics) and refactoring Profiling module

[Stevendeo]

This PR was initially open to add the get-statistics option. Some bugs and (IMHO) bad design choices in the Timer and Profiling module changed the purpose of this PR to not only add the get-statistics feature, but also to rework it.

[bclement-ocp]

I will take a look at the rest of the changes later, but this patch moves the timers from a global constant in the binary (bin/common/signals_profiling.ml) to a global constant in the library (lib/structures/profiling.ml), which is the opposite of the direction we should be going for (see also #377). Please revert that part of the change.

[Halbaroth]

We could add an option to activate profiling: (set-option :produce-statistics true).

[bclement-ocp]

If we add a set-option, we should use a name as close to the CLI option as possible to avoid confusion, such as (set-option :profiling true).

Also, (get-info :all-statistics) should not return an error. We should simply return an empty s-expression here (possibly with a warning message on stderr).

[Halbaroth]

We may use the function Hashtbl.hashhere? I know using this function involves some risks but for a profiling module, the risk is limited.

[bclement-ocp]

What are the risks of Hashtbl.hash you have in mind?

(To be fair I am not sure why we have an explicit datatype to describe profiled functions)

[Halbaroth]

I mean the hash function of Hashtbl doesn't always produce a good hash function to get a O(1) lookup function in your hash table but in our case, it doesn't matter as the hash table is tiny.

[Stevendeo]

We may use the function Hashtbl.hashhere? I know using this function involves some risks but for a profiling module, the risk is limited.

This function already was defined, I just copied it.

[Stevendeo]

If we want a shorter version, we can use Obj.magic which would here work like a charm... 😈

[Stevendeo]

Final choice: ppx_deriving.enum, as it defines the values we want.

[Halbaroth]

What is get-statistics here?

[bclement-ocp]

If we add a set-option, we should use a name as close to the CLI option as possible to avoid confusion, such as (set-option :profiling true).

Also, (get-info :all-statistics) should not return an error. We should simply return an empty s-expression here (possibly with a warning message on stderr).

[bclement-ocp]

This is a safeguard against wrong code: the profiling module maintains a "shadow" trail of decision levels which is also in the SAT module. They must be kept in sync by the SAT module calling reset_dlevel at the appropriate time. If they get out of sync, the profiling information will be garbage; having this invariant helps ensure this does not happen.

[Stevendeo]

Why not just register the decision level of the SAT instead of incrementing it? This invariant forces the Profiling module to be used in a very specific manner, which is undocumented.

[bclement-ocp]

When we make a decision the decision level is always incremented (by definition). As I say, it just looks like a safeguard. It should be correct to call reset_dlevel d here instead of incrementing state.decision_lvl, I'm not sure having the decision level in the profiling matters much anyways.

[Stevendeo]

That's why my comment mentions that, if we don't know if there is a deep meaning behind the error message and what it is, maybe we should just get rid of it. If we ever get in that case and get this error message, I'm not sure we know how to interpret it.

[bclement-ocp]

This error message means that the SAT solver is not calling the profiling module in the expected way, and that the profiling module may be accumulating incorrect statistics, because the state that the profiling module expects the solver to be in and the state the solver actually is in have diverged (they have different decision levels). I am trying to reply to your comment and explain what the error message means.

[Stevendeo]

This error message means that the SAT solver is not calling the profiling module in the expected way,

What is this "expected" way? This function is not documented. I reread the function and I noticed my remark was not correct, the invariant I state is false. My understanding of the function is the following : the decision reference counts the number of decisions taken (sounds good), and the decision level is the "depth" of the decision, in the sense that everytime we decide something we go one step deeper. As we can backtrack decisions, there also is a way to reset the decision level to a given value. Now, I really don't think the profiling module should take care of keeping track of how Alt-Ergo decides its environment handles the depth of its reasoning. Alt-Ergo has an environment depth value, which is a good thing to display while profiling, but that should be it. Calculating its decision level in the profiling looks like a hack, and the fact the printed message is in french comforts me in this idea.
I'll remove my comment anyway, we can decide in another PR if this code is relevant or not.

[bclement-ocp]

I agree this code is not very useful and would be fine removing decision_lvl altogether. I was only replying to your comment asking what it meant. Does it make sense to keep track of the decision level twice? Probably not, but that is what we currently do, and this code checks that the two places we keep track of the decision level agree. I was trying to be helpful, I am sorry if I came across any other way.

[bclement-ocp]

Unless you wrote this code, let's not be that harsh, please :)

[Stevendeo]

Sorry if you actually wrote this code (or to anyone who actually wrote it), for I know the constraints were different when it was written. I use the projects I work on as free expression (maybe I should not) and I would have been as harsh with my own code :) I won't get offended by remarks on my code actually, I use these kinds of remarks as a relief and not to insult the person who wrote it.
Anyway, I'll be more respectful in the future

[bclement-ocp]

I didn't write this code, and I know you didn't intend any harm — as you say, this code has served its purpose, even though there are probably better solutions. I just don't think it is necessary to keep disparaging comments, and it makes for an unpleasant codebase to navigate :)

[Stevendeo]

https://www.reddit.com/r/ProgrammerHumor/comments/1103mbp/c_code_has_higher_code_quality_when_it_contains/

[bclement-ocp]

Good thing we are not writing C then ;)

[bclement-ocp]

What are the risks of Hashtbl.hash you have in mind?

(To be fair I am not sure why we have an explicit datatype to describe profiled functions)

[Stevendeo]

I will take a look at the rest of the changes later, but this patch moves the timers from a global constant in the binary (bin/common/signals_profiling.ml) to a global constant in the library (lib/structures/profiling.ml), which is the opposite of the direction we should be going for (see also #377). Please revert that part of the change.

There is a fundamental issue in the whole profiling system. You can't have profiling global variables in the library to simplify profiling through the analyzer and want some other in the binary. In the previous architecture, the timer was defined in the library, declared in the binary and sent back to the library for profiling. Maybe you have discussed about it, and I would be glad to know your conclusions on the subject ; IMO I think the best choice, for now, is to centralize the whole profiling in the library because we don't want an extra argument for each module to handle profiling from the outside (but again, tell me if it was not your choice).
You will note I lazyfied the timers so that it is only created when the profiling option is on, so that we keep the same behavior than before, but . What I can do in this PR is to lazify the whole profling value instead of only the timer. One of the possibilities to address #377 would be to have sessions : when using alt-ergo-lib, you initialize a session that is linked to a specific profiling value.

[bclement-ocp]

I had a hard time understanding your message, but I see what you mean: what use is it having a Timers.t object that we pass around if it ends up stored in global timer_start and timer_pause functions anyways?

This is a fair point that I didn't consider, but am still not entirely convinced, because the Timers module does two things currently: it provides a data structure to accumulate and print timers, and hooks to register arbitrary profiling functions (that may or may not use the provided data structure, although realistically always will). This looks like good design, and keeps the use of global state to a minimum.

Regarding having an extra argument to each module for profiling: if we clean up the library, we will probably end up with some sort of Config module that is threaded around and has the role of Options currently, and it makes sense to root the profiling functions there. But you are right, that is an issue we will have anyways.

By the way, what is the reasoning for moving from arrays to hash tables for storing the profiling functions? Based on the comments mentioning hash tables that are in the code, it looks like the inverse change has been made at some point in the past.

[Stevendeo]

I had a hard time understanding your message, but I see what you mean: what use is it having a Timers.t object that we pass around if it ends up stored in global timer_start and timer_pause functions anyways?

This is a fair point that I didn't consider, but am still not entirely convinced, because the Timers module does two things currently: it provides a data structure to accumulate and print timers, and hooks to register arbitrary profiling functions (that may or may not use the provided data structure, although realistically always will). This looks like good design, and keeps the use of global state to a minimum.

I am not sure of the relevance of these hooks. What I expect of a hook is to be applied when a timer is started. Here it is quite different : the hook is the start of the timer. Worse: the hooks are not timer dependent, they are library global references...
Anyway, I am not sure what my changes have to do with your point. In my version, the Timers still have these mutable hooks.

By the way, what is the reasoning for moving from arrays to hash tables for storing the profiling functions? Based on the comments mentioning hash tables that are in the code, it looks like the inverse change has been made at some point in the past.

Using arrays is error prone: by forgetting to update a hardcoded list, the profiling option is broken in next. Also, using hashtables allows to not to have a memory saved for unused timers. This second reason is a bad reason actually; now that I think of it, I understand why they used arrays in the first place. My version allocates memory during the analysis, which alters the time spent actually analyzing stuff. With arrays, everything is allocated before the timers starts.
Hmm. We can either go back to arrays or explicitely create all hashtables with the correct sizes.

[bclement-ocp]

Anyway, I am not sure what my changes have to do with your point. In my version, the Timers still have these mutable hooks.

But they are now set in the library rather than the binary. Actually no, they are not set at all — which I think means that no profiling is done at all? Or am I missing something?

Using arrays is error prone: by forgetting to update a hardcoded list, the profiling option is broken in next.

Is this due to all_modules / all_functions not being updated? This should have been caught by the assert on the length, but looks like nb_mtag was not updated either. I think this can be solved by adding an appropriate comment to the type definitions. We could also steal from C's playbook and have M_Last and F_Last as special timers, with nb_mtag = mtag M_Last.

My version allocates memory during the analysis, which alters the time spent actually analyzing stuff. With arrays, everything is allocated before the timers starts.

Yeah, the hash tables allocating during profiling was one thing I was concerned about, indeed.

We can either go back to arrays or explicitely create all hashtables with the correct sizes.

If we initialize the hash tables to have constant sizes, using a hashtable instead of an array will just use more memory and be less efficient, so I'd prefer keeping the arrays. And having a comment (maybe at the top of the module?) that explicitly states "we make sure that functions in this module don't allocate while profiling" or something to that regard.

(Well, "perform minimal allocations" — start will always allocate due to the stack)

[Stevendeo]

But they are now set in the library rather than the binary. Actually no, they are not set at all — which I think means that no profiling is done at all? Or am I missing something?

They are set in the library on a call to Profiling.init (which is made in the binary).

Is this due to all_modules / all_functions not being updated? This should have been caught by the assert on the length, but looks like nb_mtag was not updated either. I think this can be solved by adding an appropriate comment to the type definitions. We could also steal from C's playbook and have M_Last and F_Last as special timers, with nb_mtag = mtag M_Last.

You are right, it was not caught because the counter was not updated either. I'll just go back to arrays and document this design.

[bclement-ocp]

They are set in the library on a call to Profiling.init (which is made in the binary).

Ah, I got got by the fact that this is hidden by default in GitHub's view. Since Profiling.init is in the library, and the Timers function is in the library, if we are going with this design we need to either document that the Timers function are meant for internal use and should not be called by users of the library, or that calling Profiling.init and Timers.set_timer_{start,pause} are mutually exclusive.

[bclement-ocp]

I did not notice the use of let* earlier, apologies — I think that using let* here is quite confusing because it leads to let* state = state in whose behavior is unclear. let* is also traditionally used for a monadic bind operator, which this is not.

Why not instead call this something like if_profiling or when_profiling:

let if_profiling f = if Options.get_profiling () then f (Lazy.force state)

and then use it with:

if_profiling @@ fun state ->
...

which makes the intent more precise?

[bclement-ocp]

(As an aside: in the current state of the code, this leads to duplicate Options.get_profiling () tests because most calls to the Profiling module are guarded with if Options.get_profiling, which is required in some cases because computation has to be performed prior to calling the corresponding profiling function)

[Stevendeo]

I usually go for custom lets to avoid the extra indentation. It really is a taste choice, I don't mind going for explicit continuations

[bclement-ocp]

You don't have to use extra indentation with @@ fun _ ->, and most styles I am aware of don't (in fact, ocp-indent will not let you use extra indentation in this repo if you use this construct).

[Stevendeo]

Oh my bad, I was convinced the @@ to add indentation! Okay, I'll go for it then

[Stevendeo]

They are set in the library on a call to Profiling.init (which is made in the binary).

Ah, I got got by the fact that this is hidden by default in GitHub's view. Since Profiling.init is in the library, and the Timers function is in the library, if we are going with this design we need to either document that the Timers function are meant for internal use and should not be called by users of the library, or that calling Profiling.init and Timers.set_timer_{start,pause} are mutually exclusive.

Same would go in the old functionning of timers actually, or did I miss something? Their functionning was meant for internal use, and used in the binary actually set them the only way it should have been set.
I think a better design would be to associate the timers and their hooks, and that the hooks would be triggered on calls to start.

[bclement-ocp]

Same would go in the old functionning of timers actually, or did I miss something? Their functionning was meant for internal use, and used in the binary actually set them the only way it should have been set.

With the current design, the set_timer_start and set_timer_pause functions are exposed by the library and are the only way to set the timers. This is (to my knowledge) the only interface that allows users of the library (not using the binary) to setup the timers, and so is the de-facto public API for doing so. Now this PR is changing things so that users of the library should only call Profiling.init, but the old functions are still available, and so we should give the information somewhere that the old way of doing things will no longer work as expected (even if I am not sure anyone actually uses the library…). Alt-Ergo is poorly documented, but we should improve the status-quo by writing more documentation, not less!

I think a better design would be to associate the timers and their hooks, and that the hooks would be triggered on calls to start.

I agree — I actually don't think that the hooks should be in the Timers module at all, but rather in Profiling since that's where the global state is at.

[Stevendeo]

I will leave this PR as it is, and open an issue about documenting/rewriting profiling & timers; I feel like this PR about adding all-statistics went a little too far from it's initial purpose :)

[bclement-ocp]

I am OK with that in this case, but I will note that I find it disingenuous to put it this way when the title of the PR includes "refactoring Profiling module" and most of the lines affected by the PR are not about (get-info :all-statistics) at all.