search

JetBrains / lincheck

Framework for testing concurrent data structures
Mozilla Public License 2.0
574 stars 33 forks source link

[PROPOSAL] Smart parameter setting #89

Closed sh-ad closed 1 year ago

sh-ad commented 3 years ago

The idea is that after the first run of the scenario, information about the container under test appears. This information can be useful when selecting startup options.

For example, if in some operation, there are two CAS, then you need at least three threads to check.

Therefore, there is a suggestion: to make some tool that can recommend startup parameters after the execution of a scenario.

sh-ad commented 3 years ago

The idea is to run the check and, based on the results of one iteration, make some assumptions on how best to run a full-fledged check

To do this, you need to understand which metrics can help in the analysis and how to interpret them.

Metric - the number of CAS in the operation, allows you to determine the minimum number of threads to perform the check

ndkoval commented 3 years ago

Hi @sh-ad,

That is an interesting and very nice feature to implement! However, it is much more complicated than it seems at first sight.

First, some algorithms do not use CAS-s for synchronization, some use them only for helping, others may use locks in a non-trivial way -- all these situations have to be handled automatically.

Secondly, the numbers of threads and operations in each of them are not the only parameters -- we have to adjust the numbers of iterations (= different scenarios) and invocations for each scenario. Unfortunately, it is quite complicated, especially with the model checking mode, when the number of invocations changes the depth of the analysis. For example, it is sometimes better to use fewer operations in the scenario, automatically increasing the analysis depth. At the same time, some bugs require more operations to be reproduced. How to balance here? In my opinion, there is no silver bullet, and the best configuration depends on the data structure, but we do not have intuition on how exactly it depends. Therefore, now the developer of the data structure specifies the configuration.

All in all, this feature has good potential but requires non-trivial research, so I am not sure that it worth it.

ndkoval commented 1 year ago

As #137 is on the roadmap, I am closing this issue.